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