Journal article

RYŠAVÝ Ondřej and RÁB Jaroslav. A Formal Model of Composing Components: The TLA+ Approach. Innovations in Systems and Software Engineering. London: Springer London, 2009, vol. 5, no. 2, pp. 139-149. ISSN 1614-5046.
Publication language:english
Original title:A Formal Model of Composing Components: The TLA+ Approach
Title (cs):Formální model komponent: Použití jazyka TLA+
Journal:Innovations in Systems and Software Engineering, Vol. 5, No. 2, London, GB
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.
   author = {Ond{\v{r}}ej Ry{\v{s}}av{\'{y}} and Jaroslav
   title = {A Formal Model of Composing Components: The TLA+
   pages = {139--149},
   journal = {Innovations in Systems and Software Engineering},
   volume = 5,
 number = 2,
   year = 2009,
   ISSN = {1614-5046},
   language = {english},
   url = {}

Your IPv4 address:
Switch to https