Detail publikace

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

RYŠAVÝ, O.; RÁB, J. A Component-based Approach to Verification of Embedded Control Systems using TLA+. IEEE Proceedings of International Multiconference on Computer Science and Information Technology. Wisla: IEEE Computer Society Press, 2008. p. 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
anglicky
Autoři
Ryšavý Ondřej, doc. Ing., Ph.D. (UIFS)
Ráb Jaroslav, Ing.
URL
Klíčová slova

Control systems, real-time software, temporal logic of actions, verification of RT systems, component based approach

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
ISBN
978-83-60810-14-9
Vydavatel
IEEE Computer Society Press
Místo
Wisla
BibTeX 
@inproceedings{BUT32077,
  author="Ondřej {Ryšavý} and Jaroslav {Ráb}",
  title="A Component-based Approach to Verification of Embedded Control Systems using TLA+",
  booktitle="IEEE Proceedings of International Multiconference on Computer Science and Information Technology",
  year="2008",
  pages="719--725",
  publisher="IEEE Computer Society Press",
  address="Wisla",
  isbn="978-83-60810-14-9",
  url="https://www.fit.vut.cz/research/publication/8772/"
}
Nahoru