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"
}