Verifying Service-oriented Requirements using Model Checking

Software reuse has long been recognized to be an effective way to improve software quality and productivity. Obtaining a proper set of reusable requirement is the key to achieve successful domain engineering. By tailoring the domain engineering, developers can acquire requirements models for application engineering. Early requirements analysis is one of the most important and difficult phases in the software development process. This paper presents an approach to model the user requirements in a service-oriented view. We uses the SOFM (Service-Oriented Feature Model) to structure requirements as SOCIM (Service-Oriented Computer Independent Model), furthermore, automated verification of requirements specification is done by model checking. Model checking in this paper involves two aspects such as completeness and consistency of requirements. To do so, we transform the SOCIM into a formal specification using a Kripke structure. An electric book store is introduced throughout the paper, which is used as an example to demonstrate our approach more clearly.