Testing, Model Checking and Static Analysis – Dream Team or Rivals?


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 guidelines such as the MISRA standards 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 talk, 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 will outline how to employ the mentioned techniques, how they work and which results to expect from them. Furthermore, we will highlight strengths and weaknesses of the different methods and discuss possible combinations.

In Proceedings Embedded World Conference 2021 DIGITAL, Weka
Sebastian Krings
Sebastian Krings
Software Engineer

My interests include software analysis, formal methods and offensive security.