|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|