Formalization of a Use Case Model to Kripke Structure and LTL Formulas
Software reliability can be ensured by using software verification techniques including model checking. A model checker takes a software model along with formal specifications and verifies either the provided model satisfies the input formal specifications or not. The cost and effort required to generate a software model and formal specifications may not be feasible in all software development. This opens the door for the approaches that can transform informal software requirements to formal specifications and model. There are a number of approaches to transform informal software requirements into semiformal or formal software specifications. However, the existing approaches require informal software requirements in a controlled natural language. Some approaches, require additional skills like understanding of object-oriented paradigm and domain knowledge. A number of theses approaches generate semiformal models which may not be suitable to be directly used by software verification techniques. Some of these approaches generate formal model as an output. But formal specifications, against which the model is to be verified, are still required. There is a need for an approach that generates a model along with formal specifications from the informal software requirements. The generated model, however, is a primitive model of a software, along with the generated formal specifications can be used for model checking. This facilitates the software verification process and can help to develop reliable software.
This work proposes an approach that generates a Kripke structure and Linear Temporal Logic (LTL) formulas from a use case model. A use case model is a de facto industry standard to specify software requirements. The presented approach is a metamodel-based approach. It performs model-to-model transformation. In addition to it, a GUI tool is also developed to support this approach. The user of this approach has to specify the input use case in a proposed template and the tool automatically generates the resultant Kripke structure and LTL formulas. This approach does not require any additional software development artefacts for the transformation. Two pedagogical and two industrial case studies are used to generate the resultant formal artefacts. The proposed approach is also compared with the existing approaches on the basis of the user eorts required to specify informal software requirements, ability to handle use case relationships and usefulness of the generated artefacts. It is found that four existing approaches meet this criteria. Only two out of these approaches are able to handle all use cases of these case studies and examples. Whereas, other two are unable to handle 41 out of 50 input use cases, because these approaches do not handle use case relationships. In addition to it, the existing approaches generate only the behavioural model of the software. None of these approaches generate formal software specications of the software. However, the proposed approach transforms all input use cases. This approach generates a behavioural model along with the formal software specication of a software.