Detail publikace
A Novel Approach to Modechart Verification of Real-Time Systems
Fiedor Jan, Ing., Ph.D. (UITS FIT VUT)
Gach Marek, Ing. (UITS FIT VUT)
Modechart, verifikace, rt-systém, RTL
Jelikož systémy pracující s reálným časem jsou striktně časově omezené a jejich porucha může mít fatální následky, je důležité zajistit jejich korektní chování. Existuje mnoho přístupů k verifikaci systémů pracujících s reálným časem. Jedny používají grafické formalismy, jiné různorodé množství logic umožňujících popis verifikovaných systémů. Ikdyž grafický popis je značně jednodušší pro použití, neumožňuje použít mnoho silných metod pro analýzu a verifikaci. V tomto článku navrhujeme nový přístup k verifikaci systémů pracujících s reálným časem popsaných grafickým formalismem Modechart založený na transformaci výpočtu systému do podoby množiny formulí omezené RTL logiky. Dále, jestli verifikovaná vlastnost systému je známa v době verifikace, jsme schopni redukovat počet výsledných formulí.
@INPROCEEDINGS{FITPUB9744, author = "Milan \v{C}e\v{s}ka and Jan Fiedor and Marek Gach", title = "A Novel Approach to Modechart Verification of Real-Time Systems", pages = "338--339", booktitle = "Proceedings of the 13th International Conference on Computer Aided Systems Theory", year = 2011, location = "Universidad de Las Palmas de Canaria, ES", publisher = "The Universidad de Las Palmas de Gran Canaria", ISBN = "978-84-693-9560-8", language = "english", url = "https://www.fit.vut.cz/research/publication/9744" }