by Brian Nielsen
Existing Model-Driven Development (MDD) tools and methods for real-time embedded systems are rather poor at handling the relevant quantitative constraints. Quasimodo (Quantitative System Properties in Model-Driven Design of Embedded Systems) is a new EU FP7 project whose main goal is to extend current MDD techniques and tools for modelling, verification, testing and code generation with the ability to satisfy these quantitative constraints.
A key characteristic of embedded systems is that they must meet a multitude of quantitative constraints. These involve the resources that a system may use (computation resources, power consumption, memory usage, communication bandwidth, costs etc), assumptions about the environment in which it operates (arrival rates, hybrid behaviour), and requirements on the services that the system must provide (timing constraints, quality of service, availability, fault tolerance etc). Existing MDD tools for real-time embedded systems are quite sophisticated in their handling of functional requirements, but their treatment of quantitative constraints is still very limited. Hence MDD will not realize its full potential in the embedded systems area unless the ability to handle quantitative properties is drastically improved.
To focus on aspects central to embedded systems such as performance, timeliness and efficient usage of resources, the models must provide quantitative information on timing, cost, data, stochastics and hybrid phenomena. A challenge is to develop notations that are expressive, have precise formal semantics, and that can be analysed efficiently by automated tools. Quasimodo mostly works with probabilistic, priced, timed game automata and looks at how to link these to industrial tool chains.
The analysis methods developed in Quasimodo include data structures for symbolic exploration of the behaviour of models, abstraction and compositionality principles that relate design models and help to control the size and complexity of the models, exploitation of approximate analysis techniques for partial analysis of very complex models and, orthogonally, optimal utilization of the given computing platform on which the algorithms are implemented.
In the implementation step, executable code running on given physical devices must be provided. While the theoretical framework of the quantitative models assumes infinitely fast hardware, infinitely precise clocks, unbounded memory and so on, real CPUs are subject to hard limitations in terms of frequency and memory size. Being able to guarantee that properties established by a given model are also valid in its implementation is therefore a major challenge.
Current industrial testing is often manual and without effective automation, and consequently is rather error prone and costly: it is estimated that 30-70% of the total development cost is related to testing. Model-based testing is a novel approach to testing with significant potential to improve both cost and efficiency. We intend to extend the model-based testing technology to the setting of quantitative models, allowing generation, selection, execution and provision of coverage measures to be made. Another challenge, similar to implementation synthesis, is to develop a sound and theoretically well-founded framework and tools for testing quantitative systems when these quantities (eg timing) cannot be observed and controlled accurately.
In order to demonstrate the usefulness of our techniques, we will apply them to several complex industrial case studies and provide a collection of unique tool components to be used as plug-ins in industrial tools or tool chains like Matlab/Simulink.
One case study concerns a controller for an oil accumulator system for a hydraulic pump.
The controller must maintain the gas pressure in the bladder within a safe pressure range, and should be robust against fluctuations in the energy consumption of the machine. The goal is then to find an optimal controller that minimizes the (long-term) energy consumption. Our approach consists of modelling the accumulator system as timed game automata in our game-solving tool Uppaal Tiga, and using this to automatically synthesize the optimal controller. We have produced a controller that has a 40% gain compared to classical controllers.
A second case concerns the modelling and analysis of medium-level access protocols for a specific type of sensor network. The interesting properties of the network will be modelled as probabilistic (timed) automata and linearly priced timed automata, and our model checking techniques and tools will be used to determine important system properties like collision-freeness, transmission rate and energy consumption.
Quasimodo will also model, analyse and test the application software for the Attitude Control Computer for the Hershel/Planck satellites. In particular we will evaluate the techniques for model-based online real-time testing. This work will include producing timed automata models of central aspects of both the control software and its environment, to ensure that only feasible and realistic tests are generated. Moreover, to facilitate automatic execution, test adaptation software will need to be developed to allow successful translation between abstract-model events and concrete messages to be sent/received from the system under test.
Partners in the project are Aalborg University, Denmark (coordinator); Embedded Systems Institute, the Netherlands; RWTH Aachen University, Germany; Universität des Saarlandes, Germany; Université Libre de Bruxelles, Belgium; ENS-Cachan/CNRS, France; Terma A/S, Denmark; Hydac GmbH, Germany; and Chess Beheer B.V, the Netherlands. The total budget is 2 696 000 and the project, which started in January 2008, will have a duration of 36 months.
Link:
http://www.quasimodo.aau.dk
Please contact:
Brian Nielsen
Centre of Embedded Software Systems, CISS
Aalborg University, Denmark
Tel: +45 9940 8883
E-mail: bnielsen
cs.aau.dk
