Model checking is a finite state verification technique to detect concurrency errors, which is often subtle and difficult to reproduce. Object-oriented paradigms are widely used in concurrent and distributed systems. However, many object-oriented modeling languages have weak semantic foundations and have difficulties in automatic verification.
In this thesis, we propose an automatic verification procedure for concurrent object models, which is supported by a model checker SPIN. A modeling language SPIN++ for coucurrent object-oriented systems is prepared. We adopt the concurrency model of JAVA and the control structure of Promela to support concurrent and dynamic behavior modeling. A translation algorithm from SPIN++ to Promela is described so that system models in SPIN++ can be verified by SPIN. Concurrency properties required to the system is described in extended linear temporal logic.
To demonstrate the applicability of our approach, a point-of-sale system is modeled and verified. A SPIN++ translator is implemented and the translation result of the example system is given.
