Sciweavers

Share
SPIN
2000
Springer

A Language Framework for Expressing Checkable Properties of Dynamic Software

9 years 24 days ago
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...
James C. Corbett, Matthew B. Dwyer, John Hatcliff,
Added 25 Aug 2010
Updated 25 Aug 2010
Type Conference
Year 2000
Where SPIN
Authors James C. Corbett, Matthew B. Dwyer, John Hatcliff, Robby
Comments (0)
books