Detail publikace

Model-Based Design and Verification of Reactive Systems

ČEŠKA, M. HÝSEK, J. JANOUŠEK, V.

Originální název

Model-Based Design and Verification of Reactive Systems

Anglický název

Model-Based Design and Verification of Reactive Systems

Jazyk

en

Originální abstrakt

The article is focused on a model-based design and verification of reactive systems. In opposite to common approaches to developing reliable systems, at first a model of a system is constructed in high level visual language, then it is verified on this level of abstraction and consequently a low level code for target platform is generated. In approach discussed in this article an UML statechart formalism is used for construction of the model. This model is translated into Promela model and verified by the SPIN model checker.

Anglický abstrakt

The article is focused on a model-based design and verification of reactive systems. In opposite to common approaches to developing reliable systems, at first a model of a system is constructed in high level visual language, then it is verified on this level of abstraction and consequently a low level code for target platform is generated. In approach discussed in this article an UML statechart formalism is used for construction of the model. This model is translated into Promela model and verified by the SPIN model checker.

Dokumenty

BibTex


@article{BUT46898,
  author="Milan {Češka} and Jiří {Hýsek} and Vladimír {Janoušek}",
  title="Model-Based Design and Verification of Reactive Systems",
  annote="The article is focused on a model-based design and verification of reactive
systems. In opposite to common approaches to developing reliable systems, at
first a model of a system is constructed in high level visual language, then it
is verified on this level of abstraction and consequently a low level code for
target platform is generated. In approach discussed in this article an UML
statechart formalism is used for construction of the model. This model is
translated into Promela model and verified by the SPIN model checker.",
  address="NEUVEDEN",
  booktitle="Computer Aided Systems Theory - EUROCAST 2009",
  chapter="46898",
  edition="NEUVEDEN",
  howpublished="print",
  institution="NEUVEDEN",
  journal="Lecture Notes in Computer Science (IF 0,513)",
  number="5717",
  volume="2009",
  year="2009",
  month="september",
  pages="865--872",
  publisher="NEUVEDEN",
  type="journal article - other"
}