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
+Type Name Title Size Last modified
iconrysavy_08_modeling.pdfA Formal Model of Composing Components: The TLA+ Approach186 KB2009-05-04 22:30:17
^ Select all
With selected:
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 R{\'{a}}b},
   title = {A Formal Model of Composing Components: The TLA+ Approach},
   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 IPv6 connection

DNSSEC [dnssec]