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í.
@ARTICLE{FITPUB9631, 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 = "559--567", journal = "Lecture Notes in Computer Science", volume = 2012, number = 6927, year = 2012, ISSN = "0302-9743", language = "english", url = "https://www.fit.vut.cz/research/publication/9631" }