---
abstract: "Formal modeling of computing systems yields models that are intended to be correct with respect to the requirements that have been formalized. \r\nThe complexity of typical computing systems can be addressed by formal refinement introducing all the necessary details piecemeal.\r\nWe report on preliminary results that we have obtained for tracing informal natural-language requirements into formal models across refinement levels.\r\nThe approach uses the WRSPM reference model for requirements modeling, and Event-B for formal modeling and formal refinement. \r\nThe combined use of WRSPM and Event-B is facilitated by the rudimentary refinement notion of WRSPM, \r\nwhich provides the foundation for tracing requirements to formal refinements.\r\n\r\nWe assume that requirements are evolving, meaning that we have to cope with frequent changes of the requirements model and the formal model.  \r\nOur approach is capable of dealing with frequent changes, making use of corresponding techniques already built into the Event-B method."
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id:
  - michael@jastram.de
  - sth@ecs.soton.ac.uk
  - leuschel@cs.uni-duesseldorf.de
  - agrj@aes.com.br
creators_name:
  - family: Jastram
    given: Michael
    honourific: ''
    lineage: ''
  - family: Hallerstede
    given: Stefan
    honourific: ''
    lineage: ''
  - family: Leuschel
    given: Michael
    honourific: ''
    lineage: ''
  - family: Russo Jr
    given: Aryldo G
    honourific: ''
    lineage: ''
data_type: ~
date: 2010
date_type: published
datestamp: 2010-07-08 09:48:34
department: ~
dir: disk0/00/00/02/36
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 236
event_dates: 16th-19th August 2010
event_location: 'Edinburgh, UK'
event_title: 'VSTTE’10 Verified Software: Theories, Tools and Experiments'
event_type: conference
exhibitors_id: []
exhibitors_name: []
fileinfo: /style/images/fileicons/application_pdf.png;/236/2/2010%2D03_Formal_Modelling_of_Requirements.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: 'Requirements Traceability, WRSPM, Formal Modeling, Refinement, Event-B'
lastmod: 2010-07-18 22:51:59
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ~
num_pieces: ~
number: ~
official_url: ~
output_media: ~
pagerange: ~
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: 18
series: ~
skill_areas: []
source: ~
status_changed: 2010-07-18 22:51:59
subjects:
  - deploy_method_reqevo
  - deploy_training_rodinplugins
succeeds: 235
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: "An Approach of Requirements Tracing in Formal Refinement\r\n"
type: conference_item
userid: 259
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>