--- abstract: "In goal-oriented requirements engineering methodologies, goals are structured into refinement\r\ntrees from high-level system-wide goals down to fine-grained requirements assigned to specific software/\r\nhardware/human agents that can realise them. Functional goals assigned to software agents\r\nneed to be operationalised into specification of services that the agent should provide to realise those\r\nrequirements. In this paper, we propose an approach for operationalising requirements into specifications\r\nexpressed in the Event-B formalism. Our approach has the benefit of aiding software designers\r\nby bridging the gap between declarative requirements and operational system specifications in a rigorous\r\nmanner, enabling powerful correctness proofs and allowing further refinements down to the\r\nimplementation level. Our solution is based on verifying that a consistent Event-B machine exhibits\r\nproperties corresponding to requirements." accompaniment: [] book_title: ~ commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: ~ copyright_holders: [] corp_creators: - 'e-Science Centre, STFC Rutherford Appleton Laboratory' - CETIC research centre creators_id: - benjamin.aziz@stfc.ac.uk - alvaro.arenas@stfc.ac.uk - juan.bicarregui@stfc.ac.uk - christophe.ponsard@cetic.be - philippe.massonet@cetic.be creators_name: - family: Aziz given: Benjamin honourific: '' lineage: '' - family: Arenas given: Alvaro honourific: '' lineage: '' - family: Bicarregui given: Juan honourific: '' lineage: '' - family: Ponsard given: Christophe honourific: '' lineage: '' - family: Massonet given: Philippe honourific: '' lineage: '' data_type: ~ date: 2009-04-06 date_type: published datestamp: 2009-04-20 09:35:14 department: ~ dir: disk0/00/00/00/91 divisions: [] edit_lock_since: ~ edit_lock_until: ~ edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 91 event_dates: 'April 6 - 8, 2009 ' event_location: 'Moffett Field, California ' event_title: First Nasa Formal Method Symposium event_type: other exhibitors_id: [] exhibitors_name: [] fileinfo: /style/images/fileicons/application_pdf.png;/91/1/nfm%2Dreqs%2Deventb.pdf full_text_status: public funders: [] id_number: ~ importid: ~ institution: ~ isbn: ~ ispublished: inpress issn: ~ item_issues_comment: [] item_issues_count: 0 item_issues_description: [] item_issues_id: [] item_issues_reported_by: [] item_issues_resolved_by: [] item_issues_status: [] item_issues_timestamp: [] item_issues_type: [] keywords: ~ lastmod: 2010-04-19 15:05:53 latitude: ~ learning_level: ~ longitude: ~ lyricists_id: [] lyricists_name: [] metadata_visibility: show monograph_type: ~ note: ~ num_pieces: ~ number: ~ official_url: http://ti.arc.nasa.gov/event/nfm09/ output_media: ~ pagerange: 96-105 pages: ~ patent_applicant: ~ pedagogic_type: ~ place_of_pub: ~ pres_type: paper producers_id: [] producers_name: [] projects: [] publication: ~ publisher: ~ refereed: TRUE referencetext: ~ related_url_type: [] related_url_url: [] relation_type: [] relation_uri: [] rev_number: 25 series: ~ skill_areas: [] source: ~ status_changed: 2009-04-20 09:35:14 subjects: - theory - deploy_method_reqevo - deploy_tooldev_modelc succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: From Goal-Oriented Requirements to Event-B Specifications type: conference_item userid: 34 volume: ~