Testing Real-Time Task Networks with Functional Extensions Using Model-Checking
Büker, Matthias and Metzner Alexander, Stierand, Ingo
Abstract—Analysis and verification of safety critical systemsis inevitable to assure functional and temporal correctness. Forchecking temporal system behaviour, real-time scheduling analysishas been proved to be an efficient method. As an analyticalmethod, real-time scheduling relies on rather simple task networkmodels mostly ignoring functional behaviour in order to remaincomputable and efficient. Functional and temporal system behaviourhowever are often closely related. By abstracting fromfunctional behaviour, scheduling analysis often results in largeover-approximation for such systems.We propose a task network model providing extensions todescribe also functional system behaviour. The main elementsare explicit data objects and tasks with internal states and datadependant executions. Since there are no analytical methodsknown to be available for such extended models we propose ananalysis 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 realtimesystems. Moreover, the approach provides a convenient wayto check systems against functional and temporal requirementsin contrast to analytical methods that are usually restricted tosimple temporal properties like deadlines.
09 / 2009
inproceedings
IEEE
COMBEST
Component-based Embedded Systems Design Techniques
Component-based Embedded Systems Design Techniques
