Causality-Based Model Checking for Real-Time Systems
Julian Siber
For many of today’s digital systems, correctness not only depends on the exact result that is computed, but also on whether the computation finishes in time. These real-time systems often fill safety-critical roles and interact with their physical environment, circumstances that call for rigorous verification of their correctness before deployment. A common technique for verifying whether a given system satisfies a property is model checking. With timed automata as a formal model, there exist multiple highly-optimized tools that facilitate specification and verification of real-time systems. However, even state-of-the-art model checkers struggle with the complexity introduced by concurrency. This is due to the large number of states present in a network of timed automata. For discrete systems, a promising technique for efficient model checking in concurrent settings is causality-based verification. Unlike conventional model checking methods, the causality-based approach does not rely on a comprehensive state space traversal. Instead, it analyzes the cause-effect relationships of events leading to a hypothetical error, aiming to prove the error’s non-existence by contradiction. The analysis is driven by domain-specific proof rules that facilitate inference of the causal dependencies between events. These rules potentially allow for considerable shortcuts, in this way mitigating the state space explosion inherent to the model checking problem. In this thesis, we extend causality-based verification to networks of timed automata. We apply the causality-based concurrency model of concurrent traces to a real-time setting and provide the necessary operations for model checking. Further, we define a number of appropriate proof rules that capture the cause-effect relationships in timed automata and provide an algorithm for constructing proofs of safety properties. We conclude by demonstrating that our algorithm proves the safety of Fischer’s protocol for mutual exclusion in polynomial space and time.
Bachelor Thesis.