Modern in-vehicle infotainment systems comprise highly interactive software components. The veri cation of the interfaces of such components poses a major challenge for developers. In this work, we present an approach for model-based veri cation of distributed infotainment components. We de ne a layered reference model which speci es the interaction between two components at syntactical and behavioral level. The layers abstract from the used middleware so developers may focus on the components' actual interface behavior. Additionally, we dene a model execution framework which enables the reuse of the reference model for veri cation of interface implementations. We demonstrate the applicability of the approach using an industrial case study. Our approach aims at reducing errors in the communication behavior and increasing the overall product quality.
The growing amount and the increasing interdependency of functions in modern
automobiles [
42 Infotainment / Communication
10 •Hybrid control •Fuel cell control •Start/stop control •E-vehicle control
17 •Active shock absorber •Steer-by-Wire •Electronic wedge brake
31 •Rear end crash avoidance system •Traffic sign recognition system Total
Powertrain
Chassis / Body
Active Safety where services of di erent suppliers and the OEM are integrated in a single hardware platform using an IPC bus for the message exchange. For such integration scenarios, the veri cation of software components and their interfaces is needed to assure compatibility and enable a well-de ned user experience and premiumclass quality. This can be di cult when third-party services are provided as black-boxes, where only their communication can be monitored.
Within the automotive application development, model-based approaches
have been applied successfully over time [
We identi ed the following items as most de ning challenges for the veri cation of infotainment interfaces with respect to their communication: 1. Abstraction: Middlewares de ne their own protocols and interface description languages. The modeling approach should abstract from these technical details so developers may focus on the components' actual interface behavior. 2. Parallel interactions: Manifold software-based features are assembled and executed in parallel with interfaces partially interdependent. The many potential system states and interactions are very di cult to capture. 3. Synchronization (Initialization): The parallel interactions make it hard to identify the actual communication state. Anyway, the veri cation mechanism needs to be able to assume this state for carrying out the veri cation. 4. Timeouts: Infotainment is not a safety-critical domain, but the meeting of timing requirements is essential for orchestration of interactive components. 5. Error detection: The veri cation should reliably detect an abnormal operation and encircle the actual fault leading to the erroneous functionality. 6. Executable interface speci cation: Especially with complex infotainment systems manual veri cation is a tedious and error-prone task. Automatic veri cation requires input for the interpretation by a machine. For model-based speci cations this can be achieved with executable semantics. Within this paper, we focus on an approach for model-based veri cation of the communication behavior of distributed infotainment components considering the above characteristics. Special emphasis is put on the design and reuse of so-called reference models from the speci cation phase for the veri cation. Therefore, a concept for the veri cation of infotainment components' interfaces by using executable reference models is presented. The main goals are to reduce the veri cation costs while preserving or even increasing the product quality.
The contribution of our work is twofold. First, we de ne a layered reference model which is used to specify the interaction between components at syntactical and behavioral level. Thereby we take into account that interfaces are usually de ned at syntactical level in an existing proprietary language. We seamlessly integrate those middleware dependent speci cations in our modeling approach. In addition, we de ne a framework for executing such reference models. This enables us to reuse the models de ned for speci cation in a veri cation process.
The remainder of this paper is organized as follows: In Section 2, we give a brief overview of related work. Afterwards, Section 3 outlines our approach for the model-based veri cation of infotainment interfaces using reference models. In Section 4, we present the software architecture and execution semantics used to enable the veri cation of component interfaces in the infotainment domain. In Section 5 our approach is demonstrated using an industrial case study. We conclude the paper in Section 6. 2
Model-based development of application interfaces is widely applied in the
automotive domain. For instance, MATLAB/Simulink [
Infotainment components are usually implemented by di erent parties based
on a speci cation given by the car manufacturer. Speci cations are written in
natural language and enriched with software models. In today's automotive
software engineering, the speci cation models are often only used as visual
representation of speci c aspects. We aim at maximizing the automation of veri cation
processes using these speci cation models. Current veri cation methods rely on
sequence-based tests [
An automated test oracle can be provided by execution of the speci cation
models. Further, the possibility to simulate and observe the reactions of a model
to a given sequence of events helps to understand the speci ed mechanisms. The
frameworks Populo [
In this paper, we introduce an applicable approach for the veri cation of communication interfaces in the automotive infotainment domain. We exploit executable reference models created during the speci cation phase of infotainment components for the veri cation of implementations in the integration phase. 3
We address the challenges of interface veri cation in automotive infotainment systems by using layered interface speci cations. A so-called layered reference model is manually derived from the requirements. It describes the communication between two components including all involved interfaces and behavioral interactions. Figure 2 shows the di erent layers of the reference model.
The interface de nition model describes the artifacts (e.g., broadcasts, methods, types) of the involved interfaces on a syntactical level. This layer uses the proprietary interface description language usually provided by a middleware technology. By changing this layer, the model can be adapted to the utilized target middleware. Figure 3a shows an example interface de nition model for automotive infotainment components.
The event de nition model bridges the gap between the middleware dependent interface de nition model and the middleware independent behavioral model. The modeler speci es the invocation of an interface artifact using an event de nition and re nes this event with a constraint. A constraint is de ned by bainterface definition models event definition models
IF1 : IDL1
IF2 : IDL2
IF3 : IDL3 IF1 events
IF2 events
IF3 events
defined by interface simple { interface simple { } }mv}eetrmmo}hsiauoinjtdoIoonnrr{mte{801ssiadge { R}}CReaeslsmcmmcplpeoeeooEotnttnnvnhshhssesotootenedrddrEtERaRRavveieeierefnffnenntttqtmmmue{ee{rersissiseesdssdptpaaallg=gg=y{yeee==OTnw12eo}}{{ }
} (a) interface de nition ::Timeout sic arithmetic and logical expressions using the parameters which correspond to the interface artifact. The speci ed events are used in the behavioral model as triggers for transitions. Therefore, only events needed in the behavioral models need to be de ned. An example of our textual language for this task is shown in Figure 3b. It may be adapted to other target interface de nition models.
In order to model the ordering of events in a communication relation between
two components we use stereotyped UML state machines [
In UML state machines transitions are de ned with trigger and guard. In our experience with real models, the guard conditions are a powerful concept but might become complex pieces of program code. Therefore, we allow the guard condition to be speci ed using the constraints of the event model only. Triggers may reference an event of the event model or a timeout of the behavioral model. The sender and the receiver of the event are also annotated on the transition.
The limited number of elements without nested code snippets prevents the
use of ambiguous concepts and facilitates a precise description of the
communication relationships. The approach is precise enough for direct code generation
of an executable state chart for a speci c middleware. We could already show
the applicability with a subset of this model for adapter-code generation in [
In this section, we introduce our execution framework for reference models used for the veri cation of interfaces in automotive infotainment systems. The framework monitors the component interaction and reports failures (see Figure 4).
model execution framework execution semantics
With the information from the interface and event models, the event decoder maps incoming messages to events and discards messages not relevant for the reference model. The behavioral model gets triggered by the resulting event stream. Every event which is not consumed by the model in a speci c state will be logged. If such a failure in the communication stream is detected, the current state of the communication is unclear and the active state in the behavioral model has to be determined by the Synchronizer using the next messages.
For executing the reference models, we use open and standardized semantics. fUML de nes execution semantics for a subset of UML, but this subset does not include state machines. Therefore, we use SCXML, which provides well-de ned semantics for executable state machines. SCXML is not based on UML state machines but it is su ciently similar. Most of the modeling elements and concepts in our behavioral models can be mapped straight forward to SCXML: initial nodes, transitions, states with regions for nesting as well as parallel behavior. Special treatment is only needed for the join element, which is not available in SCXML. To compensate for this discrepancy in the mapping, we redirect transitions targeting the join to a new nal state in each region. The join's outgoing transition is connected to the parallel state as source, and triggers when all nal states have been entered.
In SCXML our error semantics can be modeled by containing the original state machine in a state, where a single transition leads to the error state. This transition's trigger is set to match any event. As transitions of inner states precede those of outer states in SCXML, the error transition res only if the event is not consumed by the original state machine. We implemented a straightforward type of Synchronizer with transitions for all unique events to their corresponding target states. A more detailed description of the synchronization mechanism is beyond the scope of this paper. This mapping grants execution, error checking, and synchronization semantics to the proposed modeling approach enabling detection of the following failures: { missing messages, { additional messages, { malformed messages, and { timing violations
Thereby, our reference models together with the execution framework can be used to verify interfaces of infotainment components. 5
In this section we show the application of our approach using an automotive example. An automotive infotainment ECU implements many functions which communicate with other ECU's using the in-car network. This includes reading and setting values. This communication with the hardware services is often realized using a gateway component with respective software proxies. In the following, we introduce a ctive parking assistant (ParkA) software proxy. This service is used for producing a top-view of the car showing the surrounding obstacles. The ParkA component provides a reliable link in order to obtain upto-date sensor values. In this case the reference model describes the inter-process communication inside the infotainment ECU between a Client (e.g. a surround view) and the ParkA-service.
Figure 5a shows the syntactical interface of the ParkA component. The interface provides methods for startup, shutdown and resolution settings. The ParkA service sends the sensor values using the broadcast sensorValues. Figure 5b shows the respective event de nitions for the ParkA interface. In this model we specify concrete occurrences of broadcasts, method calls or responses.
In addition to the syntactical interface and events we de ne the protocol for a speci cation-conformant interaction with a ParkA service. Figure 5c shows the behavioral model. To initiate communication, the client has to invoke the startUp-Method. If successful (startUp_response_OK), the client is connected Interface ParkA {
CallEvent startUp {
methodRef startUp } ResponseEvent startUp_response_OK { methodRef startUp constraint {returnValue == OK} } ResponseEvent startUp_response_ERROR { methodRef startUp constraint {returnValue != OK} } BroadcastEvent sensorValues {
methodRef sensorValues } ... } (b) ParkA event de nition excerpt.
ParkA:>Client:startUp_response_OK interface ParkA{ method startUp{ in{Resolution res} out{AM_Error returnValue} } broadcast sensorValues { out{
Int32[] front_lmr Int32[] rear_lmr
Resolution res } } enumeration Resolution{ cm mm } enumeration AM_Error{ OK ERROR } ... } and the service starts sending cyclic sensor values using the sensorValuesbroadcast. The time between two of these broadcasts should not be longer than 20ms (Max: 20). At any time in the working-state the client may change the resolution of the sensor values using the setResolution-method or shut down the service using the shutDown-method. This is described using a parallel region.
We show an example for a communication trace in Figure 5c. Each line denes an event number, the timestamp of the event and the already decoded message as string. In this example we annotate the transitions of the behavioral model with the order in which the trace is executed. The ParkA service starts sending sensor values immediately after the startUp method call. This is a deviation from the speci ed behavior and causes the behavior model to trigger the unexpectedEvent-transition. The failure gets logged and the next event (sensorValues) is used for synchronization. The next failure is detected at message number 7. The timeout in state sendingValues elapses and res the timeout_sendingValues-event. This event does not trigger any transition in the active state and will be handled by the unexpectedEvent-transition. Synchronization is done after receiving the next sensorValues-broadcast. The trace completes without further failures. Other unique events have transitions from the Synchronizer into the behavior model, too, which are not shown for clarity.
The case-study illustrates how we address the challenges for the veri cation of automotive infotainment interfaces introduced in Section 1: 1. The event model abstracts from technical details, thus allowing for a clear behavioral model. 2. All potential system states of parallel and partially interdependent components can be captured by using parallel regions and multiple interfaces in the reference model. 3. Using unique messages the presented reference model can be (re-)synchronized to the tested components for initialization or after the model detected a message not conforming to the modeled behavior. 4. The synchronization mechanism allows to detect timeouts during the veri cation (e.g. when a message is not delivered in time) by treating timeouts of states like other events. 5. Reliable error detection is provided by the logged failures, which can later be evaluated by the developer, in order to verify, if the deviant behavior of the implemented interface is identi ed as a de nite error or not. 6. The presented execution framework enables running the reference models in parallel to the components for veri cation.
Thereby, our approach enables the veri cation of infotainment components' interfaces by detecting failures within the communication behavior using executable reference models. 6
In this work, we outlined the major characteristics and challenges for the veri cation of communication interfaces in in-vehicle infotainment systems. Moreover, we have introduced an approach for the veri cation of interfaces which addresses these challenges by using reference models created during the speci cation phase. We showed the applicability of our approach by an example of a parking assistant proxy component. Our approach allows exploiting the e ort once spent for a model-based speci cation in the integration phase, by verifying the quality of the implemented components.
Future emphasis will be laid on the enhancement of the proposed methodology for complex data-depending models. Furthermore, reusing the reference models for so-called restbus simulation with real ECUs will be investigated in future work.