Property Specification Pattern Wizard

 

Formal verification techniques are a powerful means to ensure that a software-intensive system fulfills its quality requirements. However, for the verification process to come feasible, it is required to formulate these properties in some mathematical logic, an aspect that has the potential of producing pragmatic barriers to application in practice. Research on property specification has supplied us with rich pattern catalogs that capture commonly occurring system properties in different temporal logics. Furthermore, these property specification pattern catalogs usually offer both a structured English grammar to facilitate the pattern selection and an associated template solutions to express the properties formally. The actual use of property specification still remains cumbersome due to the limited tool support. The PSPWizard as been developed to help practitioners formulate these properties correctly. PSPWizard consists of two main building blocks: a mapping generator that weaves a given pattern library with a target logic and a GUI front-end to the structured English grammar tailored to those patterns that are supported in the target logic. XML-based formilism has been implemented for the specification of catalog and mappings to target logics. The GUI of the tool is automatically configured for a selected catalog and a target logic and guides the user through the specification patterns, leading to a complete property specification. [TOOL] [READ ME]

References

Grunske L., Specification Patterns for Probabilistic Quality Properties. 30th International Conference on Software Engineering (ICSE 2008), Leipzig, Germany, May 10-18, 2008. ACM 2008, ISBN 978-1-60558-079-1, pp. 31-40.

M. B. Dwyer, G. S. Avrunin, and J. C. Corbett, Patterns in property specifications for finite-state verification, in Proceedings of the 1999 International Conference on Software Engineering (ICSE’99). New York: Association for Computing Machinery, 1999, pp. 411-421.

P. Bellini, P. Nesi, and D. Rogai, Expressing and organizing real-time specification patterns via temporal logics, Journal of Systems and Software, vol. 82, no. 2, pp. 183-196, 2009.

V. Gruhn and R. Laue, Patterns for timed property specifications , Electr. Not. Theor. Comp. Sci, vol. 153, no. 2, pp. 117-133, 2006.

S. Konrad and B. H. C. Cheng, Real-time specification patterns, in 27th Int. Conf. on Software Engineering, ICSE 05, G.-C. Roman, W. G. Griswold, and B. Nuseibeh, Eds. ACM, 2005, pp. 372-381.

[TOP]

Downloads

PSPWizard Binary files [READ ME]

Pattern Catalog Structured English Grammar

Expert mapping specification of MTL

Expert mapping specification of PRISM

Source Code

JAVA Documentation

[TOP]

Screenshots

1Select target logic Select the target property specification language
2List of temporal scopes List of temporal scopes will be displayed. The appropriate scope needs to be selected.
3List of Pattern categories Select the type of the pattern, whether order or occurrence
4List of Occurrence Patterns List of occurrence patterns
5List of Order Patterns List of order patterns
6State Formula Editor Add the state formulas
7Time Bound Editor Time bound editor
8Response Example in MTL Example response pattern in MTL specification language
9Response Example in PRISM Example response pattern in PRISM specification language

[TOP]

Contact

Markus Lumpe

Faculty of ICT
Swinburne University of Technology
John Street,Hawthorn
Melbourne, Victoria 3122
AUSTRALIA
Telephone: +61 3 9214 4758
Fax: +61 3 9819 0823
Email: mlumpe[at]swin.edu.au

Lars Grunske

Software Engineering: Analysis Quantitative of Aspects (AQUA)
University of Kaiserslautern
PO Box 3049
67653 Kaiserslautern
GERMANY
Telephone: +49 631 205 3958
Fax: +49 631 205 3420
Email: lgrunske[at]cs.uni-kl.de

Indika Meedeniya

Faculty of ICT
Swinburne University of Technology
John Street,Hawthorn
Melbourne, Victoria 3122
AUSTRALIA
Telephone: +61 3 9214 4758
Fax: +61 3 9819 0823
Email: imeedeniya[at]swin.edu.au

[TOP]