Automating Software Development with Explicit Model Checking - Bauch, Petr (2016)
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