A Formal Approach to System Integration Testing

TL;DR

This paper proposes a formal verification-based approach for system integration testing using SystemC models, aiming to improve applicability to industrial cases and address a gap in formal methods for integration testing.

Contribution

It introduces a novel formal verification framework for SystemC-based system integration testing, bridging the gap between theoretical methods and industrial applicability.

Findings

Formal verification of components and system models is feasible.

The approach enhances reliability verification in system integration.

It addresses limitations of existing verification frameworks for industrial use.

Abstract

System integration testing is the process of testing a system by the stepwise integration of sub-components. Usually these sub-components are already verified to guarantee their correct functional behavior. By integration of these verified subcomponents into the overall system, emergent behavior may occur, i.e. behavior that evolves by the assembling of the subcomponents. For system integration testing, both, the correct functional behavior of the overall system, and, the proper functioning of the sub-components in their system environment, have to be verified. In this work we present the idea of an approach for system integration testing based on formal verification. The system components are modeled in SystemC. In a first step these components are formally verified. Then a model of the overall system is built. In a second step this system model is formally verified. The novelty of this approach is given by two aspects: First, up to now the available verification frameworks for SystemC-models are more a proof of concept than really applicable to real industrial case studies. Secondly, although formal verification techniques are a common technique for the verification of software and hardware, by now they have only marginally considered for system integration testing.