[HTML][HTML] Building traceable Event-B models from requirements
E Alkhammash, M Butler, AS Fathabadi… - Science of Computer …, 2015 - Elsevier
Science of Computer Programming, 2015•Elsevier
Bridging the gap between informal requirements and formal specifications is a key
challenge in systems engineering. Constructing appropriate abstractions in formal models
requires skill and managing the complexity of the relationships between requirements and
formal models can be difficult. In this paper we present an approach that aims to address the
twin challenges of finding appropriate abstractions and managing traceability between
requirements and models. Our approach is based on the use of semi-formal structures to …
challenge in systems engineering. Constructing appropriate abstractions in formal models
requires skill and managing the complexity of the relationships between requirements and
formal models can be difficult. In this paper we present an approach that aims to address the
twin challenges of finding appropriate abstractions and managing traceability between
requirements and models. Our approach is based on the use of semi-formal structures to …
Abstract
Bridging the gap between informal requirements and formal specifications is a key challenge in systems engineering. Constructing appropriate abstractions in formal models requires skill and managing the complexity of the relationships between requirements and formal models can be difficult. In this paper we present an approach that aims to address the twin challenges of finding appropriate abstractions and managing traceability between requirements and models. Our approach is based on the use of semi-formal structures to bridge the gap between requirements and Event-B models and retain traceability to requirements in Event-B models. In the stepwise refinement approach, design details are gradually introduced into formal models. Stepwise refinement allows each requirement to be introduced at the most appropriate stage in the development. Our approach makes use of the UML-B and Event Refinement Structures (ERS) approaches. UML-B provides UML graphical notation that enables the development of data structures for Event-B models, while the ERS approach provides a graphical notation to illustrate event refinement structures and assists in the organisation of refinement levels. The ERS approach also combines several constructor patterns to manage control flows in Event-B. The intent of this paper is to harness the benefits of the UML-B and ERS approaches to facilitate constructing Event-B models from requirements and provide traceability between requirements and Event-B models.
Elsevier
Showing the best result for this search. See all results