Generating Logical Specifications from Requirements Models for Deduction-based Formal Verification
This addresses the problem of making deduction-based verification more accessible for software developers, particularly inexperienced users, by automating a key bottleneck, though it appears incremental as it builds on existing UML and workflow pattern techniques.
The paper tackles the difficulty of manually specifying logical specifications for deduction-based formal verification by presenting a method to automatically generate them from requirements models using UML diagrams and workflow patterns, enabling automated extraction and integration with the verification process.
The work concerns automatic generation of logical specifications from requirements models. Logical specifications obtained in such a way can be subjected to formal verification using deductive reasoning. Formal verification concerns correctness of a model behaviour. Reliability of the requirements engineering is essential for all phases of software development processes. Deductive reasoning is an important alternative among other formal methods. However, logical specifications, considered as sets of temporal logic formulas, are difficult to specify manually by inexperienced users and this fact can be regarded as a significant obstacle to practical use of deduction-based verification tools. A method of building requirements models using some UML diagrams, including their logical specifications, is presented step by step. Organizing activity diagrams into predefined workflow patterns enables automated extraction of logical specifications. The crucial aspect of the presented approach is integrating the requirements engineering phase and the automatic generation of logical specifications. A system of the deduction-based verification is proposed. The reasoning process could be based on the semantic tableaux method. A simple yet illustrative example of the requirements elicitation and verification is provided.