Publication detail

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

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

Original Title

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

Type

article in a collection out of WoS and Scopus

Language

English

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.

Keywords

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

Authors

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

RIV year

2008

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

rysavy_08_component.pdf