The MIRELA framework: modeling and analyzing mixed reality applications using timed automata

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.

Modeling Calcium Concentration and Biochemical Reactions

Almost all regions of the brain receive one or more neuromodulatory inputs, and disrupting these inputs produces deficits in neuronal function. Neuromodulators act through intracellular second messenger pathways to influence the electrical properties of neurons, integration of synaptic inputs, spatio-temporal firing dynamics of neuronal networks, and, ultimately, systems behavior. Second messengers pathways consist of series of bimolecular reactions, enzymatic reactions, and diffusion. Calcium is the second messenger molecule with the most effectors, and thus is highly regulated by buffers, pumps and intracellular stores. Computational modeling provides an innovative, yet practical method to evaluate the spatial extent, time course and interaction among second messenger pathways, and the interaction of second messengers with neuron electrical properties. These processes occur both in compartments where the number of molecules are large enough to describe reactions deterministically (e.g. cell body), and in compartments where the number of molecules is small enough that reactions occur stochastically (e.g. spines). – In this tutorial, I explain how to develop models of second messenger pathways and calcium dynamics. The first part of the tutorial explains the equations used to model bimolecular reactions, enzyme reactions, calcium release channels, calcium pumps and diffusion. The second part explains some of the GENESIS, Kinetikit and Chemesis objects that implement the appropriate equations. In depth explanation of calcium and second messenger models is provided by reviewing code, both in XPP, Chemesis and Kinetikit, that implements simple models of calcium dynamics and second messenger cascades.