PT Journal
AU Didier, J
   Djafri, B
   Klaudel, H
TI The MIRELA framework: modeling and analyzing mixed reality applications using timed automata
SO JVRB - Journal of Virtual Reality and Broadcasting
PY 2009
VL 6(2009)
IS 1
DI 10.20385/1860-2037/6.2009.1
DE Mixed reality systems modeling; formal analysis; model-checking; realtime; simulation; timed automata
AB Mixed Reality (MR) aims to link virtual entities withthe real world and has many applications such as militaryand medical domains [JBL+00, NFB07]. In manyMR systems and more precisely in augmented scenes,one needs the application to render the virtual part accuratelyat the right time. To achieve this, such systemsacquire data related to the real world from a setof sensors before rendering virtual entities. A suitablesystem architecture should minimize the delays tokeep the overall system delay (also called end-to-endlatency) within the requirements for real-time performance.In this context, we propose a compositionalmodeling framework for MR software architectures inorder to specify, simulate and validate formally thetime constraints of such systems. Our approach is firstbased on a functional decomposition of such systemsinto generic components. The obtained elements aswell as their typical interactions give rise to genericrepresentations in terms of timed automata. A wholesystem is then obtained as a composition of such defined components.To write specifications, a textual language namedMIRELA (MIxed REality LAnguage) is proposedalong with the corresponding compilation tools. Thegenerated output contains timed automata in UPPAALformat for simulation and verification of time constraints.These automata may also be used to generatesource code skeletons for an implementation on a MRplatform.The approach is illustrated first on a small example.A realistic case study is also developed. It is modeledby several timed automata synchronizing throughchannels and including a large number of time constraints.Both systems have been simulated in UPPAALand checked against the required behavioralproperties.
ER