Model Checking Real-Time Component Based Systems with Blackbox Testing

Abstract

In this paper we propose a simple model for component based real-time systems using duration automata. For this simple model we propose an algorithm for solving the emptiness problem using black-box testing for components which is in the same complexity class as for solving the emptiness problem for untimed component based systems. Furthermore, the verification of behavioural real-time properties in this model can be done with techniques from duration Calculus.