摘要：Mixed Reality (MR) aims to link virtual entities with
the real world and has many applications such as military
and medical domains [JBL+00, NFB07]. In many
MR systems and more precisely in augmented scenes,
one needs the application to render the virtual part accurately
at the right time. To achieve this, such systems
acquire data related to the real world from a set
of sensors before rendering virtual entities. A suitable
system architecture should minimize the delays to
keep the overall system delay (also called end-to-end
latency) within the requirements for real-time performance.
In this context, we propose a compositional
modeling framework for MR software architectures in
order to specify, simulate and validate formally the
time constraints of such systems. Our approach is first
based on a functional decomposition of such systems
into generic components. The obtained elements as
well as their typical interactions give rise to generic
representations in terms of timed automata. A whole
system is then obtained as a composition of such defined components.
To write specifications, a textual language named
MIRELA (MIxed REality LAnguage) is proposed
along with the corresponding compilation tools. The
generated output contains timed automata in UPPAAL
format for simulation and verification of time constraints.
These automata may also be used to generate
source code skeletons for an implementation on a MR
platform.
The approach is illustrated first on a small example.
A realistic case study is also developed. It is modeled
by several timed automata synchronizing through
channels and including a large number of time constraints.
Both systems have been simulated in UPPAAL
and checked against the required behavioral
properties.
关键词：Mixed reality systems modeling;formal analysis;model-checking;realtime;simulation;timed automata
Loading...
