EN 
DE What matters and what it brings: a practical example
Author: Georg Rößler, peiker acustic GmbH & Co. KG, Valeo peiker Telematics
Contribution – Embedded Software Engineering Congress 2016
The advantages of model-based software engineering (MBSE) have been widely described. Nevertheless, the method is less widespread than one might expect because there are some hurdles to overcome when getting started. Often, new products are developed based on an existing system with conventionally developed software. Furthermore, the client frequently expects certain functions to be demonstrated early on and extended during development.
This article uses the example of a telematics control unit for emergency calls in cars to demonstrate how these difficulties can be overcome. New functions are developed using a model-based approach, generating code from the state machines of the UML model. The methodology is designed to ensure that the new functions can be easily integrated into the existing system. The second part of the article describes how state machines can be generated using the tool [tool name missing in original text]. Spin They can be checked for correctness through simulation and formal verification.
Control unit for ERA-GLONASS emergency call
The project's objective was to develop an emergency call control unit for cars, compliant with the ERA-GLONASS standards, for the Russian market. ERA-GLONASS is based on the standardized emergency call system in the EU (EU eCall), which has been mandatory in all newly registered vehicles in the EU since spring 2018. While ERA-GLONASS is compatible with EU eCall, it incorporates several additional specifications, which are left to the discretion of the respective car or telematics control unit manufacturers as defined in the EU standards. Figure 1 (see PDF) shows the ERA-GLONASS control unit with its external interfaces and connected units.
The control unit was implemented using a UMTS-NAD (Network Access Device), which could be reused from another control unit. The NAD already provided all basic functions such as telephony, SMS, and data connections, and a prototype implementation of EU eCall was available. A new module with its own microcontroller was developed to control the hardware interfaces. This microcontroller communicates with the application controller on the NAD via a serial interface and several dedicated hardware lines.
Code generation from the state machine
The option of developing the emergency call system according to the ERA-GLONASS standards based on the EU eCall prototype was quickly discarded because the end result was expected to be a poorly structured implementation with many "holes" (convoluted code). Instead, the new function was modeled using UML, and the code for its behavior was directly generated from the state machine in the model.
For code generation to be used effectively, two requirements must be met:
- The generated code must be easily integrated into an existing system. This often results in the requirement that the generated code must function without its own runtime environment because an unusual target environment is specified.
- When further developing the state machine, the generated code must be very easy to integrate. Otherwise, neither iterative development is possible, nor is it possible to quickly react to changing requirements or reliably correct errors.
An existing custom-developed code generator was used, which generates Java code from state machines. The existing functions for importing from UML and the internal representations remained unchanged. Only the generation of C code was reimplemented. The requirement was that files either be generated completely or created manually.
The concept for code generation is inspired by a load generator for telephone systems [1], which reads in SDL models after the program starts and implements the specified behavior. The solution relies on mapping the SDL models into data structures that are interpreted by a general flow controller. Instead of creating the data structures for the specific state machine at runtime, they are statically generated by the code generator.
With the simple state machine in Figure 2 (see PDFThe basic function for the emergency call could therefore be implemented early. This automated system with only 6 states processes 14 different triggers in 17 state transitions.
During development, functions were successively added and refined. With the test call required by ERA-GLONASS, another state was added, and the automaton processed 22 triggers in 34 transitions. For complete functionality, more complex error handling was added, primarily following connection interruptions or failed attempts. This increased the automaton to 9 states and 49 transitions, triggered by 25 different factors.
The control of the operating states was also newly implemented for the ERA-GLONASS control unit, and the behavior on the NAD was modeled in a second automaton, from which the code was directly generated.
Simulation of state machines in UML
Controlling operating states is a critical function in every emergency call control unit. On the one hand, the control unit must switch to a minimal power consumption mode when the car is at rest. On the other hand, it must remain active in the event of an emergency call, regardless of the vehicle's other status. Furthermore, the emergency call control unit must remain connected to the network for a certain period of time so that it remains reachable by the emergency call center for callbacks and instructions via SMS.
Because the triggers for state changes can arrive in any order, the correct functioning of the automaton must be ensured under all circumstances.
As a first step, simulating the state machine using a UML tool was tested. For the state machine's environment on the NAD, additional state machines were designed to generate triggers for the state machine under test. A state machine was designed for the car's triggers, generating the terminal signals. These signals are processed by a second state machine on the MCU, and relevant changes are translated into messages sent to the NAD, which are then processed by the state machine for the operating states.
In a model with these three state machines, individual processes could be manually executed. However, testing in automatic mode revealed that certain processes never occurred, even though they were possible. The reason for this behavior is likely that the number of state transitions for the neglected transitions was significantly larger than for those that actually occurred during automatic execution.
For the automata in the environment, random behavior could still be enforced by explicitly modeling random branching. However, this approach was insufficient for the interaction between the automaton under test and its environment. Some processes never occurred during the automated simulation, even though they were provided for and possible in the model.
Transfer of the state machines to Spin
For further verification of state machines, the tool Spin [2], [3] was subsequently used. This required the state machine NAD Lifecycle to be defined in the language for the operating states on the NAD as well as the surrounding state machines. Promela described, which uses Spin.
The entire model consists of six processes that interact with each other. Interaction mechanisms include spin rendezvous for the synchronous exchange of messages and channels with message buffers for asynchronous communication. Processes can also interact via shared variables.
Figure 3 (see PDFFigure 1 shows a model for investigating spin. Thin lines indicate synchronous interaction, thick lines asynchronous communication over channels with message buffers.
Promela's syntax resembles common programming languages, but with the important difference that non-deterministic behavior is possible. The following excerpt from the process mculifecycle This indicates that the control unit can be started by switching on the ignition or by pressing the emergency call button for a manual emergency call.
ONLY_MANUAL:
printf( “ MCU: ERA_ONLY_MANUAL “ );
/* no messages from the last cycle in the buffer */
assert( len(rpcNadMcu) == 0 );
do
:: atomic
{
(gIgnitionOn == true) ->
gIgnEnable = 3;
pMcuNadOn!NadPwrOn;
}
/* Start communication via serial interface */
mcuOpenAspConnection();
rpcMcuNad!sysmode, modeOn;
goto ERA_ON;
:: pEbttnMcu ? param ->
assert( param == true );
pMcuNadOn!NadPwrOn;
mcuOpenAspConnection();
rpcMcuNad!trgevt, EcallButton;
rpcMcuNad!sysmode, modeEcall;
goto ECALL;
:: ( gIgnEnable == 0 ) ->
gIgnEnable = 1;
od
In this state, the process offers both options for starting the system (gIgnitionOn, pEbttnMcu). If the other side peripheral process If only one branch is offered, the corresponding branch will be selected. peripheral process However, since both options are offered, one of them is randomly selected during the simulation. During verification, both options are evaluated in the state space.
While in reality it's virtually impossible to simultaneously turn on the ignition and press the emergency call button, this is easily accommodated in the Spin model. Spin doesn't care about the time individual steps take, but only the sequence in which they occur. All sequences that are theoretically possible within the model are accepted. In the example, therefore... peripheral process First turn on the ignition, then press the emergency call button, and finally in mculifecycle respond to one of the two offers.
As a third option in the shown excerpt, the credit for an ignition change (gIgnEnable) is renewed. This credit mechanism was introduced to ensure that the simulation actually stops in the event of deadlocks in the rest of the system; otherwise, the ignition would be switched on and off indefinitely in an unproductive loop.
Simulation and verification with Spin
The model was initially created without the emergency call function (without). ecallmanager and without nadrpcrec). For the vending machine nadlifecycle The conformity with the UML model used for code generation was verified through review. The automaton mculifecycle It was created according to the specification that was also used for the implementation.
Several problems arose during the initial simulations. These were indicated by jams or violations of assertions explicitly included in the model to uncover undesired behavior. The majority of the problems stemmed not from errors in the automata themselves, but from unsuitable or incomplete representations of spin. During this phase, various models for the timer's overrun time after ignition shutdown were also tested until the model with two flags (TimerActive; Timeout) was found to be suitable. This model closely resembles the implementation that uses a counter for the timer, which is decremented at a fixed rate.
The simulation with Spin is very efficient, allowing simulations with hundreds of millions of steps to be run in just a few minutes on a standard notebook running a Linux virtual machine. After these long simulations ran flawlessly, Spin was used in verification mode. In this mode, the entire state space is examined, and Spin uses various methods to solve or avoid the notorious problem of state space explosion.
Verification can uncover new problems because it also analyzes the state space for loops without progress. This reveals error cases such as a situation where only the ignition is switched.
After the simple model was successfully simulated and verified, the two processes for emergency calls were added. The message communication thus corresponds to the real system, in which messages from the serial line are distributed to the correct recipients based on their type.
Summary and recommendations
The article presented the development of an ERA-GLONASS control unit for in-car emergency calls, employing model-based software engineering for key new functions. The behavior for emergency calls and the control of operating states were modeled using state machines, from which the code for the processes was generated. Crucially, the state machines could be incrementally extended and corrected during development because the newly generated code could be integrated with minimal effort.
The resulting implementation worked flawlessly from the outset and remained absolutely stable and reliable even after numerous repetitions in system testing. Since the model and code were identical through design, questions about its behavior could be answered directly from the model.
This example demonstrates that even when developing based on an existing system, it is possible and worthwhile to develop new components using a model-based approach. The following procedure is recommended for implementation:
- Identify new features that are suitable for model-based software engineering.
- Select a code generator that suits the task and the target environment. It is important that newly generated code can be easily integrated.
- Develop selected new features from the outset using a model-based approach.
- Start with basic functions to test the procedure and the tools.
- Gradually add further functionality
Besides the manageable risk involved in transitioning to model-based development, this approach has the advantage that developers are gradually introduced to the new development methodology, making it easier to overcome any reservations.
In the second part, the simulation and formal verification of the state machine for controlling operating states with Spin were presented, and some special features of the method were discussed. Due to the abstraction, the behavioral descriptions in Spin are both quite compact and close enough to the implementation to allow for valid statements to be made about it.
Spin is a tool suitable for the formal verification of real-world systems, not just small examples. Therefore, anyone wanting to go beyond reviews and sophisticated tests when verifying state machines can use Spin to check their behavior through simulation and formal verification, thereby uncovering and resolving deadlocks, unprogressive cycles, and unwanted behavior directly within the model.
References
[1] T. Steinert, G. Rößler, „Generation of realistic signaling traffic in an ISDN load test system using SDL User Models,“ Proceedings of FORTE/PSTV 2000, Pisa.
[2] Spin website. https://spinroot.com/
[3] M. Ben-Ari, „A Primer on Model Checking“, ACM Inroads 2010 March, Vol. 1, No. 1. Available at
https://spinroot.com/spin/Doc/p40-ben-ari.pdf
Modeling – MicroConsult Training & Coaching
Do you want to bring yourself up to date with the latest technology?
Then find out more here MircoConsult offers training courses/seminars/workshops and individual coaching on the topic of modeling/embedded and real-time software development.
Training & coaching on the other topics in our portfolio can be found here. here.
Modeling – Expertise
Valuable expertise in modeling/embedded and real-time software development is available. here Available for you to download free of charge.
You can find expertise on other topics in our portfolio here. here.
