Proposal to Improve the Requirements Process through Formal Verification using Deductive Approach

摘要

The work concerns gathering requirements and their formal verification using deductive approach. This approach is based on the semantic tableaux reasoning method and temporal logic. The semantic tableaux method is quite intuitive and has some advantages over traditional deduction strategies. System requirements are gathered using some UML diagrams. Requirements engineering based on formal analysis and verification might play an essential role in producing the correct software since this approach increases reliability and trust in software. Deductive inference is always the most natural for human beings and is used intuitively in everyday life. A use case, its scenario and its activity diagram may be linked to each other during the process of gathering requirements. When activities and actions are identified in the use case scenario then their workflows are modeled using the activity diagram. Organizing the activity diagram workflows into design patterns enables the automation of the process of generating logical specifications. The automation of this process is crucial and constitutes a challenge in the whole deductive approach. Temporal logic properties and formulas may be 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 is proposed. These formulas constitute logical specifications of requirements models. The architecture of an automatic and deduction-based verification system is proposed. Applying this innovative concept results in the reduction of software development costs as some errors might be addressed in the software requirements phase and not in the implementation or testing phases.