A Language Framework for Expressing Checkable Properties of Dynamic Software

Research on how to reason about correctness properties of software systems using model checking is advancing rapidly. Work on exnite-state models from program source code and on abstracting those models is focused on enabling the tractable checking of program properties such as freedom from deadlock and assertion violations. For the most part, the problem of specifying more general program properties has not been considered. In this paper, we report on the support for specifying properties of dynamic multi-threaded Java programs that we have built into the Bandera system. Bandera extracts nite-state models, in the input format of several existing model checkers, from Java code based on the property to be checked. The Bandera Speci cation Language BSL provides a language for de ning general assertions and pre post conditions on methods. It also supports the de nition of observations that can be made of the state of program objects and the incorporation of those observations as predicate...

• Type: Conference
• Year: 2000
• Where: SPIN
• Authors: James C. Corbett, Matthew B. Dwyer, John Hatcliff, Robby
• Keywords: Bandera Speci Cation, General Program Properties, Program Properties, SPIN 2000, Theoretical Computer Science