Faculty of Information Technology, BUT

Publication Details

A Component-based Approach to Verification of Embedded Control Systems using TLA

RYŠAVÝ Ondřej and RÁB Jaroslav. A Component-based Approach to Verification of Embedded Control Systems using TLA+. In: IEEE Proceedings of International Multiconference on Computer Science and Information Technology. Wisla: IEEE Computer Society Press, 2008, pp. 719-725. ISBN 978-83-60810-14-9.
Czech title
Verifikace vestavěných řídících systémů v jazyce TLA+ založená na komponentovém přístupu
Type
conference paper
Language
english
Authors
URL
Keywords
Control systems, real-time software, temporal logic of actions, verification of RT systems, component based approach
Abstract
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.
Published
2008
Pages
719-725
Proceedings
IEEE Proceedings of International Multiconference on Computer Science and Information Technology
Conference
International Multiconference on Computer Science and Information Technology - RTS 2008, Wisla, PL
ISBN
978-83-60810-14-9
Publisher
IEEE Computer Society Press
Place
Wisla, PL
BibTeX
@INPROCEEDINGS{FITPUB8772,
   author = "Ond\v{r}ej Ry\v{s}av\'{y} and Jaroslav R\'{a}b",
   title = "A Component-based Approach to Verification of Embedded Control Systems using TLA",
   pages = "719--725",
   booktitle = "IEEE Proceedings of International Multiconference on Computer Science and Information Technology",
   year = 2008,
   location = "Wisla, PL",
   publisher = "IEEE Computer Society Press",
   ISBN = "978-83-60810-14-9",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/8772"
}
Back to top