Marie Farrell
Ph.D. Student
Principles of Programming Research Group
Department of Computer Science
National University of Ireland Maynooth
Email: mfarrell@cs.nuim.ie
Research
I am a PhD student in the Department of Computer Science at Maynooth University. The working title of my PhD thesis is "A Logical Framework for Integrating Software Models via Refinement". My supervisors are Dr. Rosemary Monahan and Dr. James F. Power . The abstract is as follows:
A software system is a model of a real-world entity or process, which must accurately represent relevant properties from the domain of application, as well as addressing concerns such as robustness, correctness and performance. Modern software development focuses on model-driven engineering: the construction, maintenance and integration of software models, ranging from formal design documents through to program code. Each model of a language, formalism and tools. Thus a central question in software development is how we can map between these different models while preserving their semantics and other relevant properties. In particular, we ask how we can correctly combine information from models which focus on different aspects of the software system, so that the software system as a whole can be modelled through their integration.
In software development it is common to model software at different levels of abstraction, starting with a very high level abstract specification and finishing with a detailed concrete implementation. In formal software engineering we can map between these levels of abstraction in a verifiable way through a process known as refinement. In contrast to the approach used in model-driven engineering, refinement typically happens within a single modelling language. The goal of this project is to fully integrate this process of formal refinement into the model-driven engineering approach so that models expressed in different modelling languages, formalisms and tools can be combined within one formal framework in a provable correct way. The resulting framework will support the sharing of refinement steps, and their associated proofs, between different modelling environments. The impact will be an improved software development process which allows the integration of software models, which focus on different aspects of the software, modelled at different levels of abstraction. The overall consequence will be the provision of a solid mathematical foundation for Model Driven Engineering.
Funding
This project is funded by the Irish Research Council and supported by the John & Pat Hume Scholarship. At various stages, travel has been supported by ACM-W, CAV Mentoring Workshop, VerifyThis and ESSLLI Student Scholarship.
EVT: An institution for Event-B
A formulation of the Event-B formal specification language in terms of the theory of institutions is available here. This description of Event-B allows us to exploit the specification-building operations of this theory to modularise Event-B specifications. A case study of a traffic-light simulation is presented to illustrate our approach. The files containing the Event-B code for this case study and the modularised version can be found below:
Related Publications
[1] Farrell, M., Monahan, R., Power, J. F.
[2] Farrell, M., Monahan, R., Power, J. F.
[3] Farrell, M., Monahan, R., Power, J. F.
[4] Farrell, M., Monahan, R., Power, J. F.
[5] Farrell, M., Monahan, R., Power, J. F.
[6] Farrell, M.
[7] Farrell, M., Monahan, R., Power, J. F.
[8] Farrell, M., Monahan, R., Power, J. F.
Related Presentations
Other Projects
Refining Software Specifications to Reliable Implementations (Final Year Project)
This project is based on the Industrial strength Event B specification language and its associated tool-set Rodin. The project analyses the Rodin software development proof support which guarantees the correctness of an implementation with respect to its specification. The aim of this project was to provide a more user friendly proof output which will be used to train existing software engineers on how to integrate safety and correctness properties into their development. The target user audience is developers of safety critical software. Formal software development aims to prevent disasters like ARIANE 5 from recurring. By making tools like the Rodin Platform more accessible and friendly to the non-familiar user they become more accessible to companies in industry who may be trying to introduce aspects of formal software development into their software development processes. The solution presented in this project attempts to somewhat bridge the gap between programmer and mathematician. It is clear from the test results that the developed plugin improves the usability of the Rodin Platform. By reducing the ambiguity of the current proof tree, the Rodin Platform is now more accessible to those who may not be well versed in the notion of formal mathematical proof in the field of set theory.
Imagine Cup 2012
In 2012 my team (3 students) won the Irish finals of the Microsoft Imagine Cup Competition Microsoft then funded our representation of Ireland at the world finals of this prestigious student technology competition in Sydney, Australia. Our project "doctek" built a system for managing Multiple Sclerosis. Using the latest mobile technologies we developed a patient app that provides a medicinal reminder and a symptom log which operates solely on one-touch interactions. By using cloud services, not only can patient accounts be synchronised across their devices, but the recorded information can be securely accessed by their doctor. With our technology, statistical and graphical overviews can be provided to the medical professional and background algorithms can detect trends of symptoms of the patients’ progress that are indicative of a relapse, and discreetly alert the doctor that the patient may require attention. Current version of "Marie's App"
SPUR 2012
In 2012 I was awarded a research scholarship under the NUI Maynooth SPUR programme as the nominee of the Department of Computer Science. This is a competitive university-wide programme designed specifically to give undergraduate students experience in working in a research environment. The scholarship funding provided for six weeks research work in close collaboration with the Principles of Programming (POP) research group . This internship was based in the area of software verification specifically formal modelling. The aim of this project was to provide a case study of a metamodel based translation from Event B to Boogie2. The POP Research Group at NUI Maynooth is currently developing a framework to facilitate the process of translation into Boogie2, and my project provided a case study of its use. Translating Event B to Boogie2 at the source code level allows us to automate the proving experience and simplify the process for the user. The POP group are using metamodelling as their approach to translation. The results have shown that the developed product provides a systematic way of translating Event B to Boogie2. It is in fact so systematic that it can be easily reproduced. As a result of the logical nature of this translation, the methodology can be repeated for many similar languages in the field of Software Verification. Upon completion of this internship I constructed a technical report based on this research entitled "A Metamodel based translation from Event B to Boogie2".
I also, took part in the verification competition "Verify This" 2012 that was held at the international "Formal Methods" conference in Paris. I was the only undergraduate to take part in the competition and the language I used was the Dafny verification language. My teammate was a PhD student who is a member of the POP group at NUI Maynooth. The competition entailed providing verified solutions to three questions in the language of choice in a set amount of time.
Awards
Education