Experience has shown that the quality of a product greatly depends on the development process used for producing it. In Situational Method Engineering (SME), the objective is to develop a Software Development Methodology (SDM); hence, SME approaches need reliable verification and validation methods for analyzing and assuring the quality of the methodologies that they produce. Since process and product models are used in SME for representing the target methodology, one way to incorporate verification and validation in SME approaches is to analyze – verify and validate – the process/product models through the application of systematic methods. The ultimate objective in assuring the quality of the produced SDM is to detect and rectify the problems that may adversely affect the quality of the software systems which will be developed through applying that SDM.
Model checking techniques are among the most effective model analysis techniques, and have come a long way in Software Engineering (SE). However, model checking is a relatively young field in SME. The main objective of this research is to propose the use of model checking techniques for analyzing the models produced in SME. To this aim, SE model checking techniques will be customized for use in the context of SME models. The stages of the research include the following: The model checking techniques currently practiced in SE will first be reviewed and analyzed; the research efforts that have so far been conducted on analyzing SME models will then be studied; customized SE model checking techniques that are applicable to SME models will be proposed next; and ultimately, the validity of the proposed techniques will be assessed based on a set of evaluation criteria and a case study.