Indefinite waitings in MIRELA systems
Software Engineering
2015-06-12 v1 Logic in Computer Science
Abstract
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.
Cite
@article{arxiv.1506.03553,
title = {Indefinite waitings in MIRELA systems},
author = {Johan Arcile and Jean-Yves Didier and Hanna Klaudel and Raymond Devillers and Artur Rataj},
journal= {arXiv preprint arXiv:1506.03553},
year = {2015}
}
Comments
In Proceedings ESSS 2015, arXiv:1506.03250