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
Ryšavý Ondřej, doc. Ing., Ph.D. (DIFS FIT BUT)
Ráb Jaroslav, Ing. (DIFS FIT BUT)
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