Efficient Model-Checking for Real-Time Task Networks

Formal methods play an important role in the development of safety-critical systems. Their well-defined semantics can be employed for automatic formal system verification. Model-checking, a well-established formal verification technique, is however often restricted to an abstract level due to complexity reasons. For example, checking temporal system behavior with respect to hardware architectures and operating systems is often not possible.Real-time scheduling theory on the other hand provides efficient techniques for temporal analysis of real-world systems at architecture level.However, models used in real-time scheduling theory usually lack a semantics that is compatible to those used by formal specifications. This prevents to verify temporal system behavior at the architecture level with the same formal methods.We present an approach that combines a timed automata representation of task networks and efficient scheduling analysis techniques. Based on existing task network formalisms we define a consistent timed automaton model, and a mapping between both formalisms. We prove that the mapping induces behavioral equivalence of the models.We show an application of the approach by verifying task networks against Live Sequence Charts (LSC).