Publication detail

A Formal Model of Composing Components: The TLA+ Approach

RYŠAVÝ, O. RÁB, J.

Original Title

A Formal Model of Composing Components: The TLA+ Approach

Type

journal article - other

Language

English

Original 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.

Keywords

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

Authors

RYŠAVÝ, O.; RÁB, J.

RIV year

2009

Released

8. 4. 2009

ISBN

1614-5046

Periodical

Innovations in Systems and Software Engineering

Year of study

5

Number

2

State

United Kingdom of Great Britain and Northern Ireland

Pages from

139

Pages to

149

Pages count

10

URL

https://www.fit.vut.cz/research/publication/8861/

BibTex

@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/"
}

Documents

rysavy_08_modeling.pdf