Duration: 2004 until 2008
Funded by: NWO
Summary of the project
The aim of this project is to develop and implement model checking techniques for object-oriented designs and programs, based on a representation of program states as graphs and computation steps as graph transformations. The advantage of this representation over the more traditional one (which is essentially based on fixed state vectors determined at compile time) is that the graph formalism quite naturally captures the dynamic nature of object-oriented systems that is due to object (de)allocation and patterns of method invocations. Furthermore, graphs offer new insights in state abstraction, one of the most promising principles to combat state space explosion. Finally, the representation of objects as graphs provides a direct link to popular design notations such as those offered by the UML, and the use of graph transformation is currently advocated in several earlier stages of software development; thus, there is a realistic hope of integrating graph-based object-oriented verification techniques into a more encompassing, truly useful software engineering process.
