Detail výsledku

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.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Ryšavý Ondřej, doc. Ing., Ph.D., UIFS (FIT)
Ráb Jaroslav, Ing., FIT (FIT), UIFS (FIT)
Abstrakt

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.

Klíčová slova

Control systems, real-time software, temporal logic of actions, verification of RT systems, component based approach

URL
Rok
2008
Strany
719–725
Sborník
IEEE Proceedings of International Multiconference on Computer Science and Information Technology
Konference
International Multiconference on Computer Science and Information Technology - RTS 2008
ISBN
978-83-60810-14-9
Vydavatel
IEEE Computer Society Press
Místo
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/"
}
Soubory
Projekty
Bezpečnost a zabezpečení aplikací sítí vestavěných systémů, GAČR, Standardní projekty, GA102/08/1429, zahájení: 2008-01-01, ukončení: 2010-12-31, ukončen
Rámec pro deduktivní analýzu softwarových aplikací vestavěných systémů, GAČR, Postdoktorandské granty, GP201/07/P544, zahájení: 2007-01-01, ukončení: 2008-12-31, ukončen
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, zahájení: 2007-01-01, ukončení: 2013-12-31, řešení
Výzkumné skupiny
NES@FIT - Výzkumná skupina počítačové sítě (VZ NES@FIT)
Pracoviště
Ústav informačních systémů (UIFS)
Nahoru