Home / Issues / 6.2009 / The MIRELA framework: modeling and analyzing mixed reality applications using timed automata
Document Actions

Citation and metadata

Back to the article.

Recommended citation

Jean-Yves Didier, Bachir Djafri, and Hanna Klaudel, The MIRELA framework: modeling and analyzing mixed reality applications using timed automata. JVRB - Journal of Virtual Reality and Broadcasting, 6(2009), no. 1. (urn:nbn:de:0009-6-17423)

Download Citation

Endnote

%0 Journal Article
%T The MIRELA framework: modeling and analyzing mixed reality applications using timed automata
%A Didier, Jean-Yves
%A Djafri, Bachir
%A Klaudel, Hanna
%J JVRB - Journal of Virtual Reality and Broadcasting
%D 2009
%V 6(2009)
%N 1
%@ 1860-2037
%F didier2009
%X 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.
%L 004
%K Mixed reality systems modeling
%K formal analysis
%K model-checking
%K realtime
%K simulation
%K timed automata
%R 10.20385/1860-2037/6.2009.1
%U http://nbn-resolving.de/urn:nbn:de:0009-6-17423
%U http://dx.doi.org/10.20385/1860-2037/6.2009.1
Download

Bibtex

@Article{didier2009,
  author = 	"Didier, Jean-Yves
		and Djafri, Bachir
		and Klaudel, Hanna",
  title = 	"The MIRELA framework: modeling and analyzing mixed reality applications using timed automata",
  journal = 	"JVRB - Journal of Virtual Reality and Broadcasting",
  year = 	"2009",
  volume = 	"6(2009)",
  number = 	"1",
  keywords = 	"Mixed reality systems modeling; formal analysis; model-checking; realtime; simulation; timed automata",
  abstract = 	"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.",
  issn = 	"1860-2037",
  doi = 	"10.20385/1860-2037/6.2009.1",
  url = 	"http://nbn-resolving.de/urn:nbn:de:0009-6-17423"
}
Download

RIS

TY  - JOUR
AU  - Didier, Jean-Yves
AU  - Djafri, Bachir
AU  - Klaudel, Hanna
PY  - 2009
DA  - 2009//
TI  - The MIRELA framework: modeling and analyzing mixed reality applications using timed automata
JO  - JVRB - Journal of Virtual Reality and Broadcasting
VL  - 6(2009)
IS  - 1
KW  - Mixed reality systems modeling
KW  - formal analysis
KW  - model-checking
KW  - realtime
KW  - simulation
KW  - 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.
SN  - 1860-2037
UR  - http://nbn-resolving.de/urn:nbn:de:0009-6-17423
DO  - 10.20385/1860-2037/6.2009.1
ID  - didier2009
ER  -
Download

Wordbib

<?xml version="1.0" encoding="UTF-8"?>
<b:Sources SelectedStyle="" xmlns:b="http://schemas.openxmlformats.org/officeDocument/2006/bibliography"  xmlns="http://schemas.openxmlformats.org/officeDocument/2006/bibliography" >
<b:Source>
<b:Tag>didier2009</b:Tag>
<b:SourceType>ArticleInAPeriodical</b:SourceType>
<b:Year>2009</b:Year>
<b:PeriodicalTitle>JVRB - Journal of Virtual Reality and Broadcasting</b:PeriodicalTitle>
<b:Volume>6(2009)</b:Volume>
<b:Issue>1</b:Issue>
<b:Url>http://nbn-resolving.de/urn:nbn:de:0009-6-17423</b:Url>
<b:Url>http://dx.doi.org/10.20385/1860-2037/6.2009.1</b:Url>
<b:Author>
<b:Author><b:NameList>
<b:Person><b:Last>Didier</b:Last><b:First>Jean-Yves</b:First></b:Person>
<b:Person><b:Last>Djafri</b:Last><b:First>Bachir</b:First></b:Person>
<b:Person><b:Last>Klaudel</b:Last><b:First>Hanna</b:First></b:Person>
</b:NameList></b:Author>
</b:Author>
<b:Title>The MIRELA framework: modeling and analyzing mixed reality applications using timed automata</b:Title>
<b:Comments>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.</b:Comments>
</b:Source>
</b:Sources>
Download

ISI

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
Download

Mods

<mods>
  <titleInfo>
    <title>The MIRELA framework: modeling and analyzing mixed reality applications using timed automata</title>
  </titleInfo>
  <name type="personal">
    <namePart type="family">Didier</namePart>
    <namePart type="given">Jean-Yves</namePart>
  </name>
  <name type="personal">
    <namePart type="family">Djafri</namePart>
    <namePart type="given">Bachir</namePart>
  </name>
  <name type="personal">
    <namePart type="family">Klaudel</namePart>
    <namePart type="given">Hanna</namePart>
  </name>
  <abstract>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.</abstract>
  <subject>
    <topic>Mixed reality systems modeling</topic>
    <topic>formal analysis</topic>
    <topic>model-checking</topic>
    <topic>realtime</topic>
    <topic>simulation</topic>
    <topic>timed automata</topic>
  </subject>
  <classification authority="ddc">004</classification>
  <relatedItem type="host">
    <genre authority="marcgt">periodical</genre>
    <genre>academic journal</genre>
    <titleInfo>
      <title>JVRB - Journal of Virtual Reality and Broadcasting</title>
    </titleInfo>
    <part>
      <detail type="volume">
        <number>6(2009)</number>
      </detail>
      <detail type="issue">
        <number>1</number>
      </detail>
      <date>2009</date>
    </part>
  </relatedItem>
  <identifier type="issn">1860-2037</identifier>
  <identifier type="urn">urn:nbn:de:0009-6-17423</identifier>
  <identifier type="doi">10.20385/1860-2037/6.2009.1</identifier>
  <identifier type="uri">http://nbn-resolving.de/urn:nbn:de:0009-6-17423</identifier>
  <identifier type="citekey">didier2009</identifier>
</mods>
Download

Full Metadata

Bibliographic Citation JVRB, 6(2009), no. 1.
Title

The MIRELA framework: modeling and analyzing mixed reality applications using timed automata (eng)
Author Jean-Yves Didier, Bachir Djafri, Hanna Klaudel
Language eng
Abstract 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.
Subject Mixed reality systems modeling, formal analysis, model-checking, realtime, simulation, timed automata
Classified Subjects
swd
  • 4148259-1, Simulation
  • 4713349-1, Timed automata
  • 4560202-5, Mixed Reality
DDC 004
Rights DPPL
URN: urn:nbn:de:0009-6-17423
DOI https://doi.org/10.20385/1860-2037/6.2009.1