Indefinite waitings in MIRELA systems

Johan Arcile
(Laboratoire IBISC, Université d'Evry-Val d'Essonne)
Jean-Yves Didier
(Laboratoire IBISC, Université d'Evry-Val d'Essonne)
Hanna Klaudel
(Laboratoire IBISC, Université d'Evry-Val d'Essonne)
Raymond Devillers
(Département d'Informatique, Université Libre de Bruxelles)
Artur Rataj
(Institute of Theoretical and Applied Computer Science)

MIRELA is a high-level language and a rapid prototyping framework dedicated to systems where virtual and digital objects coexist in the same environment and interact in real time. Its semantics is given in the form of networks of timed automata, which can be checked using symbolic methods. This paper shows how to detect various kinds of indefinite waitings in the components of such systems. The method is experimented using the PRISM model checker.

In Jun Pang, Yang Liu and Sjouke Mauw: Proceedings 4th International Workshop on Engineering Safety and Security Systems (ESSS 2015), Oslo, Norway, June 22, 2015, Electronic Proceedings in Theoretical Computer Science 184, pp. 5–18.
Published: 10th June 2015.

ArXived at: http://dx.doi.org/10.4204/EPTCS.184.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org