Diagram-Based Verification of Real-Time Systems using Timed Predicate Diagrams

Computers are frequently used in critical applications where predictable response times are essential for correctness. Such systems are called real-time systems and are a class of reactive systems. Many verification methods for verifying reactive systems were proposed, including diagram-based verification. One of diagrams used for reactive systems verification is predicate diagrams proposed by Cansell et.al. It has been shown that this diagram can be used for the verification of discrete reactive systems. In this paper, a class of diagrams called timed predicate diagrams is introduced. These diagrams are a variant of predicate diagrams, which can be used to verify real-time systems. This method has been applied on an example problem which is Fischer’s protocol. Key words