Marie Farrell

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. Modularising and Promoting Interoperability for Event-B Specifications using Institution Theory European Summer School in Logic, Language and Information. 2016. [Extended Abstract] [Poster]

[2] Farrell, M. Using the Theory of Institutions to Integrate Software Models via Refinement Doctoral Symposium at Integrated Formal Methods. 2016. [PDF]

[3] Farrell, M., Monahan, R., Power, J. F. A Logical Framework for Integrating Software Models via Refinement British Colloquium for Theoretical Computer Science. 2016. Abstracts published in the Bulletin of EATCS

[4] Farrell, M., Monahan, R., Power, J. F. An Approach to Integrating Software Models via Refinement ACM womENcourage. 2014. [PDF]

Related Presentations




Refinement and Institutions. This talk was delivered as part of "JML: Advancing Specification Language Methodologies", a workshop held at Lorentz Center, Leiden, Netherlands. 2015. [Slides]

An Analysis of Refinement Caluli. This talk was delivered as part of the Computer Science Postgraduate Workshop at Maynooth University. 2015. [Slides]

Examining Refinement: Theory, Tools and Mathematics This talk was given during a trip to the MOSEL research group at INRIA, Nancy, France. 2015. [Slides]

Research Overview and General Refinement This talk was delivered during a meeting of the Principles of Programming research group at Maynooth University. 2014. [Slides]

An Introduction to Back's Refinement Calulus This talk was delivered during a meeting of the Principles of Programming research group at Maynooth University. 2014. [Slides]

An Introduction to Refinement This talk was delivered during a meeting of the Principles of Programming research group at Maynooth University. 2014. [Slides]

A Logical Framework for Integrating Software Models via Refinement This talk was delivered as part of the Computer Science Postgraduate Workshop at Maynooth University. 2014. [Slides]

Communicating Sequential Processes This talk was delivered during a meeting of the Principles of Programming research group at Maynooth University. 2014. [Slides]

Denotational Semantics This talk was delivered during a meeting of the Principles of Programming research group at Maynooth University. 2013. [Slides]

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




Intel Medal for Best Final Year Student in Computer Science. 2013. National University of Ireland Maynooth

Government of Ireland Postgraduate Scholarship. 2013. Awarded by the Irish Research Council 2013, this provides 4 years of funding to pursue my PhD.

Education




Ph.D. Computer Science. Oct 2013 - Current. National University of Ireland Maynooth.

B.Sc. Science (Double Honours Computer Science and Applied Mathematics). Sept 2009 - Sept 2013 1st class honours. National University of Ireland Maynooth. Project Supervisor: Dr. Rosemary Monahan