Marie Farrell
Royal Academy of Engineering Research Fellow
Department of Computer Science
The University of Manchester
Email: marie.farrell@manchester.ac.uk
My Royal Academy of Engineering Fellowship is entitled "Strong Software Reliability for Autonomous Space Robotics". This work aims to devise new ways of describing, analysing and assuring the autonomous behaviour of robotic space systems. Previously, I was a Senior Post-Doctoral Researcher in the Department of Computer Science at Maynooth University (VALU3S project). This work involved eliciting and verifying requirements for an aircraft engine controller. Before that, I worked on the EPSRC funded FAIR-SPACE Hub and participated in the RAIN and ORCA Hubs. This work focused on using and combining formal methods to reason about and provide certification evidence for robotic systems that are to be deployed in hazardous environments. I received my PhD from Maynooth University in 2017 for my work on defining a semantics, modularisation constructs and interoperability for the Event-B formal specification language using the theory of institutions.
Topics of Interest
- Formal methods and their application to autonomous, automated and/or robotic/aerospace systems
- Integrated formal methods
- Category theory and its use in Computer Science
- Formal semantics of programming and specification languages
Professional Activities
Invited Talk at the University of Southampton: slides
Invited Talk at the University of Lancaster: slides
Engineering The Future at Manchester: slides
Co-Chair of the IEEE International Conference on Space Mission Challenges for Information Technology 2023 and 2024.
Co-Organiser of the VerifyThis 2022 program verification competition.
Co-Chair of the PhD Symposium at the International Conference on Integrated Formal Methods 2022.
Secretary of the Working Group developing the IEEE P7009 Standard on Fail-Safe Design of Autonomous and Semi-Autonomous Systems.
Co-Chair of Workshop on Accelerating the Use of Autonomy on Robotic Space Missions at SMC-IT 2021.
Co-Chair of Workshop on Formal Methods for Autonomous Systems 2019--2023.
Co-Chair of the Logic and Computation Track at the ESSLLI Student Session 2017.
Co-Organiser of Postgraduate Computer Science Seminar Series at Maynooth University until 2018.
Part of the following programme committees: iFM 2019, AAMAS 2019, FTfJP 2019, ECAI 2020, AAAI-20 Programs, AAMAS 2020, FTfJP 2020, FTfJP 2021, AI4Space 2021, AAAI-21, ESEC/FSE Demonstrations 2021, NFM 2022, AAAI-22 Student Abstracts and Posters, AI4Space 2022, FTSCS 2022, AAMAS 2023, NFM 2023, ABZ 2023, FTSCS 2023, iFM 2023, FACS 2023, AREA 2023.
Member of the Autonomy and Verification Network.
PhD Supervision
Publications
Dennis, L. A., Farrell, M., Fisher, M.
MacConville, D., Farrell, M., Luckcuck, M., Monahan, R.
Farrell, M., Monahan, R., Power J. F.
MacConville, D., Farrell, M., Luckcuck, M., Monahan, R.
Luckcuck, M., Taylor, H. M., Farrell, M.
Ferrando, A., Cardoso, R. C., Farrell, M., Luckcuck, M., Papacchini, F., Fisher, M., Mascardi, V.
Farrell, M., Monahan, R., Power, J. F.
Farrell, M., Luckcuck, M., Sheridan, O., Monahan, R.
Farrell, M., Mavrakis, N., Ferrando, A., Dixon, C., Gao, Y.
Farrell, M., Mavrakis, N., Ferrando, A., Dixon, C., Gao, Y.
Luckcuck, M., Farrell, M., Sheridan, O., Monahan, R.
Farrell, M., Luckcuck, M., Sheridan, O., Monahan, R.
Farrell, M., Luckcuck, M., Pullum, L., Fisher, M., Hessami, A., Gal, D., Murahwi, Z., Wallace, K.
Farrell, M., Reynolds, C., Monahan, R.
Cardoso, Kourtis, G., Dennis, L. A., Dixon, C., Farrell, M., Fisher, M., Webster, M.
Fisher, M., Cardoso, R. C., Collins, E. C., Dadswell, C., Dennis, L. A., Dixon, C., Farrell, M., Ferrando, A., Huang, X., Jump, M., Kourtis, G., Lisitsa, A., Luckcuck, M., Luo, S., Page, V., Papacchini, F., Webster, M.
Bourbouh, H., Farrell, M., Mavridou, A., Sljivo, I., Brat, G., Dennis, L. A., Fisher, M.
Wu, H., Farrell, M.
Farrell, M., Mavrakis, N., Dixon, C., Gao, Y.
Cardoso, R. C., Dennis, L. A., Farrell, M., Fisher, M., Luckcuck, M.
Cardoso, R. C., Farrell, M., Luckcuck, M., Ferrando, A., Fisher, M.
Maple, C., Bradbury, M., Yuan, H., Farrell, M., Dixon, C., Fisher, M., Atmaca, U. I.
Farrell, M., Wu, H.
Luckcuck, M., Farrell, M., Dennis, L. A., Dixon, C., Fisher, M.
Farrell, M., Cardoso, R., Dennis, L., Dixon, C., Fisher, M., Kourtis, G., Lisitsa, A., Luckcuck, M., Webster, M.
Farrell, M., Bradbury, M., Fisher, M., Maple, C.
Farrell, M., Bradbury, M., Yuan, H., Fisher, M., Dennis, L., Dixon, C., Maple, C.
Farrell, M., Luckcuck, M., Dennis, L., Dixon, C., Fisher, M.
Farrell, M., Luckcuck, M., Fisher, M.
Farrell, M.
Farrell, M., Monahan, R., Power, J. F.
Farrell, M., Monahan, R., Power, J. F.
Farrell, M., Monahan, R., Power, J. F.
Farrell, M., Monahan, R., Power, J. F.
Farrell, M., Monahan, R., Power, J. F.
Farrell, M.
Farrell, M., Monahan, R., Power, J. F.
Farrell, M., Monahan, R., Power, J. F.
PhD Thesis
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.
Supervisors: Dr. Rosemary Monahan and Dr. James F. Power .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