RE2B: Enhancing Correctness of Both Requirements and Design Models

Software requirements are the criteria for the correctness of the software behaviors. How to verify the correctness of the requirements is a big challenge in requirements engineering. Among various requirements approaches, the environment modeling based requirements engineering(EBRE) gains great popularity due to its explicit environment model. However, it still lacks of a formal approach to verify the correctness of the requirements models proposed in EBRE. Event-B is a popular formal method employing step-wise refinement to construct system models and verify their correctness according to the system requirements. This paper combines EBRE with Event-B to merge the advantages of the two methods. On the one hand, we transform the EBRE models to the initial Event-B model to guide the further design and development of the system. On the other hand, the transformed Event-B model can provide formal proof on the consistency of the requirements model. We also implement a plug-in tool on the Rodin platform to realize the automatic transformation from EBRE models to Event-B model and to commit a formal verification on the correctness of the transformed requirements model.