Software Components for Embedded Control Systems

PhD: John Knudsen

 Casestory

1. Purpose of the Project
This PhD. research project aims to address the verification of embedded control systems. By considering the architecture of a control system as a component systems concepts for validating architectures and for verifying component based systems will be merged to form a set of verification rules. In order to refine and test the verification rules, the concepts of the research are applied in an industrial case study.

2. Perspective
In the past decade embedded systems have become a substantial part of industrial production and personal equipment. As the available resource of such systems have increased so has the demand of complex and even critical systems. As correctness and dependability of the embedded systems is a major issue, methods to ensure these properties becomes essential.

Embedded software has typically, due to the restrictions imposed by hardware, been relatively small programs controlling and monitoring simple devices. As more resources become available, because the hardware has evolved, larger systems are possible. That challenges developers: Issues such as maintainability and reusability that have been addressed in other software development practices becomes interesting in this field as well. Furthermore, as the systems become more complex, the validation becomes a major issue. These problems are essentially addressed by providing more structure information for the software and by using higher level programming that reduces program size. Thus UML and Object Oriented methods, that are focused on these issues, are considered. A related topic is reuse of software, thus Component Based Development is becoming interesting for the community of embedded software developers. The proposed research project aim to address key issues in this field:

• Architecture pattern(s).
• Verification rules for control software architectures.
• The project furthermore demonstrates the concepts applied to maritime diesel engine control systems.

Sections 2.2 and 2.3 give an introduction to these topics after the introduction of Component Based Development in Section 2.1. In Section 3 the subject of the experiments and the empirical framework is presented.

2.1 Component Based Development(CBD)
The vision of component based development is a market where small independent solutions, software and hardware, are sold as components that can be composed to form larger software systems. Although component enabled frameworks have been available for some years, a well formed theory on the subject still remains to be formulated. The research community yet have to establish clear formal definitions of components, address topics of composability and develop tools supporting development of systems using components and other. Most definitions of components are derived from the work of Szyperski[Szy97]. According to Szyperski a component is

a unit of composition with contractually specified interfaces and fully explicit context dependencies that can be deployed independently and is a subject to third party composition.

This definition fits well the common perception of architectures as they describe a system as a composition of subsystems and their dependencies. That the proposed architecture is in accordance with this definition is essential to the verification of it, which means that each component specified in the case study must have a clear syntactic and, if possible, functional interface to allow composition with other components and an elaborate specification to enable third party composition. The specification could be the subject of verification, provided that it is of proper format.

This is as mentioned a major topic for researchers around the world. A large European contribution is the work of ARTIST, a network of researchers addressing advanced topics of real-time systems and component based development for embedded systems and the work of this group is presented in a collection of contributions from prominent researchers of the fields: the Roadmap[BCC+04]. The Roadmap addresses research challenges with in 3 fields related to embedded software development: Hard Real-Time Development Environments, Component Based Design and Integration Platforms and Adaptive Real-Time Systems for Quality of Service Management. As the topic of this project is Software Components for Embedded Systems the main inspiration will be from the part covering component based design, however, the subject of the case study is of such a nature that the other parts can not be entirely ignored. An interesting contribution to this comminity regarding composition of components is the Interface Automata of Alfaro and Henzinger [dAH01].

2.2 Architecture Pattern(s)
Providing a template for the a software design as an architecture is common for control systems as well for other types of systems. The general concepts of a control system can be described as: monitoring and controlling a plant, where sensors provide input from the plant to the controls, who in turn calculate the next state of actuators, that are capable of driving the plant to a desired state. The most interesting architectures for this project are the Reactive Architecture[Bro86,Bro91] and the Three Layered Architecture[Gat97].

2.3 Architecture Verification Rules
Validating, i.e. ensuring software correctness and system dependability is still a research challenge. The industrial efforts to accomplish better software has recently been improving the development process by implementing more disciplined testing procedures. A few companies have and are trying to verify their software through more formal verification methods.

Formal verification of software primarily remains an academic task as the human resources capable of applying these methods are scarce and the methods themselves struggle with lack of computational resources due to the state space explosion. Several methods have been put forth in order to make formal verification more tractable by automating the verification of preset general properties such as reachability and deadlock. A recent, yet unpublished, work [DHO03] is an interesting contribution to this field. In [DHO03] an approach building on component based development exploits that components are themselves independent pieces of software by verifying the components separately and then devise rules for verifying their composition. This could prove to be an interesting result for the component based community as it could support incremental development of components systems. If an additional component is needed to a composition in order to satisfy the requirement and the composition as well as the new component are already verified then only their composition needs verification.

In verification of software systems the interesting properties are usually considered to be safety, liveness, bounded liveness and deadlock freeness, but as the subject of the case study is a control system properties observability, controllability, stability and optimality must be considered as well.

In my research I will try to follow the lines of [DHO03] and construct rules that can be applied to verify the properties that are of general interest. Along with this I will try to consider the 60 criteria of [Lev97] and their relationship to the property classes and the rules of the particular patterns.

3. Industrial Application
During the development phase of my study, appropriate methods are to be implemented as a control system for maritime diesel engines. The subject of the case study is the control system of MAN B&W a market leader in the field of big maritime diesel engines. To acquire the needed domain knowledge their current control system and requirement specifications are analyzed. During this work key components should be derived and an elaborated architecture of a control system will be devised based on these components and suggested architecture.

4. Bibliography

[BCC+04]	Ed Brinksma, Geoff Coulson, Ivica Crnkovic, Andy Evans, S´ebastien G´erard, Susanne Graf, Holger Hermanns, Jean-Marc J´ez´equel, Bengt Jonsson, Anders Ravn, Philippe Schnoebelen, Francois Terrier, and Angelika Votintseva. Selected topics in embedded systems design: Roadmaps for research. Technical report, ARTIST, 2004.
[Bro86]	Rodney A. Brooks. A robust layered control system for a mobile robot. IEEE Journal of Robotics and Automation, RA-2, No1:14–23, 1986.
[Bro91]	Rodney A. Brooks. New approaches to robotics. Science, 253:1227–1232, 1991.
[dAH01]	Luca de Alfaro and Thomas A. Henzinger. Interface automata. In In Proc. of the 8th European Software Engineering Conf., pages 109–120, 2001.
[DHO03]	Werner Damm, Hardi Hungar, and Ernst-Rdiger Olderog. On the veri?cation of cooperating traffc agents. In FMCO, 2003.
[Gat97]	Erann Gat. On three-layer architectures. In D. Kortenkamp, R. P. Bonnasso, and R. Murphy, editors, Artificial Intelligence and Mobile Robots. MIT/AAAI Press, 1997.
[Lev97]	N. Leveson. Analyzing software speci?cations for mode confusion potential, 1997.
[Szy97]	Clemens Szyperski. Component software, beyond object-oriented programming. Addison-Wesley, 1997.