?url_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rft.title=Towards+Automated+Re%EF%AC%81nement%3A+Patterns+in+Event+B+&rft.creator=Iliasov%2C+Alexei&rft.creator=Troubitsyna%2C+Elena&rft.creator=Laibinis%2C+Linas&rft.creator=Romanovsky%2C+Alexander&rft.subject=Composition+and+reuse&rft.subject=Methodology&rft.description=Formal+modelling+is+indispensable+for+engineering+highly+dependable+systems.+However%2C+a+wider+acceptance+of+formal+methods+is+hindered+by+their+insufficient+usability+and+scalability.+In+this+paper%2C+we+aim+at+assisting+developers+in+rigorous+modelling+and+design+by+increasing+automation+of+development+steps.+We+introduce+a+notion+of+re%EF%AC%81nement+patterns+%E2%80%93+generic+representations+of+typical+correctness-preserving+model+transformations.+Our+definition+of+a+re%EF%AC%81nement+pattern+contains+a+description+of+syntactic+model+transformations%2C+as+well+as+the+pattern+applicability+conditions+and+proof+obligations+for+verification+of+correctness+preservation.+This+establishes+a+basis+for+building+a+tool+supporting+formal+system+development+via+pattern+reuse+and+instantiation.+We+present+a+prototype+of+such+a+tool+and+some+examples+of+re%EF%AC%81nement+patterns+for+automated+development+in+the+Event+B+formalism.+%0D%0A&rft.publisher=Technical+Report&rft.date=2009-05-19&rft.type=Monograph&rft.type=NonPeerReviewed&rft.format=application%2Fpdf&rft.identifier=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F106%2F1%2Fmain-ictac2009.pdf&rft.identifier=++Iliasov%2C+Alexei+and+Troubitsyna%2C+Elena+and+Laibinis%2C+Linas+and+Romanovsky%2C+Alexander++(2009)+Towards+Automated+Re%EF%AC%81nement%3A+Patterns+in+Event+B.++Working+Paper.+Technical+Report.++++(Unpublished)++&rft.relation=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F106%2F