Přístupnostní navigace
E-application
Search Search Close
Publication result detail
RYŠAVÝ, O.; RÁB, J.
Original Title
A Component-based Approach to Verification of Embedded Control Systems using TLA
English Title
Type
Paper in proceedings outside WoS and Scopus
Original 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.
English abstract
Keywords
Control systems, real-time software, temporal logic of actions, verification of RT systems, component based approach
Key words in English
Authors
RIV year
2012
Released
27.10.2008
Publisher
IEEE Computer Society Press
Location
Wisla
ISBN
978-83-60810-14-9
Book
IEEE Proceedings of International Multiconference on Computer Science and Information Technology
Pages from
719
Pages to
725
Pages count
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/" }
Documents