Software modeling as networked, certified components
In order to master the complexity of today's software systems, a software architecture is often complemented by product functions. These product functions are implemented by e.g. state-machines or MatLab/SimuLink models. The advantages of this approach are the simple implementation of even complicated, non-linear functions with many operating modes, high flexibility and easy modifiability. The downside is the unimaginably high number of unknown and undesirable states that such state machines or MatLab/SimuLink models can assume. According to a 2007 MIT study, even systems with relatively simple functions, such as a Traffic Collision Avoidance System (TCAS), can reach up to 10^40 states. Modern engine control units easily reach more than 10^120 states.
The "Contract Based Design (CBD)" method provides a solution to this problem. In contrast to analytical Model-Based Development, the CBD methodology is synthetic. In this approach, a system is built up of components with interfaces whose components have inputs and outputs. Contracts provide constraints on input and output relations thus imposing that the components communicate correctly, thus limiting the number of undesired states of the whole system. In other workds, CBD guarantees that the properties and states of the components involved in the system become limited and thus manageable.
eTrice is a mature open-source model-based software engineering tool, based on the ROOM methodology and developed by Protos GmbH (who are project partners). It is currently used in the industry for the development of solutions for domains such as health, heavy machinery and the automotive. eTrice natively incorporates mechanisms for runtime verification. At the request of the developers of eTrice, fortiss has incorporated model checking in their tool chain.
The results of this research are very promising for Protos and its business. We have shown with a real-world example that important properties of a system can be checked on eTrice specifications while not intruding whatsoever in the currently existing specification language. Because of our work, properties that could not be proved with Rv can now be checked in eTrice specifications. Additionally, model checking allows doing so efficiently, at design time and covering corner cases that might occur very sparsely in practice. Our experience leads us to believe that the CBD approach might be extended to other development environments in an affordable fashion.