Software Property Specification
Extraction of checkable models is just one piece of the puzzle. Another key impediment to the use of finite-state verification tools in practice is the problem of encoding statements of system correctness requirements in the formal languages that those tools take as input. The Specification Patterns project addresses that problem. The patterns work has recently been integrated with Bandera.
- Robby's MS thesis describing the Bandera specification language in detail.
- A Language Framework For Expressing Checkable Properties of Dynamic Software, James C. Corbett, Matthew B. Dwyer, John Hatcliff, and Robby in Proceedings of the SPIN Software Model Checking Workshop, Lecture Notes in Computer Science, Springer-Verlag, Aug, 2000.