?url_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rft.title=Starting+B+Specifications+from+Use+Cases&rft.creator=Russo+Jr%2C+Aryldo+G&rft.creator=de+Sousa%2C+Thiago&rft.subject=Requirements+and+evolution&rft.description=The+B+method+is+gaining+visibility+in+formal+methods+com-+munity+due+to+excellent+support+for+refinement.+However%2C+the+traceability+between+the+requirements+and+the+formal+model+is+still+an+issue+of+this+method.+On+the+other+hand%2C+use+cases+have+become+the+informal+industry+standard+for+mapping+functional+requirements%2C+describing+the+system's+behavior+using+natural+language.+In+this+paper+we+show+how+controlled+use+cases+can+be+used+as+a+guideline+for+starting+B+specifications.+In+other+words%2C+our+approach+presents+how+a+transaction%2C+which+is+defined+as+an+atomic+part+of+the+use+case+scenario%2C+can+be+mapped+as+a+B+operation%2C+providing+a+practical+way+to+establish+traceability+between+functional+re-+quirements+and+formal+models.&rft.date=2010&rft.type=DEPLOY+Associate+Item&rft.type=PeerReviewed&rft.format=application%2Fpdf&rft.identifier=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F211%2F1%2Fpaper_63-3.pdf&rft.identifier=++Russo+Jr%2C+Aryldo+G+and+de+Sousa%2C+Thiago++(2010)+Starting+B+Specifications+from+Use+Cases.++%5BDEPLOY+Associate+Item%5D++++(Unpublished)++&rft.relation=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F211%2F<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>