Applying model checking to concurrent object-oriented software

Model checking is a formal verification technique which checks the consistency between a requirement specification and a behavior model of the system by exploring the state space of the model. We apply model checking to formal verification of concurrent object-oriented systems, using an existing model checker SPIN which has been successful in verifying parallel systems. First, we propose an Actor-based modeling language, called APromela, by extending a modeling language Promela which is a modeling language supported in SPIN. APromela supports not only all the primitives of Promela, but additional primitives needed to model concurrent object-oriented systems, such as class definition, object instantiation, message send, and synchronization. Second, we provide translation rules for mapping APromela´s such modeling primitives to Promela´s. By giving an example of specification, translation, and verification, we also demonstrate the applicability of our proposed approach, and discuss the limitations and further research issues