Result 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.
Type
conference paper
Language
English
Authors
Ryšavý Ondřej, doc. Ing., Ph.D., DIFS (FIT)
Ráb Jaroslav, Ing., FIT (FIT), DIFS (FIT)
Ráb Jaroslav, Ing., FIT (FIT), DIFS (FIT)
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.
Keywords
Control systems, real-time software, temporal logic of actions, verification of RT systems, component based approach
URL
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
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/"
}
Files
Projects
Framework for the deductive analysis of embedded software, GACR, Postdoktorandské granty, GP201/07/P544, start: 2007-01-01, end: 2008-12-31, completed
Safety and security of networked embedded system applications, GACR, Standardní projekty, GA102/08/1429, start: 2008-01-01, end: 2010-12-31, completed
Security-Oriented Research in Information Technology, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, start: 2007-01-01, end: 2013-12-31, running
Safety and security of networked embedded system applications, GACR, Standardní projekty, GA102/08/1429, start: 2008-01-01, end: 2010-12-31, completed
Security-Oriented Research in Information Technology, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, start: 2007-01-01, end: 2013-12-31, running
Research groups
Departments