A component-based approach to verification of embedded control systems using TLA+
Ondřej Ryšavý, Jaroslav Rab · Proceedings of the International Multiconference on Computer Science and Information Technology · 2008
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.