Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail publikace
RYŠAVÝ, O. RÁB, J.
Originální název
A Formal Model of Composing Components: The TLA+ Approach
Typ
článek v časopise - ostatní, Jost
Jazyk
angličtina
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.
Klíčová slova
Composing Specifications, Component Model, Hierarchical Specifications, Synchronous Mode of Executions, Temporal Logic of Actions
Autoři
RYŠAVÝ, O.; RÁB, J.
Rok RIV
2009
Vydáno
8. 4. 2009
ISSN
1614-5046
Periodikum
Innovations in Systems and Software Engineering
Ročník
5
Číslo
2
Stát
Spojené království Velké Británie a Severního Irska
Strany od
139
Strany do
149
Strany počet
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/" }