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/ |
| Shrnutí: | 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 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 |
|---|---|
| Popis jednotky: | Vedoucí práce: Jiří Barnat |
| Fyzický popis: | xiii, 149 stran |