Detail publikace

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

RYŠAVÝ, O. RÁB, J.

Originální název

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

Typ

článek ve sborníku mimo WoS a Scopus

Jazyk

angličtina

Originální 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

Autoři

RYŠAVÝ, O.; RÁB, J.

Rok RIV

2008

Vydáno

27. 10. 2008

Nakladatel

IEEE Computer Society Press

Místo

Wisla

ISBN

978-83-60810-14-9

Kniha

IEEE Proceedings of International Multiconference on Computer Science and Information Technology

Strany od

719

Strany do

725

Strany počet

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/"
}

Dokumenty

rysavy_08_component.pdf