Patterns in Property Specifications for Finite-State Verification* Matthew B. Dwyer Kansas State University Department of Computing and Information Sciences Manhattan, KS 66506-2302 +l 785 532 6350 [email protected] George S. Avrunin University of Massachusetts Department of Mathematics and Statistics Amherst, MA 01003-4515 +l 413 545 4251 [email protected] James C. Corbett University of Hawai‘i Department of Information and Computer Science Honolulu, HI 96822 +l 808 956 6107 [email protected] ABSTRACT cess support for formal methods. Model checkers and other finite-state verification tools allow developers to detect certain kinds of errors au- tomatically. Nevertheless, the transition of this tech- nology from research to practice has been slow. While there are a number of potential causes for reluctance to adopt such formal methods, we believe that a primary cause is that practitioners are unfamiliar with specifi- cation processes, notations, and strategies. In a recent paper, we proposed a pattern-based approach to the presentation, codification and reuse of property specifi- cations for finite-state verification. Since then, we have carried out a survey of available specifications, collect- ing over 500 examples of property specifications. We found that most are instances of our proposed patterns. Furthermore, we have updated our pattern system to accommodate new patterns and variations of existing patterns encountered in this survey. This paper reports the results of the survey and the current status of our pattern system. Keywords We believe that the recent availability of tool support for finite-state verification provides an opportunity to overcome some of these barriers. Finite-state verifica- tion refers to a set of techniques for proving properties of finite-state models of computer systems. Properties are typically specified with temporal logics or regular expressions, while systems are specified as finite-state transition systems of some kind. Tool support is avail- able for a variety of verification techniques including, for example, techniques based on model checking [19], bisimulation [4], language containment [14], flow anal- ysis [lo], and inequality necessary conditions [l]. In contrast to mechanical theorem proving, which often requires guidance by an expert, most finite-state verifi- cation techniques can be fully automated, relieving the user of the need to understand the inner workings of the verification process. Finite-state verification techniques are especially critical in the development of concurrent systems, where non-deterministic behavior makes test- ing especially problematic. Patterns, finite-state verification, formal specification, concurrent systems 1 INTRODUCTION Although formal specification and verification methods offer practitioners some significant advantages over the current state-of-the-practice, they have not been widely adopted. Partly this is due to a lack of definitive ev- idence in support of the cost-saving benefits of formal methods, but a number of more pragmatic barriers to adoption of formal methods have been identified [22], including the lack of such things as good tool support, appropriate expertise, good training materials, and pro- Despite the automation, users of finite-state verification tools still must be able to specify the system require- ments in the specification language of the tool. This is more challenging than it might at first appear. For example, consider the following requirement for an ele- vator: Between the time an elevator is called at a floor and the time it opens its doors at that floor, the ele- vator can arrive at that floor’ at most twice. To verify this property with a linear temporal logic (LTL) model checker, a developer would have to translate this infor- mal requirement into the following LTL formula: q ((cal1 A Oopen) + *This work wan partially supported by NSF grants CGR- 9407182, CCR-9633388, CCR-9703094, and CCR-9708184 and by NASA grant NAG-02-1209. permission to make digital or hard copies <fall or part ofthis work fhr personal or classroom use is granted without fee provided that wits art: not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the tirst page. TO COPY otlwrwise, to republish, to post on servers or to redistribute 10 lists. requires prior specific permission andior a fee. ICSE ‘99 Los Angclcs CA Copyright ACM 1999 l-581 l3-074-0/99/05...$5.00 ((Tatfloor A lopen) U (open V ((atfloor A -open) U (open V ((Tatfloor A -open) U (open V ((atfloor A -open) U (open V (=tfioor U own)))>)>>>>> Not only is this formula difficult to read and understand, it is even more difficult to write correctly without some expertise in the idioms of the specification language. 411We contend that acquiring this level of expertise rep- resents a substantial obstacle to the adoption of auto- mated finite-state verification techniques and that pro- viding an effective way for practitioners to draw on a large experience base can greatly reduce this obstacle. Even with significant expertise, dealing with the com- plexity of such a specification can be daunting. In many software development phases, such as design and cod- ing, complexity is addressed by the definition and use of abstractions. For complex specification problems, ab- straction is just as important. In [9], we proposed to capture the experience base of ex- pert specifiers and enable the transfer of that experience between practitioners by way of a specification pattern system. This system is, essentially, a collection of pa- rameterizable, high-level, formalism-independent speci- fication abstractions. To maximize the coverage of these abstractions, we have described a variety of techniques for tuning