Publication Details
A Formal Model of Composing Components: The TLA+ Approach
Ráb Jaroslav, Ing.
Composing Specifications, Component Model, Hierarchical Specifications, Synchronous Mode of Executions, Temporal Logic of Actions
In this paper, a method for writing composable TLA+ specifications that conform to the formal model called Masaccio is introduced. Specifications are organized in TLA+ modules that correspond to Masaccio components by means of a trace-based semantics. Hierarchical TLA+ specifications are built from atomic component specifications by parallel and serial composition that can be arbitrary nested. While the rule of parallel composition is a variation of the classical joint-action composition, the authors do not know about a reuse method for the TLA+ that systematically employs the presented kind of a serial composition. By combining these two composition rules and assuming only the noninterleaving synchronous mode of an execution, the concurrent, sequential, and timed compositionality is achieved.
@article{BUT47967,
author="Ondřej {Ryšavý} and Jaroslav {Ráb}",
title="A Formal Model of Composing Components: The TLA+ Approach",
journal="Innovations in Systems and Software Engineering",
year="2009",
volume="5",
number="2",
pages="139--149",
issn="1614-5046",
url="https://www.fit.vut.cz/research/publication/8861/"
}