Efficient techniques and tools for software testing based on traces and coverage analysis

Abstract

To ensure ultra-high dependability and ultra-low defect rates, certification standards such as DO-178C requires safety-critical software with the highest safety level (Level A) in avionics systems to conform to the modified condition decision coverage (MC/DC) criterion. MC/DC is a strong coverage criterion that subsumes existing coverage criteria and it requires a small number of test inputs compared to the combinatorially exhaustive multiple condition coverage (MCC). MC/DC has also proven to reveal many program defects. However, both MC/DC measurement and generating test cases satisfying MC/DC remain a challenging task. In addition, related properties such data races detection can be monitored using some methods used to check MC/DC, as good concurrency coverage increases a likelihood of catching concurrent-related bugs. To address the above challenges, existing strategies rely on intrusive instrumentation which is not recommended for safety critical software since it consumes valuable resources and can alter the behaviour of the system under test (SUT) if it remains in the released code.

To overcome the above challenges, this thesis introduces novel paradigms and tools for software testing based on traces and coverage analysis. Our aim is to analyse the MC/DC without instrumentation and to monitor data races with a lightweight instrumentation. In addition, we explore the applicability of MC/DC criterion on the design level models. Furthermore, we investigate new techniques for test cases generation satisfying MC/DC with the aim to increase the coverage.

The scientific contribution of this thesis is fourfold:

First, we propose an approach for measuring MC/DC without instrumentation. This has resulted in a tooling for MC/DC measurement and analysis based on the trace of an executing program. A static analysis is used to find conditional jumps in object code that correspond to conditions in the source code. With that information the assignments of the conditions during the execution of the code can be reconstructed by analyzing the trace. MC/DC is then evaluated and the covered/uncovered conditionals in the program can be identified. This approach is evaluated on C programs.

Secondly, we provide a non-intrusive tooling for data races detection using the continuous observation of embedded multicore systems (COEMS) technology through continuous online monitoring with lightweight instrumentation on a novel FPGA-based external platform for embedded multicore systems. It is used in combination with formal specifications in the high-level temporal stream-based specification language (TeSSLa), in which we encode a lockset-based algorithm to indicate potential race conditions. We show how to instantiate a TeSSLa template that is based on the Eraser algorithm, and present a corresponding light-weight instrumentation mechanism that emits the required observations to the FPGA with low overhead.

Thirdly, we investigated the applicability of MC/DC criterion on design level models, where specifically, we conducted a coverage analysis to Coloured Petri Nets (CPNs) models. We implement a library for CPN Tools and a post-processing tool for MC/DC coverage analysis of net inscriptions on a set of model executions and evaluate our approach on eleven larger publicly available CPN models.

In the fourth contribution, we propose a new and alternative strategy for test case generation satisfying MC/DC.We have implemented an algorithm for MC/DC test cases based on binary decision diagrams (BDDs) and evaluated on Traffic Alert and Collision Avoidance System (TCAS II) benchmarks. A performance evaluation with respect to the state-of-the art in the form of related work has been conducted.