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.



Related Papers:

Related Topics:

Finite State Verification Tools:

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