To Enable Formal Verification of Semi-formal Requirements by Using Pre-defined Template and Mapping Rules to map to Promela Specification to Reduce Rework

摘要

Gap has always been found between semi-formal requirements and formal specification. Semi-formal or informal requirements are not able to do formal verification as imprecise and ambiguity is always found. The proposed research is to carry out the mapping of semi-formal requirements to Promela (Process Meta Language) specification in order to enable early verification before the requirements analysis process take place and to obtain highly accurate and complete requirements specification. The proposed solutions include a set of pre-define requirements templates that helps analysts to collect requirements and a set of mapping rules to bridge semi-formal and formal specification. The inputs are a set of semi-formal requirements specifications called Swimlane Domain-specific Requirements Language based on business processes, business actor, flow of processes and simple formula or logics within a process. The target language is Promela, a Process Meta language that can be verified using SPIN (Simple Promela Interpreter) tool to perform formal verification. Inconsistency of requirements will be identified before the inputs are mapped to Promela language. The supporting tool will be included and tested with a group of novice users by applying different formalization strategies like generation of OCL (Object Constraint Language) specification from UML (Unified Modeling Language) diagram set, generation of Z specification from UML and the proposed solution to measure the hours required to finalized requirements, accuracy of the generated specification and the completeness of requirements comparing to the prepared requirements set for measuring purpose.