Testing real-time systems from compositional symbolic specifications

Symbolic models for testing real-time systems that abstract both data and time have been investigated. The goal is to address the state space explosion problem that may occur during test case generation. In this context, testing is often investigated by abstracting the structure of the system under test and by observing traces of expected outputs. However, since real-time systems are usually composed of a number of communicating subsystems, the next challenge is to take into account how the composition of subsystems is specified, developed and possibly tested separately or as a whole system. This paper addresses this challenge by providing a sequential and a parallel operator for composing symbolic models of real-time systems and an integration testing strategy that makes use of them. Also, we present a case study from the avionics domain and discuss barriers regarding the considered conformance relation.