Journal article

Ryšavý, O., Ráb, J.: A Formal Model of Composing Components: The TLA+ Approach, In: Innovations in Systems and Software Engineering, Vol. 5, No. 2, 2009, London, GB, p. 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+

Pages:

139-149

Place:

Year:

2009

Journal:

Innovations in Systems and Software Engineering, Vol. 5, No. 2, London, GB

ISSN:

1614-5046

URL:

http://www.springerlink.com/content/vjh60p16x5343401/fulltext.pdf [PDF]

Files:

Keywords

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

Annotation

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.

BibTeX:

@ARTICLE{
   author = {Ondřej Ryšavý and Jaroslav Rá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 = {http://www.fit.vutbr.cz/research/view_pub.php?id=8861}
}

You are in section

Journal article