Title :
A component-based approach to verification of embedded control systems using TLA+
Author :
Rysavy, Ondrej ; Rab, Jaroslav
Author_Institution :
Fac. of Inf. Technol., Brno Univ. of Technol., Brno
Abstract :
The method for writing TLA+ specifications that obey formal model called Masaccio is presented in this paper. The specifications consist of components, which are built from atomic components by parallel and serial compositions. Using a simple example, it is illustrated how to write specifications of atomic components and components those are products of parallel or serial compositions. The specifications have standard form of TLA+ specifications hence they are amenable to automatic verification using the TLA+ model-checker.
Keywords :
control engineering computing; formal specification; formal verification; object-oriented programming; Masaccio; TLA+ model-checker; TLA+ specification; atomic component; automatic verification; component-based approach; embedded control system; formal model; Computer science; Control system synthesis; Control systems; Embedded software; Information technology; Input variables; Object oriented modeling; Object oriented programming; Read only memory; Writing;
Conference_Titel :
Computer Science and Information Technology, 2008. IMCSIT 2008. International Multiconference on
Conference_Location :
Wisia
Print_ISBN :
978-83-60810-14-9
DOI :
10.1109/IMCSIT.2008.4747321
