Embedded Systems Solutions logo  
 
 
 
     
     
  Products  
     
   
     
 
 
     
  Events & Promos  
 
     
 
Axivion Logo
 
 
     
  Testing, Model Checking and Static Analysis | Dream Team or Rivals?  
     
   
     
 

Abstract — Ensuring reliability and quality of software has become a necessity. This is especially true for safety critical systems. To do so, different techniques have been established in industry and academia. For instance, coding standards such as the MISRA ruleset or the AutosarC++14 ruleset have been developed. Additionally, software testing, static analysis and even model checking and formal proof are used. These approaches differ with respect to the effort needed and the environments they can be used efficiently in.

In this paper, we will present a simple case study. Following the development of a light and speed control system, we will highlight how and when verification techniques can be employed and how selected requirements can be translated into properties to be checked. In particular, we outline how to employ the mentioned techniques, how they work and which results to expect from them. Furthermore, we highlight strengths and weaknesses of the different methods and discuss possible combinations.


Keywords—component; formatting; style; styling; insert (key words)

[By Dr. Sebastian Krings – originally published at Embedded World DIGITAL conference 2021]

 
     
 

INTRODUCTION:

 
     
 

With the ongoing digitalization, the trend towards the internet of things, industry 4.0, and the ongoing integration of embedded devices into everyday objects, our dependency on software components increases by the hour. From cars to trains to medical equipment, software components are more safety critical than ever. Or, as Marc Andreessen put it: “Software is eating the world” [1].

As a consequence, ensuring both reliability and quality of software has become a necessity. This is especially true for safety critical systems, where a malfunction can directly endanger users as well as innocent bystanders. However, even for software not deemed safety-critical, malfunction can and has led to enormous damage and financial losses [2].

In consequence, several techniques for ensuring the proper functionality of software have been developed and are in active use in industry as well as being actively researched in academia. In the following, we will use a simple case study to highlight some key techniques for verification and validation and discuss their application to an embedded software product.

 
     
 

CASE STUDY:

 
     
 

The case study used as an example throughout this paper is based on the ABZ 2020 case study [3]. It describes two assistant systems commonly found in modern cars. The overall system consists of two loosely coupled components, namely an adaptive exterior light system (ELS) and a speed control system (SCS). The ELS controls head- and taillights, setting their brightness depending on the surroundings and user preference. At the same time, the SCS controls the vehicle’s speed, again by considering the environment as well as parameters given by the driver. Obviously, both are safety critical components, rendering safety and security a development priority.

Both components are to be developed in C, following the MISRA C 2012 coding guidelines [4]. A (simplified) component diagram, taken from [5], is shown in Fig. 1. As you can see, both ELS and SCS are supposed to be realized as continuous loops of reading sensors, executing their particular functionality and storing the last state for future reference. This might be needed to compute timer offsets or react to changing user inputs.

Both systems receive inputs from the driver via the steering wheel and various other actuators. Further inputs are provided by multiple sensors, e.g., for speed or brightness. The system contains a clock and might have to fulfill various requirements regarding real-time operations. Finally, the systems provide output to the actors controlling the car’s light and speed.

 
     
 

TESTING, MODEL CHECKING AND STATIC ANALYSIS:

 
     
 

In the following section, we will outline how common verification techniques could be used to validate and verify the correct operation of ELS and SCS.

A. Testing
Testing is perhaps the most commonly known technique for asserting the quality of a software system. Simply speaking, testing tries to ensure the correct behavior of software by executing it on a set of input data. After execution, the results are compared to a set of expected results.

 
     
   
 
Learn More Scroll Top