Observer Patterns for Real-Time Systems

In the past few decades, many formal techniques for verifying complex concurrent and real-time systems, as well as many property languages, have been proposed. Unfortunately, many of these techniques involve formalisms that are not always easy to handle by engineers, furthermore, they generally need dedicated tools. We propose here a set of correctness patterns encoding common properties met when verifying concurrent real-time systems. We show how to translate these patterns into pure reachability problems, thus avoiding the use of complex verification algorithms. Furthermore, we provide an instantiation of these patterns in both timed automata and stateful timed CSP, to show the applicability of our approach.