Indefinite waitings in MIRELA systems
Johan Arcile (Laboratoire IBISC, Universit\'e d'Evry-Val d'Essonne),, Jean-Yves Didier (Laboratoire IBISC, Universit\'e d'Evry-Val d'Essonne),, Hanna Klaudel (Laboratoire IBISC, Universit\'e d'Evry-Val d'Essonne), Raymond, Devillers (D\'epartement d'Informatique
TL;DR
This paper presents a method to detect indefinite waitings in MIRELA systems, which combine virtual and digital objects, using symbolic analysis and the PRISM model checker.
Contribution
It introduces a novel approach for identifying indefinite waitings in MIRELA components through formal verification techniques.
Findings
Effective detection of indefinite waitings demonstrated
Method successfully applied using PRISM model checker
Enhances reliability of MIRELA-based systems
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.