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.
展开▼
