"Property Specification Patterns for Finite-State Verification"

paper

"Property Specification Patterns for Finite-State Verification"
Matthew B. Dwyer Kansas State University, Department of Computing and Information Sciences, 234 Nichols Hall Manhattan, KS
George S. Avrunin University of Massachusetts, Department of Mathematics and Statistics, Box 34515, Amherst, MA
James C. Corbett University of Hawai'i, Department of Information and Computer Science, Honolulu, HI


ABSTRACT
Finite-state verification (e.g., model checking) provides a powerful means to detect errors that are often subtle and difficult to reproduce. Nevertheless, the transition of this technology from research to practice has been slow. While there are a number of potential causes for reluctance in adopting such formal methods in practice, we believe that a primary cause rests with the fact that practitioners are unfamiliar with specification processes, notations, and strategies. Recent years have seen growing success in leveraging experience with design and coding patterns. We propose a pattern-based approach to the presentation, codification and reuse of property specifications for finite-state verification.

Keywords
Patterns, fin&state verification, formal specification,
concurrent system

@inproceedings{298598,
author = {Dwyer, Matthew B. and Avrunin, George S. and Corbett, James C.},
title = {Property specification patterns for finite-state verification},
booktitle = {FMSP '98: Proceedings of the second workshop on Formal methods in software practice},
year = {1998},
isbn = {0-89791-954-8},
pages = {7--15},
location = {Clearwater Beach, Florida, United States},
doi = {http://doi.acm.org/10.1145/298595.298598},
publisher = {ACM},
address = {New York, NY, USA},
}

CF)
Property Patterns for the Formal Verification of Automated

Jose Creissac Campos  Jose Machado  Eurico Seabra

Abstract: In recent years, several approaches to the analysis of automation systems depend-
ability through the application of formal veri cation techniques have been proposed. Much of
the research has been concerned with the modelling languages used, and how best to express the
automation systems, so that automated veri cation might be possible. Less attention, however,
has been devoted to the process of writing properties that accurately capture the requirements
that need veri cation. This is however a crucial aspect of the veri cation process. Writing
appropriate properties, in a logic suitable for veri cation, is a skilful process, and indeed there
have been reports of properties being wrongly expressed. In this paper we put forward a tool
and a collection of property patterns that aim at providing help in this area.
Keywords: Analysis of reliability and safety, Methodologies and tools for analysis of complexity, Modelling

Proceedings of the 17th World Congress
The International Federation of Automatic Control
Seoul, Korea, July 6-11, 2008