by Jan Friso Groote
Can a car drive faster than the speed limit the cruise control indicates? Are computerised protocols between planes and air traffic control safe? Communication between software components in cars, planes and other intelligent embedded systems is often very complex and prone to errors. The Design and Analysis of Systems group at Eindhoven University of Technology is releasing a new toolset, mCRL2, to improve the quality of embedded system design.
An embedded system can roughly be described as some piece of equipment with one or more computer processors in it. The processor allows this equipment to behave with an amazing level of intelligence. Copiers order their own paper and cars actively avoid accidents. The end of this is not in sight. The behaviour of such systems will become far more advanced than it is today.
The downside of this is that the behaviour of systems becomes so complex that we cannot easily understand it anymore. As a consequence, most features of contemporary equipment remain unused. But it is even worse. Because the system components are exhibiting more and more complex behaviour, they do not always understand each other. The consequence is that intelligent systems often behave erraticly. For modern TV sets a 'misunderstanding' between the components occurs every minute in each television. Much effort goes into building internal firewalls to restrain these flaws so they are not noticed by those watching TV.
Now that the behaviour of systems is becoming so complex, it has become an important research topic. Just as in other engineering disciplines, complexity is tackled by making models. These behavioural models describe the potential behaviour of the system, ie which interactions can take place when. Typical examples are sending messages, pressing buttons, activating actuators and reading sensors. Questions that must be answered are: are all messages properly processed; can a car ever be instructed to drive faster than the speed limit of the cruise control; does a copier always order paper in time or is it possible that it orders twice the amount needed due to message duplication?
The major challenge to answering such questions is the 'state space explosion'. Even relatively simple behavioural models give rise to millions of states. In order to show that a system behaves correctly, all these states must be investigated. It goes without saying that analysis tools are essential here. It is impossible to carry out the analysis of an industrial behavioural model by hand, but manual manipulation and human insight is also essential to reduce it to a manageable size.
At Eindhoven University of Technology, in close cooperation with CWI in Amsterdam, we are developing a mathematical methodology accompanied with tools to model and analyse the (discrete) behaviour of embedded systems. The method is called mCRL2, where CRL stands for Common Representation Language. The methodology is based on process algebra, extended with data types. The method has been applied to almost all major embedded system industries within the Netherlands. Furthermore, it is being taught at several universities.
The major idea underlying the methodology is to transform each model to a normal form, a so called linear process. Due to its simple structure, a linear process is very amenable to symbolic manipulation and simplification. For instance, by detecting confluent behaviour in a linear process, the associated state space is often exponentially smaller than without the use of confluence. Experience has shown that all models can straightforwardly be translated to linear form. Unfortunately, not every form of analysis can be carried out on linear processes. For this state automata are needed, but these can not always be generated.
Besides the analysis tools, the toolset comes with several visualisation tools. In particular, tools that can visualise the structure of state spaces of up to a million states are very helpful in obtaining an insight into the behaviour of embedded systems. These techniques have been used more than once to detect symmetric or erroneous behaviour. They have also been very helpful in understanding the extent of problematic behaviour compared with the overall behaviour.
The tools and techniques are being developed in the scientific domain. This not only means that the ideas and technologies being used are published within the scientific community (as is common), but also that the tools are an open source, free for both scientific and commercial use. A preliminary version of the toolset can be found at www.mcrl2.org. A full first release is expected in the autumn of 2006 and will be available for Linux, Mac OS X and Windows. It will contain all available modelling, analysis and visualisation tools.
Please contact:
Jan Friso Groote, Eindhoven University of Technology, The Netherlands
Tel: +31 40 2475003
E-mail: jfg
win.tue.nl
http://www.win.tue.nl/~jfg
