Marie Farrell

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. Developing Multi-Agent Systems with Degrees of Neuro-Symbolic Integration [A Position Paper] Neuro-symbolic AI for Agent and Multi-Agent systems [NeSyMAS] Workshop at AAMAS 2023. pre-print

MacConville, D., Farrell, M., Luckcuck, M., Monahan, R. CSP2Turtle: Verified Turtle Robot Plans Robotics, 12(2), 62. 2023. Paper and related poster presented at SMC-IT 2023.

Farrell, M., Monahan, R., Power J. F. Journal First: Building Specifications in the Event-B Institution ABZ 2023. slides

MacConville, D., Farrell, M., Luckcuck, M., Monahan, R. Modelling the Turtle Python library in CSP Workshop on Agents and Robots for reliable Engineered Autonomy. 2022.

Luckcuck, M., Taylor, H. M., Farrell, M. An Abstract Architecture for Explainable Autonomy in Hazardous Environments International Requirements Engineering Conference Workshops (RE4ES). 2022.

Ferrando, A., Cardoso, R. C., Farrell, M., Luckcuck, M., Papacchini, F., Fisher, M., Mascardi, V.Bridging the Gap Between Single-and Multi-Model Predictive Runtime Verification Formal Methods in System Design. 2022.

Farrell, M., Monahan, R., Power, J. F. Building Specifications in the Event-B Institution Logical Methods in Computer Science. 2022.

Farrell, M., Luckcuck, M., Sheridan, O., Monahan, R. Towards Refactoring FRETish Requirements NASA Formal Methods Symposium. 2022.

Farrell, M., Mavrakis, N., Ferrando, A., Dixon, C., Gao, Y. Journal First: Formal Modelling and Runtime Verification of Autonomous Grasping for Active Debris Removal. International Conference on Integrated Formal Methods. 2022.

Farrell, M., Mavrakis, N., Ferrando, A., Dixon, C., Gao, Y. Formal Modelling and Runtime Verification of Autonomous Grasping for Active Debris Removal. Frontiers in Robotics and AI. 2022. Paper and related poster presented at SMC-IT 2023.

Luckcuck, M., Farrell, M., Sheridan, O., Monahan, R. A Methodology for Developing a Verifiable Aircraft Engine Controller from Formal Requirements. IEEE Aerospace Conference. 2022.

Farrell, M., Luckcuck, M., Sheridan, O., Monahan, R. FRETting about Requirements: Formalised Requirements for an Aircraft Engine Controller. International Working Conference on Requirements Engineering: Foundation for Software Quality. 2022.

Farrell, M., Luckcuck, M., Pullum, L., Fisher, M., Hessami, A., Gal, D., Murahwi, Z., Wallace, K. Evolution of the IEEE P7009 Standard: Towards Fail-Safe Design of Autonomous Systems. International Symposium on Software Reliability Engineering - Industry Track. 2021.

Farrell, M., Reynolds, C., Monahan, R. Using dafny to solve the VerifyThis 2021 challenges. International Workshop on Formal Techniques for Java-like Programs. Pages 32-38. 2021.

Cardoso, Kourtis, G., Dennis, L. A., Dixon, C., Farrell, M., Fisher, M., Webster, M. A Review of Verification and Validation for Space Autonomous Systems. Current Robotics Reports. Pages 1-11. 2021.

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. An Overview of Verification and Validation Challenges for Inspection Robots. Robotics 10(2). 2021.

Bourbouh, H., Farrell, M., Mavridou, A., Sljivo, I., Brat, G., Dennis, L. A., Fisher, M. Integrating Formal Verification and Assurance: An Inspection Rover Case Study. NASA Formal Methods Symposium. Volume 12673 of LNCS. Pages 53-71. 2021. Poster presented at SMC-IT 2023.

Wu, H., Farrell, M. A formal approach to finding inconsistencies in a metamodel. Software and Systems Modeling. Pages 1-28. 2021.

Farrell, M., Mavrakis, N., Dixon, C., Gao, Y. Formal Verification of an Autonomous Grasping Algorithm. International Symposium on Artificial Intelligence, Robotics and Automation in Space. 2020.

Cardoso, R. C., Dennis, L. A., Farrell, M., Fisher, M., Luckcuck, M. Towards Compositional Verification for Modular Robotic Systems. Workshop on Formal Methods for Autonomous Systems. EPTCS 329. Pages 15-22. 2020.

Cardoso, R. C., Farrell, M., Luckcuck, M., Ferrando, A., Fisher, M. Heterogeneous Verification of an Autonomous Curiosity Rover. NASA Formal Methods Symposium. Volume 12229 of LNCS. Pages 353-360. 2020.

Maple, C., Bradbury, M., Yuan, H., Farrell, M., Dixon, C., Fisher, M., Atmaca, U. I. Security-Minded Verification of Space Systems. IEEE Aerospace Conference. Pages 1-12. 2020.

Farrell, M., Wu, H. When the Student becomes the Teacher. International Workshop on Formal Methods - Fun for Everybody. (to appear) 2019.

Luckcuck, M., Farrell, M., Dennis, L. A., Dixon, C., Fisher, M. A Summary of Formal Specification and Verification of Autonomous Robotic Systems. International Conference on Integrated Formal Methods. Volume 11918 of LNCS. Pages 538-541. 2019.

Farrell, M., Cardoso, R., Dennis, L., Dixon, C., Fisher, M., Kourtis, G., Lisitsa, A., Luckcuck, M., Webster, M. Modular Verification of Autonomous Space Robotics. Assurance of Autonomy for Robotic Space Missions Workshop. 2019.[Link]

Farrell, M., Bradbury, M., Fisher, M., Maple, C. Workshop Report: Space Security Scoping. FAIR-SPACE Technical Report. 2019. [Link]

Farrell, M., Bradbury, M., Yuan, H., Fisher, M., Dennis, L., Dixon, C., Maple, C. Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages. International Conference on Software Engineering and Formal Methods. 2019.

Farrell, M., Luckcuck, M., Dennis, L., Dixon, C., Fisher, M. Formal Specification and Verification of Autonomous Robotic Systems: A Survey. ACM Computing Surveys (CSUR) 52 (5). 2019.[Link to arxiv preprint]

Farrell, M., Luckcuck, M., Fisher, M. Robotics and Integrated Formal Methods: Necessity meets Opportunity. International Conference on Integrated Formal Methods. 2018.

Farrell, M. Event-B in the Institutional Framework: Defining a Semantics, Modularisation Constructs and Interoperability for a Specification Language. PhD Thesis, Department of Computer Science, Maynooth University. 2017.[PDF]

Farrell, M., Monahan, R., Power, J. F. Combining Event-B and CSP: An Institution Theoretic Approach to Interoperability. International Conference on Formal Engineering Methods 2017.

Farrell, M., Monahan, R., Power, J. F. Specification Clones: An empirical study of the structure of Event-B specifications. International Conference on Software Engineering and Formal Methods 2017.

Farrell, M., Monahan, R., Power, J. F. An Institution for Event-B. International Workshop on Algebraic Development Techniques 2016. Volume 10644 of LNCS. Pages 104--119.

Farrell, M., Monahan, R., Power, J. F. Providing a Semantics and Modularisation Constructs for Event-B using Institutions. Workshop on Algebraic Development Techniques 2016.

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]

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

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

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

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




Best Presentation Award at iFM 2018. Paper titled: ''Robotics and Integrated Formal Methods: Necessity meets Opportunity''.

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 provided 4 years of funding to pursue my PhD.

Education




Ph.D. Computer Science. Oct 2013 - 2017. Maynooth University, 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