Detail publikace

A Component-based Approach to Verification of Embedded Control Systems using TLA

RYŠAVÝ Ondřej a RÁB Jaroslav. A Component-based Approach to Verification of Embedded Control Systems using TLA. In: IEEE Proceedings of International Multiconference on Computer Science and Information Technology. Wisla: IEEE Computer Society Press, 2008, s. 719-725. ISBN 978-83-60810-14-9.
Název česky
Verifikace vestavěných řídících systémů v jazyce TLA+ založená na komponentovém přístupu
Typ
článek ve sborníku konference
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

Methoda pro zápis TLA+ specifikací, které splňují vlastnosti formálního modelu Masaccio je prezentována v tomto příspěvku. Specifikace se sestává z komponent, které jsou vytvořeny z atomických komponent pomocí operaci seriového   a paralelního uspořádání. Za použití jednoduchého příkladu je ilustrováno, jak jsou tyto operace použity ve specifikaci. Výsledná specifikace má standardní tvar TLA+ specifikace a je tudíž vhodným vstupem pro automatickou verifikaci za použití TLA+ model-checkeru.

Rok
2008
Strany
719-725
Sborník
IEEE Proceedings of International Multiconference on Computer Science and Information Technology
Konference
International Multiconference on Computer Science and Information Technology - RTS 2008, Wisla, PL
ISBN
978-83-60810-14-9
Vydavatel
IEEE Computer Society Press
Místo
Wisla, PL
BibTeX 
@INPROCEEDINGS{FITPUB8772,
   author = "Ond\v{r}ej Ry\v{s}av\'{y} and Jaroslav R\'{a}b",
   title = "A Component-based Approach to Verification of Embedded Control Systems using TLA",
   pages = "719--725",
   booktitle = "IEEE Proceedings of International Multiconference on Computer Science and Information Technology",
   year = 2008,
   location = "Wisla, PL",
   publisher = "IEEE Computer Society Press",
   ISBN = "978-83-60810-14-9",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/8772"
}
Nahoru