Detail publikace

A Novel Approach to Modechart Verification of Real-Time systems

ČEŠKA, M.; FIEDOR, J.; GACH, M. A Novel Approach to Modechart Verification of Real-Time systems. Lecture Notes in Computer Science, 2012, vol. 2012, no. 6927, p. 559-567. ISSN: 0302-9743.
Název česky
Nový přístup verifikace real-time systémů ve formalismu Modechart
Typ
článek v časopise
Jazyk
anglicky
Autoři
Češka Milan, prof. RNDr., CSc.
Fiedor Jan, Ing., Ph.D. (UITS)
Gach Marek, Ing.
Klíčová slova

Modechart, verifikace, rt-systém, RTL

Abstrakt

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í.

Rok
2012
Strany
559–567
Časopis
Lecture Notes in Computer Science, roč. 2012, č. 6927, ISSN 0302-9743
BibTeX 
@article{BUT91441,
  author="Milan {Češka} and Jan {Fiedor} and Marek {Gach}",
  title="A Novel Approach to Modechart Verification of Real-Time systems",
  journal="Lecture Notes in Computer Science",
  year="2012",
  volume="2012",
  number="6927",
  pages="559--567",
  issn="0302-9743"
}
Nahoru