Detail publikace
A Novel Approach to Modechart Verification of Real-Time systems
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{BUT76434,
author="Jan {Fiedor} and Marek {Gach} and Milan {Češka}",
title="A Novel Approach to Modechart Verification of Real-Time systems",
booktitle="Proceedings of the 13th International Conference on Computer Aided Systems Theory",
year="2011",
pages="338--339",
publisher="The Universidad de Las Palmas de Gran Canaria",
address="Universidad de Las Palmas de Canaria",
isbn="978-84-693-9560-8"
}