Example Repository

for Finite State Verification Tools

This is an online repository of examples of concurrent systems. It includes many of the problems examined in the literature as well as several real world problems. We hope people will contribute to this repository and use these pages to experiment with available finite state verification tools.

The repository includes a high level description of each problem and some related properties. An implementation of each problem is provided in Ada. Each property is given in several formal property specification languages. These include Computation Tree Logic (CTL), INCA Queries, Never Claims, and Quantified Regular Expressions (QRE). We chose these formalisms because each has tool support for automated analysis: SMV accepts CTL, SPIN accepts Never Claims, and FLAVERS accepts QREs.

This will not be a static repository. We plan on adding more examples and perhaps supporting additional programming languages and property formalisms.

Send any questions/comments/additions to laser-software@laser.cs.umass.edu.

Examples:

• Alternating Bit Protocol
• Border Defense System
• Chiron User Interface
• Cyclic Scheduler
• Divide and Conquer Computation
• Dining Philosophers
• Dining Philosophers with Dictionary
• Dining Philosophers with Fork Manager
• Dining Philosophers with Host
• Elevator (Sequential)
• Elevator (Concurrent)
• Furnace
• Gas Station (Non-Queueing)
• Gas Station (Queueing)
• Hartstone
• Key
• Memory Management
• Overwrite Protocol
• Producers/Consumers
• Readers/Writers
• Sentest
• Speed
• Three Way Handshake Protocol
• Token Ring

References

Related Papers:

• A. T. Chamillard, Lori A. Clarke, and George S. Avrunin, An Emperical Comparison of Static Concurrency Analysis Techniques, Technical Report 96-084, Department of Computer Science, University of Massachusetts at Amherst, August 1996. Revised May 1997.

• James C. Corbett, An Empirical Evaluation of Three Methods for Deadlock Analysis of Ada Tasking Programs, Proceedings of the 1994 International Symposium on Software Testing and Analysis (ISSTA), ed. Thomas Ostrand, August, 1994.

• James C. Corbett, Evaluating Deadlock Detection Methods for Concurrent Software, IEEE Transactions on Software Engineering, 22(3), 05, 1996.

• K. M. Olender and L. J. Osterweil, Cecil: A sequencing constraint language for automatic static analysis generation. IEEE Transactions on Software Engineering, 16(3):268-280, March 1990.

Related Topics:

• Specification Pattern System for information about formal property specification languages.

Finite State Verification Tools:

• FLAVERS contact laser-software@laser.cs.umass.edu
• SMV
• SPIN

Last modified 8 January 2003 at 15:02:16 EST