Publication Details

A Formal Model of Composing Components: The TLA+ Approach

RYŠAVÝ Ondřej and RÁB Jaroslav. A Formal Model of Composing Components: The TLA+ Approach. Innovations in Systems and Software Engineering, vol. 5, no. 2, 2009, pp. 139-149. ISSN 1614-5046.
Czech title
Formální model komponent: Použití jazyka TLA+
Type
journal article
Language
english
Authors
URL
Keywords

Composing Specifications, Component Model, Hierarchical Specifications, Synchronous Mode of Executions, Temporal Logic of Actions

Abstract

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.

Published
2009
Pages
139-149
Journal
Innovations in Systems and Software Engineering, vol. 5, no. 2, ISSN 1614-5046
Publisher
Springer London
BibTeX
@ARTICLE{FITPUB8861,
   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 = "https://www.fit.vut.cz/research/publication/8861"
}
Back to top