Model-based testing and model checking for safety critical hierarchical systems

Abstract

The ever-growing magnitude and complexity of computer systems, along with the pressure to drastically reduce system development time and the rising society’s reliance on their correctness, make the delivery of correct systems an extremely important and difficult task. Traditional systems verification techniques such as testing often prove themselves inadequate to face such challenges, thus, both in academia and industry, techniques are sought to reduce and ease the verification efforts while increasing their effectiveness. The model-based verification approach introduces formal methods in the verification process and allows for the application of techniques ranging from automatic test case generation to model checking. This thesis work extends previous research in model-based verification conducted within the CRYSTAL European project. In such previous research, the Dynamic State Machines (DSTM) formal specification language was introduced, along with an automatic test case generation procedure from a DSTM model. In this thesis work, several crucial issues with the previously-defined procedure are detected and addressed by devising a novel test case generation procedure. Furthermore, a novel logic formalism (Hierarchical Linear-time Temporal Logic with Interrupts) is proposed and theoretical foundations for DSTM model checking are laid down.