Formalizing the use case model: A model-based approach

In general, requirements expressed in natural language are the first step in the software development process and are documented in the form of use cases. These requirements can be specified formally using some precise mathematical notation (e.g. Linear Temporal Logic (LTL), Computational Tree Logic (CTL) etc.) or using some modeling formalism (e.g. a Kripke structure). The rigor involved in writing formal requirements requires extra time and effort, which is not feasible in several software development scenarios. A number of existing approaches are able to transform informal software requirements to formal specifications. However, most of these approaches require additional skills like understanding of specification languages additional artifacts, or services of domain expert(s). Consequently, an automated approach is required to reduce the overhead of effort for converting informal requirements to formal specifications. This work introduces an approach that takes a use case model as input in the proposed template and produces a Kripke structure and LTL specifications as output. The proposed approach also considers the common use case relationships (i.e., include and extend). The generated Kripke structure model of the software allows analysis of software behavior early at the requirements specification stage which otherwise would not be possible before the design stage of the software development process. The generated LTL formal specifications can be used against a formal model like a Kripke structure generated during the software development process for verification purpose. We demonstrate the working of the proposed approach by a SIM vending machine example, where the use cases of this system are inputs in the proposed template and the corresponding Kripke structure and LTL formal specifications are produced as final output. Additionally, we use the NuSMV tool to verify the generated LTL specifications against the Kripke structure model of the software, which reports no counterexamples thus validating the proposed approach.