Graphical Scenarios for Specifying Temporal Properties:
an Automatic Approach

Temporal logics are commonly used for reasoning about concurrent systems. Model checkers and other finite-state verification techniques allow for automated checking of system model compliance to given temporal properties. These properties are typically specified as linear-time formulae in temporal logics. Unfortunately, the level of inherent sophistication required by these formalisms too often represents an impediment to move these techniques from "research theory" to "industry practice". The objective of this work is to facilitate the non trivial and error prone task of specifying, correctly and without expertise, temporal properties. In this pages we present a simple but expressive formalism for specifying temporal properties. We present a scenario-based visual language that is an extended graphical notation of a subset of the UML 2.0 Interaction Sequence Diagrams. This formalism is called Property Sequence Charts. In addition, we propose an algorithm, implemented as a plugin of our CHARMY tool, to translate such a specified property into a test automaton (i.e., Buchi automaton). We have validated the expressiveness of our approach with respect to well known property specification patterns.">.

The mapping for all the property specification patterns can be found here.