Detail publikace

A Formal Model of Composing Components: The TLA+ Approach

RYŠAVÝ Ondřej a RÁB Jaroslav. A Formal Model of Composing Components: The TLA+ Approach. Innovations in Systems and Software Engineering, roč. 5, č. 2, 2009, s. 139-149. ISSN 1614-5046.
Název česky
Formální model komponent: Použití jazyka TLA+
Typ
článek v časopise
Jazyk
angličtina
Autoři
Ryšavý Ondřej, doc. Ing., Ph.D. (UIFS FIT VUT)
Ráb Jaroslav, Ing. (UIFS FIT VUT)
URL
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
Vydavatel
Springer London
BibTeX 
@ARTICLE{FITPUB8861,
   author = "Ond\v{r}ej Ry\v{s}av\'{y} and Jaroslav R\'{a}b",
   title = "A Formal Model of Composing Components: The TLA+ Approach",
   pages = "139--149",
   journal = "Innovations in Systems and Software Engineering",
   volume = 5,
   number = 2,
   year = 2009,
   ISSN = "1614-5046",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/8861"
}
Nahoru