Indefinite waitings in MIRELA systems
This addresses a specific issue in real-time mixed-reality systems, but it appears incremental as it applies existing model-checking techniques to a particular framework.
The paper tackled the problem of detecting indefinite waitings in MIRELA systems, which are used for virtual and digital object interactions, by applying symbolic methods with the PRISM model checker, but no concrete numerical results were provided.
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.