?url_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rft.title=Mapping+Requirements+to+B+models&rft.creator=Jastram%2C+Michael&rft.creator=Leuschel%2C+Michael&rft.creator=Bendisposto%2C+Jens&rft.creator=Russo+Jr%2C+Aryldo+G&rft.subject=Requirements+and+evolution&rft.description=Formal+methods+in+systems+engineering+are+gaining+traction%2C+at+least+in+some+areas.+While+the+formal+specification+process+from+abstraction+via+refinement+to+implementation+is+fairly+well+understood%2C+the+traceability+between+the+initial+user+requirements+and+the+formal+model+is+still+unsatisfying.+There+are+some+promising+attempts+(e.g.+KAOS)+that+inspired+some+of+the+work+done+here.%0D%0A%0D%0AOur+objective+is+to+find+a+practical+way+to+establish+traceability+between+natural+language+requirements+and+B+models.%0D%0A%0D%0AWe+select+a+number+of+existing+methods+and+notations+for+bringing+natural+language+requirements+and+B+specifications+together.++Specifically%2C+we+use+UML-B+for+building+a+data+model%3B+we+use+invariants+(part+of+the+B+method)+to+model+safety+requirements%3B+and+we+use+temporal+expressions+(LTL)+to+model+liveness+requirements.%0D%0A%0D%0AIn+this+paper%2C+we+show+a+pragmatic+way+that+may+lead+to+a+method+for+making+traceability+between+natural+language+requirements+and+B+models+easier+to+understand%2C+maintain+and+validate.&rft.type=Other&rft.type=NonPeerReviewed&rft.format=application%2Fpdf&rft.identifier=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F104%2F1%2F2009-05_Requirements_Traceability.pdf&rft.identifier=++Jastram%2C+Michael+and+Leuschel%2C+Michael+and+Bendisposto%2C+Jens+and+Russo+Jr%2C+Aryldo+G+++Mapping+Requirements+to+B+models.++UNSPECIFIED.++++(Unpublished)++&rft.relation=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F104%2F<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>