?url_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rft.title=A+Basis+for+Feature-Oriented+Modelling+in+Event-B&rft.creator=Sorge%2C+Jennifer&rft.creator=Poppleton%2C+Michael&rft.creator=Butler%2C+Michael&rft.subject=Event-B&rft.subject=Composition+and+reuse&rft.description=Feature-oriented+modelling+is+a+well-known+approach+for+Software+Product+%0D%0ALine+(SPL)+development.+It+is+a+widely+used+method+when+developing+groups+of+%0D%0Arelated+software.+With+an+SPL+approach%2C+the+development+of+a+software+product+%0D%0Ais+quicker%2C+less+expensive+and+of+higher+quality+than+a+one-o%EF%AC%80+development+since+%0D%0Amuch+e%EF%AC%80ort+is+re-used.+However%2C+this+approach+is+not+common+in+formal+methods+%0D%0Adevelopment%2C+which+is+generally+high+cost+and+time+consuming%2C+yet+crucial+in+%0D%0Athe+development+of+critical+systems.+With+the+increase+of+more+complex+critical+%0D%0Asystems%2C+it+becomes+more+important+to+apply+formal+methods+to+the+development+%0D%0Acycle%2C+and+we+propose+a+method+that+allows+the+application+of+SPL+development+%0D%0Atechniques+to+formal+methods.+This+results+in+faster+and+cheaper+development+of+%0D%0Aformal+systems.+%0D%0AOur+method+combines+Event-B+%5B1%5D+and+feature+models+%5B2%5D.+A+feature+in+a+%0D%0Afeature+model+represents+a+requirement+of+the+product+family+and+is+formally+%0D%0Adescribed+in+Event-B+using+special+feature+modelling+patterns.+A+feature+repre-+%0D%0Asented+in+Event-B+is+referred+to+as+component.+We+develop+composition+rules%2C+%0D%0Awhich+allow+components+to+be+composed.+Special+composition+proof+obligations+%0D%0Aallow+the+veri%EF%AC%81cation+of+the+composition.+%0D%0AThe+feature+model+is+formed+by+features+which+may+be+associated+with+Event-+%0D%0AB+components.+A+subset+of+features+from+the+feature+model+can+be+selected+to+%0D%0Aform+a+feature+model+instance%2C+thereby+selecting+several+of+these+Event-B+com-+%0D%0Aponents.+These+components+are+composed+pair-wise%2C+and+composition+POs+can+%0D%0Abe+discharged+to+prove+properties+and+to+ensure+consistency+of+the+composition.+%0D%0AThe+%EF%AC%81nal+Event-B+machine+represents+the+formal+speci%EF%AC%81cation+which+is+associated+%0D%0Awith+the+feature+model+instance+and+is+obtained+by+composing+these+components.+%0D%0AThe+motivation+of+our+work+is+to+allow+product+line+development+for+critical+%0D%0Asystems.+We+use+traditional+product+line+methods%2C+i.e.+feature+modelling%2C+and+%0D%0Alink+it+with+the+formal+method+Event-B.+%0D%0AFuture+work+is+focussed+on+amending+feature+diagrams+to+re%EF%AC%82ect+Event-B+%0D%0Acomponents+more+precisely.+Re%EF%AC%81nement+patterns+will+also+be+addressed.+%0D%0A&rft.publisher=Springer&rft.date=2010-02&rft.type=Other&rft.type=NonPeerReviewed&rft.format=application%2Fpdf&rft.identifier=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F252%2F1%2Fpaper_53-1.pdf&rft.identifier=++Sorge%2C+Jennifer+and+Poppleton%2C+Michael+and+Butler%2C+Michael++(2010)+A+Basis+for+Feature-Oriented+Modelling+in+Event-B.++Springer%2C+ABZ2010.+++++&rft.relation=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F252%2F<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>