PublicaĆ§Ć£o
Code generation for event-B
| datacite.subject.fos | Engenharia e Tecnologia::Engenharia EletrotĆ©cnica, EletrĆ³nica e InformĆ”tica | pt_PT |
| dc.contributor.advisor | CataƱo Collazos, Nestor | |
| dc.contributor.author | Rivera ZĆŗƱiga, Victor Alfonso | |
| dc.date.accessioned | 2017-03-10T16:05:48Z | |
| dc.date.available | 2017-04-28T00:30:09Z | |
| dc.date.issued | 2014-11-14 | |
| dc.description.abstract | Stepwise reļ¬nement 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 reļ¬nement a model starts with an abstraction of the system and more details are added through reļ¬nements. Each reļ¬nement 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 beneļ¬t 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 beneļ¬ts of both? This thesis answers this question by translating the stepwise reļ¬nement method with EventB to Design-by-Contract with Java and JML, so users can take full advantage of both formal approaches without losing their beneļ¬ts. 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 ļ¬nal 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.tid | 101383282 | pt_PT |
| dc.identifier.uri | http://hdl.handle.net/10400.13/1464 | |
| dc.language.iso | eng | pt_PT |
| dc.subject | Reļ¬nement calculus | pt_PT |
| dc.subject | Event-B | pt_PT |
| dc.subject | Design-by-contract | pt_PT |
| dc.subject | Java | pt_PT |
| dc.subject | JML | pt_PT |
| dc.subject | EventB2Java | pt_PT |
| dc.subject | Informatics Engineering, specialty in Software Engineering | pt_PT |
| dc.subject | . | pt_PT |
| dc.subject | Faculdade de CiĆŖncias Exatas e da Engenharia | |
| dc.title | Code generation for event-B | pt_PT |
| dc.type | doctoral thesis | |
| dspace.entity.type | Publication | |
| oaire.awardURI | info:eu-repo/grantAgreement/FCT/3599-PPCDT/PTDC%2FEIA-CCO%2F105034%2F2008/PT | |
| oaire.fundingStream | 3599-PPCDT | |
| person.familyName | Rivera | |
| person.givenName | Victor | |
| person.identifier.orcid | 0000-0002-1946-8979 | |
| project.funder.identifier | http://doi.org/10.13039/501100001871 | |
| project.funder.name | FundaĆ§Ć£o para a CiĆŖncia e a Tecnologia | |
| rcaap.rights | openAccess | pt_PT |
| rcaap.type | doctoralThesis | pt_PT |
| relation.isAuthorOfPublication | 94069578-2d56-4b93-a990-ae8123372e66 | |
| relation.isAuthorOfPublication.latestForDiscovery | 94069578-2d56-4b93-a990-ae8123372e66 | |
| relation.isProjectOfPublication | c3cc7231-f884-487a-bb80-f4ba38aa57af | |
| relation.isProjectOfPublication.latestForDiscovery | c3cc7231-f884-487a-bb80-f4ba38aa57af | |
| thesis.degree.name | Doctorate in Informatics Engineering, specialty in Software Engineering | pt_PT |