Statechart-based Verification of Object-Oriented Design Models

Recently, design models that precise behavior of objects is specified are proposed. Though, currently, they are mainly used for their execution and automatic source code generation, they also have potential to allow us to verify them in the design phase. In this paper, we propose a method to verify such design models in the design phase. In addition, we adopt theorem proving systems to rigorously and efficiently verify it.