creators_name: Aziz, Benjamin creators_name: Arenas, Alvaro creators_name: Bicarregui, Juan creators_name: Ponsard, Christophe creators_name: Massonet, Philippe creators_id: benjamin.aziz@stfc.ac.uk creators_id: alvaro.arenas@stfc.ac.uk creators_id: juan.bicarregui@stfc.ac.uk creators_id: christophe.ponsard@cetic.be creators_id: philippe.massonet@cetic.be type: conference_item datestamp: 2009-04-20 09:35:14 lastmod: 2010-04-19 15:05:53 metadata_visibility: show corp_creators: e-Science Centre, STFC Rutherford Appleton Laboratory corp_creators: CETIC research centre title: From Goal-Oriented Requirements to Event-B Specifications ispublished: inpress subjects: theory subjects: deploy_method_reqevo subjects: deploy_tooldev_modelc full_text_status: public pres_type: paper abstract: 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. date: 2009-04-06 date_type: published pagerange: 96-105 event_title: First Nasa Formal Method Symposium event_location: Moffett Field, California event_dates: April 6 - 8, 2009 event_type: other refereed: TRUE official_url: http://ti.arc.nasa.gov/event/nfm09/ citation: Aziz, Benjamin and Arenas, Alvaro and Bicarregui, Juan and Ponsard, Christophe and Massonet, Philippe (2009) From Goal-Oriented Requirements to Event-B Specifications. In: First Nasa Formal Method Symposium, April 6 - 8, 2009 , Moffett Field, California . (In Press) document_url: http://deploy-eprints.ecs.soton.ac.uk/91/1/nfm-reqs-eventb.pdf