Detail publikace

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.
Název česky
Formální model komponent: Použití jazyka TLA+
Typ
článek v časopise
Jazyk
anglicky
Autoři
Ryšavý Ondřej, doc. Ing., Ph.D. (UIFS)
Ráb Jaroslav, Ing.
URL
Klíčová slova

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

Abstrakt

 V tomto článku je představena metoda pro zápis TLA+ specifikací, které odpovídají modelu Masaccio. Specifikace jsou organizovány jako TLA+ moduly, které korespondují s Masaccio komponenty trace-based semantikou. Hierarchické TLA+ specifikace jsou tvořeny z atomických komponent pomocí operací seriového a paralelního skládání. Zatímco pravidlo paralelního skládání je variantou klasického joint-action skládání, operace seriového skládání a její systematické využití v TLA+ specifikací je nové. Kombinací těchto operací a předpoklad neprokládaného synchroního režimu provádění je dosaženo paralelní, sekvenční a časové komposability.

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