Detail publikace

A Formal Model of Composing Components: The TLA+ Approach

Originální název

A Formal Model of Composing Components: The TLA+ Approach

Anglický název

A Formal Model of Composing Components: The TLA+ Approach

Jazyk

en

Originální abstrakt

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.

Anglický abstrakt

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{BUT47967,
  author="Ondřej {Ryšavý} and Jaroslav {Ráb}",
  title="A Formal Model of Composing Components: The TLA+ Approach",
  annote="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.",
  address="NEUVEDEN",
  chapter="47967",
  edition="NEUVEDEN",
  howpublished="print",
  institution="NEUVEDEN",
  journal="Innovations in Systems and Software Engineering",
  number="2",
  volume="5",
  year="2009",
  month="april",
  pages="139--149",
  publisher="NEUVEDEN",
  type="journal article - other"
}