From goal-oriented requirements to Event-B specifications

Benjamin Aziz, A. Arenas, J. Bicarregui, C. Ponsard, P. Massonet

Research output: Contribution to conferencePaperpeer-review

82 Downloads (Pure)


In goal-oriented requirements engineering methodologies, goals are structured into refinement trees from high-level system-wide goals down to fine-grained requirements assigned to specific software/ hardware/human agents that can realise them. Functional goals assigned to software agents need to be operationalised into specification of services that the agent should provide to realise those requirements. In this paper, we propose an approach for operationalising requirements into specifications expressed in the Event-B formalism. Our approach has the benefit of aiding software designers by bridging the gap between declarative requirements and operational system specifications in a rigorous manner, enabling powerful correctness proofs and allowing further refinements down to the implementation level. Our solution is based on verifying that a consistent Event-B machine exhibits properties corresponding to requirements.
Original languageEnglish
Publication statusPublished - 2009
EventFirst Nasa Formal Method Symposium - , United States
Duration: 6 Apr 20088 Apr 2008


ConferenceFirst Nasa Formal Method Symposium
Abbreviated titleNFM 2009
Country/TerritoryUnited States


Dive into the research topics of 'From goal-oriented requirements to Event-B specifications'. Together they form a unique fingerprint.

Cite this