Correctness Verification Of EBRE Model Based On Event-B

Requirements analysis plays a very important role in software engineering.It plays a guiding role in design,and it is a key process in software engineering.The correctness of requirements analysis is directly related to the efficiency and quality of the developed system.Among various requirements approaches,the environment modeling based requirements engineering(EBRE),which proposed by Jin,gains greatly popularity because of its environment perspective.This method explicitly models the interactive environment,and provides a systematic process and requirements model for requirements capture and analysis based on the environment model.How to verify the correctness of EBRE model is currently one of the issue of concern.At present,there are corresponding tools to verify the integrity of the EBRE model based on the environmental ontology,but there is lack of formal proof,that the correctness of requirements model cannot be guaranteed at the level of mathematical logic proof.Event-B,as a typical formal method,is based on set theory and first-order logic to perform formal modeling and verification in a refinement manner,and verify its correctness according to system requirements.It can be used as an approach to verifying the correctness of the EBRE requirements model.We combine EBRE with Event-B to complement each other,and propose the correctness verification approach of the EBRE requirements model based on Event-B.We transform the EBRE models to the abstract Event-B model to guide the further design and development of the system.The transformed Event-B model can provide formal proof on the consistency of the requirements model.On this basis,we implemented an automated transformation tool from the EBRE model to the Event-B model,and released it in the form of the plug-in on the Rodin platform,so as to realize the automatic verification of the correctness of the EBRE model.The main work and contributions are as follows:1.The transformation from EBRE requirements model to Event-B model: By analyzing the correspondence between the EBRE model elements and the Event-B model elements,we define a set of transformation rules to transform the EBRE requirements model to the Event-B model,and ensure that the EBRE requirements model is consistent with the transformed Event-B model in semantic.2.The verification on the correctness of requirements model: The transformed Event-B model will generate proof obligations.The automatic theorem proof mechanism of the Rodin platform can be carried out to verify the correctness of the system and the satisfiability of requirements.By analyzing the one-to-one correspondence between the proof obligations and the properties to be satisfied in the requirements model,the Event-B verification mechanism is applied to the correctness verification of the requirements model to verify the correctness of the requirements.3.The model automatic transformation plug-in tool for Rodin platform: Based on the methodology of the transformation from EBRE requirements model to Event-B model and the correctness verification of EBRE requirements model,we realize the plug-in tool for automatic transformation from requirements model to the Event-B model,thereby providing technical support for the verification of the correctness of the requirements model.