Testing real-time task networks with functional extensions using model-checking

Analysis and verification of safety critical systems is inevitable to assure functional and temporal correctness. For checking temporal system behaviour, real-time scheduling analysis has been proved to be an efficient method. As an analytical method, real-time scheduling relies on rather simple task network models mostly ignoring functional behaviour in order to remain computable and efficient. Functional and temporal system behaviour however are often closely related. By abstracting from functional behaviour, scheduling analysis often results in large over-approximation for such systems. We propose a task network model providing extensions to describe also functional system behaviour. The main elements are explicit data objects and tasks with internal states and data dependant executions. Since there are no analytical methods known to be available for such extended models we propose an analysis based on a combination of model-checking and testing. Although this technique does not provide exhaustive verification, it is a first step towards time-accurate analysis of complex realtime systems. Moreover, the approach provides a convenient way to check systems against functional and temporal requirements in contrast to analytical methods that are usually restricted to simple temporal properties like deadlines.