Automating Software Development with Explicit Model Checking /
Tato práce je postavená na předpokladu, že funkční požadavky je možné vyjádřit temporální logikou a obsahem této práce jsou nové způsoby verifikace jak požadavků samotných tak jejích splnění běhěm celého vývojového procesu. Cílem práce je automatizace některých verifikačních procesů, které se v souč...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Další autoři: | |
| Typ dokumentu: | VŠ práce nebo rukopis |
| Jazyk: | Angličtina |
| Vydáno: |
2016
|
| Témata: | |
| On-line přístup: | http://is.muni.cz/th/208047/fi_d/ |
| LEADER | 05681ctm a22009017i 4500 | ||
|---|---|---|---|
| 001 | MUB01006359895 | ||
| 003 | CZ BrMU | ||
| 005 | 20240516125459.0 | ||
| 008 | 160219s2016 xr ||||| |||||||||||eng d | ||
| STA | |a POSLANO DO SKCR |b 2016-12-16 | ||
| 035 | |a (ISMU-VSKP)220693 | ||
| 040 | |a BOD114 |b cze |d BOD018 |e rda | ||
| 072 | 7 | |a 004.4/.6 |x Programování. Software |2 Konspekt |9 23 | |
| 080 | |a (0.034.2)004.4 |2 MRF | ||
| 080 | |a 004.42 |2 MRF | ||
| 080 | |a 681.5 |2 MRF | ||
| 100 | 1 | |a Bauch, Petr |% UČO 208047 |* [absolvent FI MU] |4 dis | |
| 242 | 1 | 0 | |a Automating Software Development with Explicit Model Checking |y eng |
| 245 | 1 | 0 | |a Automating Software Development with Explicit Model Checking / |c Petr Bauch |
| 264 | 0 | |c 2016 | |
| 300 | |a xiii, 149 stran | ||
| 336 | |a text |b txt |2 rdacontent | ||
| 337 | |a bez média |b n |2 rdamedia | ||
| 338 | |a svazek |b nc |2 rdacarrier | ||
| 500 | |a Vedoucí práce: Jiří Barnat | ||
| 502 | |a Dizertace (Ph.D.)--Masarykova univerzita, Fakulta informatiky, 2016 | ||
| 520 | 2 | |a Tato práce je postavená na předpokladu, že funkční požadavky je možné vyjádřit temporální logikou a obsahem této práce jsou nové způsoby verifikace jak požadavků samotných tak jejích splnění běhěm celého vývojového procesu. Cílem práce je automatizace některých verifikačních procesů, které se v současné době používají během vývoje programů. Hlavním prostředkem pro dosažení tohoto cíle je technika ověřování modelů pomocí automatů s explicitními stavy. V části zaměřené na ověřování požadavků navrhujeme nové techniky, které automaticky detekují nedostatky a navrhují zlepšení daných požadavků. Konkrétně popisujeme a experimentálně vyhodnocujeme postupy ověřování konzistence a redundance, které identifikují všechny nekonzistence a přesně lokalizují jejich zdroj (nejmenší nekonzistentní podmnožiny). V části zaměřené na splnění požadavků navrhujeme rozšíření explicitní kontroly modelů aby škálovala v realistických programech. Používáme techniky kontroly modelů s explicitními stavy pro zachyce |% cze | |
| 520 | 2 | 9 | |a This thesis builds on the fact that functional requirements can be expressed in temporal logic and we propose new means of verifying the requirements themselves and the compliance to those requirements throughout the development process. The goal is the automation of some of the verification processes currently employed in software development. The tool is the automata-based, explicit-state model checking. With respect to requirements, we propose new techniques that automatically detect flaws and suggest improvements of given requirements. Specifically, we describe and experimentally evaluate approaches to consistency and redundancy checking that identify all inconsistencies and pinpoint their exact source (the smallest inconsistent set). With respect to compliance to requirements, we propose extending the explicit model checking to scale to more realistic programs. We apply the techniques of explicit-state model checking to account for the control aspects of verified programs and use |9 eng |
| 650 | 0 | 7 | |a software |7 ph125823 |2 czenas |
| 650 | 0 | 7 | |a programování |7 ph115891 |2 czenas |
| 650 | 0 | 7 | |a automatizace |7 ph114100 |2 czenas |
| 650 | 0 | 9 | |a software |2 eczenas |
| 650 | 0 | 9 | |a programming |2 eczenas |
| 650 | 0 | 9 | |a automation |2 eczenas |
| 655 | 7 | |a disertace |7 fd132024 |2 czenas | |
| 655 | 9 | |a dissertations |2 eczenas | |
| 658 | |a Informatika (čtyřleté) |b Počítačové systémy a technologie |c FI D-IN4 PST (PST) |2 CZ-BrMU | ||
| 700 | 1 | |a Barnat, Jiří, |d 1977- |7 mub2010575337 |% UČO 3496 |4 ths | |
| 710 | 2 | |a Masarykova univerzita. |b Katedra teorie programování |4 dgg | |
| 856 | 4 | 1 | |u http://is.muni.cz/th/208047/fi_d/ |
| CAT | |c 20160219 |l MUB01 |h 0420 | ||
| CAT | |a HANAV |b 02 |c 20160222 |l MUB01 |h 1653 | ||
| CAT | |a POSPEL |b 02 |c 20160224 |l MUB01 |h 0751 | ||
| CAT | |a POSPEL |b 02 |c 20160914 |l MUB01 |h 1427 | ||
| CAT | |a POSPEL |b 02 |c 20160920 |l MUB01 |h 0817 | ||
| CAT | |a POSPEL |b 02 |c 20160927 |l MUB01 |h 0741 | ||
| CAT | |a VESELA |b 02 |c 20161130 |l MUB01 |h 1454 | ||
| CAT | |c 20161216 |l MUB01 |h 1323 | ||
| CAT | |a POSPEL |b 02 |c 20170228 |l MUB01 |h 1036 | ||
| CAT | |a POSPEL |b 02 |c 20170302 |l MUB01 |h 0828 | ||
| CAT | |a POSPEL |b 02 |c 20180314 |l MUB01 |h 0814 | ||
| CAT | |a POSPEL |b 02 |c 20180503 |l MUB01 |h 0729 | ||
| CAT | |a POSPEL |b 02 |c 20180710 |l MUB01 |h 0635 | ||
| CAT | |a POSPEL |b 02 |c 20190213 |l MUB01 |h 0800 | ||
| CAT | |a POSPEL |b 02 |c 20190924 |l MUB01 |h 0745 | ||
| CAT | |a POSPEL |b 02 |c 20200510 |l MUB01 |h 2306 | ||
| CAT | |a POSPEL |b 02 |c 20201212 |l MUB01 |h 2150 | ||
| CAT | |a POSPEL |b 02 |c 20210122 |l MUB01 |h 0054 | ||
| CAT | |a POSPEL |b 02 |c 20210322 |l MUB01 |h 1142 | ||
| CAT | |a POSPEL |b 02 |c 20210327 |l MUB01 |h 0026 | ||
| CAT | |c 20210614 |l MUB01 |h 1018 | ||
| CAT | |c 20210614 |l MUB01 |h 2005 | ||
| CAT | |a BATCH |b 00 |c 20210724 |l MUB01 |h 1244 | ||
| CAT | |a POSPEL |b 02 |c 20210912 |l MUB01 |h 2336 | ||
| CAT | |a POSPEL |b 02 |c 20211010 |l MUB01 |h 2218 | ||
| CAT | |a HANAV |b 02 |c 20211115 |l MUB01 |h 1631 | ||
| CAT | |a POSPEL |b 02 |c 20220629 |l MUB01 |h 0104 | ||
| CAT | |a POSPEL |b 02 |c 20221019 |l MUB01 |h 2326 | ||
| CAT | |a POSPEL |b 02 |c 20221101 |l MUB01 |h 0840 | ||
| CAT | |a POSPEL |b 02 |c 20230629 |l MUB01 |h 0037 | ||
| CAT | |a POSPEL |b 02 |c 20240226 |l MUB01 |h 1300 | ||
| CAT | |a POSPEL |b 02 |c 20240405 |l MUB01 |h 2123 | ||
| CAT | |a VESELAX |b 02 |c 20240516 |l MUB01 |h 1254 | ||
| CAT | |a VESELAX |b 02 |c 20240516 |l MUB01 |h 1254 | ||
| LOW | |a POSLANO DO SKCR |b 2016-12-16 | ||
| 994 | - | 1 | |l MUB01 |l MUB01 |m VYSPR |1 FI |a Fakulta informatiky |3 Diz. práce 2015 |5 42005D2669 |8 20161130 |f 72 |f Týdenní |r 20161130 |
| AVA | |a INF50 |b FI |d Diz. práce 2015 |e available |t K dispozici |f 1 |g 0 |h N |i 0 | ||