Specifying Temporal Properties in UML Using Patterns: A Tool-Supported Approach

When designing software and hardware systems, it's important to ensure that they function correctly. Formal specification and verification of temporal properties is a critical aspect of achieving this. However, inexperienced designers often struggle with the mathematical nature and notation involved in the process. To make it easier for UML designers, a new property specification technique has been developed in Temporal OCL (TOCL). This technique uses only UML notations and builds upon existing specification patterns. It has been implemented in the Temporal Property Validator (TPV) tool, which makes it accessible and easy to use. Two case studies have shown that this method can specify a variety of temporal properties effectively.