Publication Details

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

RYŠAVÝ, O.; RÁB, J. A Component-based Approach to Verification of Embedded Control Systems using TLA+. IEEE Proceedings of International Multiconference on Computer Science and Information Technology. Wisla: IEEE Computer Society Press, 2008. p. 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)
Ráb Jaroslav, Ing.
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
ISBN
978-83-60810-14-9
Publisher
IEEE Computer Society Press
Place
Wisla
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/"
}
Back to top