by Alexandre David and Brian Nielsen
Model-driven development (MDD) has an enormous potential for improving verification, testing and synthesis of embedded systems. Our UPPAAL tool-suite for MDD of embedded real-time systems has recently been extended with components for automatic test generation and code synthesis. Presentation and demonstration at a European industrial conference on Systematic Testing spawned a lot of interest in these new techniques.
Our research centre was recently invited to participate in an industrial gathering on 'Systematic Testing' of embedded systems in Berlin, together with approximately eighty industrial participants from various sectors all over Europe ranging from the automotive industry, avionics, control systems and consumer electronics. It was observed that although these sectors vary in their technical intricacies and level of safety and reliability requirements, many common challenges exist. These include the ever-increasing size and complexity of software, demands for reduced time to market, and rapid changes in technology. At the same time we observed a change in attitude reflecting a decreased tolerance for errors, even towards zero-defects. This is also true of sectors beyond conventional safety-critical software. It is no longer accepted that systems will 'by nature' contain a certain number of errors and that the purpose of testing is to eliminate the worst of them. Quality systems are not allowed to misbehave, and certainly not in any way that users would notice. In combination, these developments make conventional quality assurance and testing techniques ineffective and too expensive.
MDD is a promising approach that will contribute significantly to solving these challenges by enabling early model analysis (via simulation and model checking, for example) and design space exploration. Furthermore, model-based testing allows the test engineer to focus on the intellectual challenge of specifying and modelling the behaviour of interest at a high level of abstraction, rather than on manual test-case design, laborious scripting and manual test execution. Using model-based testing, a test generation tool generates an appropriate set of test cases and lets a test automatically execute these.
In the academic world, UPPAAL is a well-known and widely used model-checking tool for real-time systems. It is jointly developed by Aalborg University, Denmark, and Uppsala University, Sweden. The behaviour of timed systems is graphically modelled using the timed automata formalism extended with various modelling features such as concurrency and C-like functions and data structures, to make it practically expressive and user-friendly. UPPAAL contains a graphical editor and animator/simulator, and an efficient model-checker. The latter performs an exhaustive symbolic analysis of the model and provides either a proof that the model satisfies a property, or a counter-example consisting of a trace of actions and delays exemplifying how the property is violated. It has been applied successfully to numerous industrial cases.
UPPAAL was recently extended with components for test generation and controller synthesis. This is an important step towards the vision of being an integrated tool suite for MDD of embedded systems, where the entire development lifecycle - from specification to running code - is driven by successive refinements and iterations.
UPPAAL can now handle both online and offline test generation. Specifically, UPPAAL-TRON is an online tool for black-box conformance testing of real-time systems. In an online tool, test events are generated and executed simultaneously in real time, on the physical implementation being tested. A further verdict on the observed interaction sequences may also be made online. TRON has well-defined formal semantic and correctness criteria defining how a correct implementation should behave compared to the modelled behaviour. The tool implementation extends the efficient algorithms and data structures of the model-checker engine to enable real-time testing of many real-time systems. TRON is connected to the system under test via an adaptor component (defined by the user), translating physical I/O or signalling to the abstract events of the model. TRON has for example been applied to test an embedded refrigeration controller for industrial cooling plants.
UPPAAL-TIGA is an extension of UPPAAL used to solve two-player timed games. Its main application is for controller synthesis. In a timed game automata model, actions are partitioned as being either controllable or uncontrollable. The idea is to have a controller playing with controllable actions and an environment playing with uncontrollable actions. The model-checker tries to compute a so-called winning strategy that tells the controller which actions to take (and when) to ensure that a property holds, no matter what the environment does. The tool implements a state-of-the-art algorithm that computes such strategies on the fly, ie while exploring states. The tool, in combination with Matlab-Simulink, has been successfully used to generate executable code of a climate controller for pig stables. Recently it was also applied to generate an optimal controller for a hydraulic pump.
However, despite the relative maturity of these techniques more work is needed to integrate with industrial tool-chains like Matlab-Simulink or UML-based tools, to further scale the techniques and to deal with other quantitative constraints beyond real time.
Link:
http://www.uppaal.com/
Please contact:
Brian Nielsen
Centre of Embedded Software Systems, CISS
Aalborg University, Denmark
Tel: +45 9940 8883
E-mail: bnielsen
cs.aau.dk
