Formal methods offer an effective means to assert the correctness of software systems through mathematical reasoning. However, the need to formulate system properties in a purely mathematical fashion can create pragmatic barriers to the application of these techniques. For this reason, Dwyer et al. invented property specification patterns which is a system of recurring solutions to deal with the temporal intricacies that would make the construction of reactive systems very hard otherwise. Today, property specification patterns provide general rules that help practitioners to qualify order and occurrence, to quantify time bounds, and to express probabilities of events.

PSP framework
Property Specification Pattern Framework (PSPFramework).

To combine all these aspects in a single approach we have created PSPFramework, a three-tier system consisting of a unified patterns catalogue, a natural language interface based on Structured English Grammar, and a collection of mappings to suitable logic formalisms.

PSP framework PSPFramework's Pattern Catalogue.

The pattern catalogue in the bottom tier defines all the patterns that we have catalogued in PSPFramework. A Structured English Grammar, an English-like specification scheme to capture pattern-based system properties, constitutes the middle tier. Conceptually, the Structured English Grammar is paired with a set of suitable logic formalism mappings. The resulting isomorphisms yield a PSP Framework set of syntax-directed definitions that system engineers can use to formalize requirements (the system properties) in a pattern-based fashion. The top tier encompasses supported pattern mappings to logic formalisms of choice. At present, it provides support for LTL, CTL, MTL, TCTL, CSL, and PLTL PSPFramework contains qualitative, real-time, and probabilistic property specification patterns. However, a given logic formalism may only offer limited support for representing a specific pattern instance. As a result, some patterns may not be denotable in the logic formalism of choice. We can express this by omitting a corresponding mapping from a Structured English Grammar phrase (or sub-phrase) to the target logic.

jCT framework

To further simplify the specification of system properties PSPFramework also includes PSPWizard, a tool to specify temporal logical properties with specification Patterns. PSPWizard is a stand-alone application written in Java. PSPWizard is designed to allow system engineers the flexibility to define system properties generically, without having to commit to writing a qualitative, real-time, or probabilistic specification in a specific logic formalism. This mechanism provides an effective means to map a given specification to various formats. PSPWizard, once instantiated with a concrete target logic mapping, guides the system engineer through the property specification pattern catalog in a top-down fashion to indicate which patterns and subordinate attributes are supported in the selected target formalism.