RE2B: Enhancing Correctness of Both Requirements and Design Models

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

1 Scopus citations

Abstract

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.

Original languageEnglish
Title of host publicationProceedings - 2021 International Symposium on Theoretical Aspects of Software Engineering, TASE 2021
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages191-198
Number of pages8
ISBN (Electronic)9781665441636
DOIs
StatePublished - Aug 2021
Event15th International Symposium on Theoretical Aspects of Software Engineering, TASE 2021 - Shanghai, China
Duration: 25 Aug 202127 Aug 2021

Publication series

NameProceedings - 2021 International Symposium on Theoretical Aspects of Software Engineering, TASE 2021

Conference

Conference15th International Symposium on Theoretical Aspects of Software Engineering, TASE 2021
Country/TerritoryChina
CityShanghai
Period25/08/2127/08/21

Keywords

  • Environment Modeling based Requirements Engineering
  • Event-B
  • Requirements Verification

Fingerprint

Dive into the research topics of 'RE2B: Enhancing Correctness of Both Requirements and Design Models'. Together they form a unique fingerprint.

Cite this