Detail výsledku

A Formal Model of Composing Components: The TLA+ Approach

RYŠAVÝ, O.; RÁB, J. A Formal Model of Composing Components: The TLA+ Approach. Innovations in Systems and Software Engineering, 2009, vol. 5, no. 2, p. 139-149. ISSN: 1614-5046.
Typ
článek v časopise
Jazyk
anglicky
Autoři
Ryšavý Ondřej, doc. Ing., Ph.D., UIFS (FIT)
Ráb Jaroslav, Ing., UIFS (FIT)
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

URL
Rok
2009
Strany
139–149
Časopis
Innovations in Systems and Software Engineering, roč. 5, č. 2, ISSN 1614-5046
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/"
}
Soubory
Projekty
Bezpečnost a zabezpečení aplikací sítí vestavěných systémů, GAČR, Standardní projekty, GA102/08/1429, zahájení: 2008-01-01, ukončení: 2010-12-31, ukončen
Rámec pro deduktivní analýzu softwarových aplikací vestavěných systémů, GAČR, Postdoktorandské granty, GP201/07/P544, zahájení: 2007-01-01, ukončení: 2008-12-31, ukončen
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, zahájení: 2007-01-01, ukončení: 2013-12-31, řešení
Výzkumné skupiny
NES@FIT - Výzkumná skupina počítačové sítě (VZ NES@FIT)
Pracoviště
Ústav informačních systémů (UIFS)
Nahoru