Deduction-Based Formal Verification of Requirements Models with Automatic Generation of Logical Specifications

This work concerns requirements gathering and their formal verification using deductive approach. The approach is based on temporal logic and the semantic tableaux reasoning method. Requirements elicitation is carried out with some UML diagrams. A use case, its scenario and its activity diagram may be linked to each other during the process of gathering requirements. Activities are identified in the use case scenario and then their workflows are modeled using the activity diagram. Organizing the activity diagram workflows into design patterns is crucial and enables generating logical specifications in an automated way. Temporal logic specifications, formulas and properties are difficult to specify by inexperienced users and this fact can be a significant obstacle to the practical use of deduction-based verification tools. The approach presented in this paper attempts to overcome this problem. Automatic transformation of workflow patterns to temporal logic formulas considered as a logical specification is defined. The architecture of an automatic generation and deduction-based verification system is proposed.