by Michal Pluska and David Sinclair
Embedded systems that interact with the physical world should be designed with a high degree of safety. In most existing design approaches that deal with such systems, verification is done afterwards and may lead to redesign problems. Moreover verification is done by simulation which may not consider the whole spectrum of system operation. The Lero – Irish Software Engineering Research Centre work at the Dublin City University introduces a methodology that helps design systems that can be verified by formal methods and according to system requirements. Moreover it helps partition the system into the objects from which it is built.
Hybrid systems are built as a combination of computational systems and real-world physical parts. The computational parts can be seen as one or more embedded computers connected by a network and interacting with the physical world via sensors and actuators, with control engineering techniques helping to coordinate this set-up. The computational part of the system is therefore affected by the real-world physical part; moreover, it has to deal with the real-time properties of the physical world. In addition, hybrid systems can be seen as a group of cooperating devices of which the computing device is only one; on the other hand, it may be the one that is responsible for coordinating the whole system and ensuring it works as intended.
The complexity of hybrid systems makes the design a very challenging issue. Obtaining the correct design can be problematic, and extensive testing of various prototypes may be necessary. Unfortunately this can raise the design costs and the time required to finish it. The other problem to tackle during the design is correctness of the system. This problem is addressed with a design methodology using formal methods for verification of the system in the design.
Most widespread approaches to hybrid system design and later verification reassemble the bottom-up design methodology. The work begins with information about the system gathered in the form of physical rules and equations. Objects in the design are related to physical objects of the system and the interactions between them are made according to the physical equations. Those interactions can also be described as an agent-based approach to the description of a system. This bottom-up methodology is focused on detailed description and its relevance to the physical world. Describing the system from the beginning of the design may lead to too many detailed equations in the initial stage. This is clearly visible with large systems described by many physical laws. Currently abstraction of those systems, useful during design, is possible only by using less realistic physical equations. Moreover there is no established rule for keeping track of the changes. Every case is explored individually with different levels of abstraction, and its solution is found by numerous experiments. The number of considered details can be problematic for the design engineer and can easily be a cause of error.
System design by this approach is verified by numerous simulations. The aim of simulation is to avoid extensive testing after the manufacture and hence reduce the cost and time. Unfortunately the degree of confidence in the correctness of the simulated design may be limited. The main cause of this is that too large a set of input data will cause unpredicted interactions with the environment that are impossible to check. Building a prototype of the system suffers from identical problems as the system complexity rises.
In comparison, formally verifying high-level designs of complex systems can be very useful for hybrid systems, many of which are safety critical. By building a formal mathematical model of the system it is possible to use automated model-checking methods to prove that all requirements are met or all possible system input sequences are checked. Simulations only allow some of the potential system inputs to be checked.
On the other hand, the usefulness of formal methods is limited by the lack of a well-defined methodology that would make it broadly applicable. There are no tools for interactive model building and analysis interpretation. Moreover the complexity of the system in design can be overcome by using appropriate abstraction of model’s details what is currently not supported at all. There is also a need for aids to translate informal requirements specifications into formal specifications. A final aspect worth mentioning is that formal methods specification and verification might be problematic for practical engineers, because their focus during design is on different aspects.
Figure 1: The proposed modelling and verification of the hybrid system.
The proposed modelling and verification of the hybrid system is divided into stages (see Figure 1). This partitioning allows the correct complex system to be built from the start and avoids problems which otherwise would only be found after the initial design is complete. Our design methodology is focused on describing the system requirements by examples of its usage in use cases. It allows verification of the gathered requirements and represents a starting point for the analysis. The analysis of those objects will hierarchically decompose them according to the abstraction levels that build the system model. This is done with respect to the abstraction level boundaries. This stage of the methodology design system model has all the features described in the requirements and is a backbone of the model used in the system verification process. All the necessary information is gathered during the design of the system model. The final verification of the system and the possible parameters of the system is done by a hybrid automaton. This approach builds and verifies the system model independently of the hardware. This makes it possible to use control software already verified on a different hardware platform, depending on the needs of engineers.
This work was supported, in part, by Science Foundation Ireland grant 03/CE2/I303_1 to Lero - the Irish Software Engineering Research Centre (http://www.lero.ie)
Please contact:
Michal Pluska
Dublin City University, Ireland
E-mail:
