Extending Model Checking To Object Process Validation

Object-oriented techniques allow the gathering and modelling of system requirements in terms of an application area. The expression of data and process models at that level is a great asset in communication with non-technical people in that area, but it does not necessarily lead to consistent models. To avoid that inconsistencies are only discovered during the latest phases of development, it is helpful if analysis models can be verified, especially if this is done in an automated process and if it gives feedback that helps repair the models. This thesis presents such an approach for the process aspects of analysis models.