Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail publikačního výsledku
RYŠAVÝ, O.; RÁB, J.
Originální název
A Component-based Approach to Verification of Embedded Control Systems using TLA
Anglický název
Druh
Stať ve sborníku mimo WoS a Scopus
Originální abstrakt
The method for writing TLA+specifications that obey a formal model called Masaccio is presented in this paper. The specifications consist of components, which are built from atomic components by parallel and serial composition. Using a simple example, it is illustrated how to write specifications of atomic components and components that are products of parallel or serial compositions. The specifications have standard form of the TLA+specifications hence they are amenable to automatic verification using the TLA+model-checker.
Anglický abstrakt
Klíčová slova
Control systems, real-time software, temporal logic of actions, verification of RT systems, component based approach
Klíčová slova v angličtině
Autoři
Rok RIV
2012
Vydáno
27.10.2008
Nakladatel
IEEE Computer Society Press
Místo
Wisla
ISBN
978-83-60810-14-9
Kniha
IEEE Proceedings of International Multiconference on Computer Science and Information Technology
Strany od
719
Strany do
725
Strany počet
7
URL
https://www.fit.vut.cz/research/publication/8772/
BibTex
@inproceedings{BUT32077, author="Ondřej {Ryšavý} and Jaroslav {Ráb}", title="A Component-based Approach to Verification of Embedded Control Systems using TLA", booktitle="IEEE Proceedings of International Multiconference on Computer Science and Information Technology", year="2008", pages="719--725", publisher="IEEE Computer Society Press", address="Wisla", isbn="978-83-60810-14-9", url="https://www.fit.vut.cz/research/publication/8772/" }
Dokumenty