Repository logo
 
Publication

Code generation for event-B

datacite.subject.fosEngenharia e Tecnologia::Engenharia Eletrotécnica, Eletrónica e Informáticapt_PT
dc.contributor.advisorCataño Collazos, Nestor
dc.contributor.authorRivera Zúñiga, Victor Alfonso
dc.date.accessioned2017-03-10T16:05:48Z
dc.date.available2017-04-28T00:30:09Z
dc.date.issued2014-11-14
dc.description.abstractStepwise refinement and Design-by-Contract are two formal approaches for modelling systems. These approaches are widely used in the development of systems. Both approaches have (dis-)advantages: in stepwise refinement a model starts with an abstraction of the system and more details are added through refinements. Each refinement must be provably consistent with the previous one. Hence, reasoning about abstract models is possible. A high level of expertise is necessary in mathematics to have a good command of the underlying languages, techniques and tools, making this approach less popular. Design-by-Contract, on the other hand, works on the program rather than the program model, so developers in the software industry are more likely to have expertise in it. However, the benefit of reasoning over more abstract models is lost. A question arises: is it possible to combine both approaches in the development of systems, providing the user with the benefits of both? This thesis answers this question by translating the stepwise refinement method with EventB to Design-by-Contract with Java and JML, so users can take full advantage of both formal approaches without losing their benefits. This thesis presents a set of syntactic rules that translates Event-B to JML-annotated Java code. It also presents the implementation of the syntactic rules as the EventB2Java tool. We used EventB2Java to translate several Event-B models. The tool generated JML-annotated Java code for all the considered Event-B models that serve as final implementation. We also used EventB2Java for the development of two software applications. Additionally, we compared EventB2Java against two other tools that also generate Java code from Event-B models. EventB2Java enables users to start the software development process in Event-B, where users can model the system and prove its consistency, to then transition to JML-annotated Java code, where users can continue the development process.pt_PT
dc.identifier.tid101383282pt_PT
dc.identifier.urihttp://hdl.handle.net/10400.13/1464
dc.language.isoengpt_PT
dc.subjectRefinement calculuspt_PT
dc.subjectEvent-Bpt_PT
dc.subjectDesign-by-contractpt_PT
dc.subjectJavapt_PT
dc.subjectJMLpt_PT
dc.subjectEventB2Javapt_PT
dc.subjectInformatics Engineering, specialty in Software Engineeringpt_PT
dc.subject.pt_PT
dc.subjectFaculdade de Ciências Exatas e da Engenharia
dc.titleCode generation for event-Bpt_PT
dc.typedoctoral thesis
dspace.entity.typePublication
oaire.awardURIinfo:eu-repo/grantAgreement/FCT/3599-PPCDT/PTDC%2FEIA-CCO%2F105034%2F2008/PT
oaire.fundingStream3599-PPCDT
person.familyNameRivera
person.givenNameVictor
person.identifier.orcid0000-0002-1946-8979
project.funder.identifierhttp://doi.org/10.13039/501100001871
project.funder.nameFundação para a Ciência e a Tecnologia
rcaap.rightsopenAccesspt_PT
rcaap.typedoctoralThesispt_PT
relation.isAuthorOfPublication94069578-2d56-4b93-a990-ae8123372e66
relation.isAuthorOfPublication.latestForDiscovery94069578-2d56-4b93-a990-ae8123372e66
relation.isProjectOfPublicationc3cc7231-f884-487a-bb80-f4ba38aa57af
relation.isProjectOfPublication.latestForDiscoveryc3cc7231-f884-487a-bb80-f4ba38aa57af
thesis.degree.nameDoctorate in Informatics Engineering, specialty in Software Engineeringpt_PT

Files

Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
DoutoramentoRiveraZuniga.pdf
Size:
1.26 MB
Format:
Adobe Portable Document Format
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.71 KB
Format:
Item-specific license agreed upon to submission
Description: