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+

Anglický název

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

Jazyk

en

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.

Anglický 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.

Dokumenty

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+",
  annote="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.",
  address="IEEE Computer Society Press",
  booktitle="IEEE Proceedings of International Multiconference on Computer Science and Information Technology",
  chapter="32077",
  edition="NEUVEDEN",
  howpublished="print",
  institution="IEEE Computer Society Press",
  year="2008",
  month="october",
  pages="719--725",
  publisher="IEEE Computer Society Press",
  type="conference paper"
}