My publication and/or reviewing records are available on the following sites.
Automated Aircraft Control Systems
I’m currently working as a Post-Doctoral Researcher at at Maynooth University, Ireland. I’m researching formal verification techniques for automated aircraft engine control systems, as part of the the Verification and Validation of Automated Systems’ Safety and Security (VALU3S) project. My work on this project started with an extensive survey paper of formal verification for aerospace systems, and focusses on integrating formal methods with the Simulink models provided by the project’s use case provider.
Autonomous Robots in Hazardous Environments
Most of my work in this job was for the Robotics and AI in Nuclear (RAIN) Hub. Other colleagues were involved in the the hubs for offshore, and space, so some of my collaborative work crossed over to those domains too. These environments are remote and hazardous to humans, so robotic systems deployed there require a high level of autonomy and rigorous verification.
My work on this project began with an extensive survey paper, and then focussed on linking heterogeneous verification approaches applied across an autonomous software system, and runtime verification of an autonomous system’s behaviour. I also lead a collaboration with the UK’s Office for Nuclear Regulation on developing guidance for developers of autonomous systems that ensures their systems are amenable to robust verification and can provide useful assurance evidence.
During this job I also helped setup the research group (now network) website alongside Rafael Cardoso, and was ‘volunteered’ to setup and run a Twitter account for the group (now network). Most of the activities we did for these projects got tweeted about, and can be found under #HazardousHubs.
My research interests include formal modelling, model checking, safety-critical systems, and programming. My PhD relates to formalising Safety-Critical Java (SCJ) using the state-rich process algebra Circus, which combines elements of Z and CSP. I was supervised jointly by Professors Ana Cavalcanti and Andy Wellings at the University of York.
SCJ adopts a new programming paradigm for applications that must be certified. SCJ programs have a specific concurrent design and use region-based memory management (instead of garbage collection); specialised virtual machines are available to execute SCJ programs. It is organised into three compliance levels, of ascending complexity. My PhD focuses on the most complex compliance level, the programs of which are highly concurrent, potentially multi-processor, and make use of suspension and a variety of release patterns. My PhD provides the most complex compliance level of SCJ with its first semantics, enables further integration with other Circus semantics for SCJ, and provides automatic translation from SCJ to our model.
A copy of my PhD thesis can be found on the White Rose repository. The slides for my Thesis Seminar, which is a presentation of my entire thesis work given just before the final hand in, can be downloaded here
Publications and Presentations
You can find external lists of my publications on my dblp page or my google scholar page. My thesis work produced the list of publications below, which also shows links to the papers and slide (where available).
- Farrell, M., Luckcuck, M., and Fisher, M. (2018). Robotics and Integrated Formal Methods: Necessity meets Opportunity. In Integrated Formal Methods IFM 2018. Lecture Notes in Computer Science, vol 11023. https://doi.org/10.1007/978-3-319-98938-9_10
- Luckcuck, M., Cavalcanti, A., and Wellings, A. (2016). A Formal Model of the Safety-Critical Java Level 2 Paradigm. In Proceedings of the 12th International Conference on Integrated Formal Methods - Volume 9681 (pp. 226–241). New York, NY, USA: Springer-Verlag New York, Inc. http://doi.org/10.1007/978-3-319-33693-0_15
- Luckcuck, M., Wellings, A., and Cavalcanti, A. (2017). Safety-Critical Java: level 2 in practice. Concurrency and Computation: Practice and Experience, http://doi.org/10.1002/cpe.3951
- Luckcuck, M. (2015). A Formal Model for the SCJ Level 2 Paradigm. In Aichernig and B. Alessandro (Eds.), Doctoral Symposium of Formal Methods 2015 (pp. 45–48).
- Wellings, A., Luckcuck, M., and Cavalcanti, A. (2013). Safety-critical Java level 2: motivations, example applications and issues. In Proceedings of the 11th International Workshop on Java Technologies for Real-time and Embedded Systems (pp. 48–57). New York, NY, USA: ACM. https://doi.org/10.1145/2512989.2512991
- Certifiable Java for Embedded Systems (CJ4ES)
- Efficient Model Checking in FDR
- Using Circus to Verify Safety-Critical Java Level 2 Programs