MURAL - Maynooth University Research Archive Library



    Using formal methods for autonomous systems: Five recipes for formal verification


    Luckcuck, Matt (2023) Using formal methods for autonomous systems: Five recipes for formal verification. Proceedings of the Institution of Mechanical Engineers, Part O: Journal of Risk and Reliability, 237 (2). pp. 278-292. ISSN 1748-006X

    [img]
    Preview
    Download (308kB) | Preview


    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...



    Add this article to your Mendeley library


    Abstract

    Formal Methods are mathematically-based techniques for software design and engineering, which enable the unambiguous description of and reasoning about a system’s behaviour. Autonomous systems use software to make decisions without human control, are often embedded in a robotic system, are often safety-critical, and are increasingly being introduced into everyday settings. Autonomous systems need robust development and verification methods, but formal methods practitioners are often asked: Why use Formal Methods for Autonomous Systems? To answer this question, this position paper describes five recipes for formally verifying aspects of an autonomous system, collected from the literature. The recipes are examples of how Formal Methods can be an effective tool for the development and verification of autonomous systems. During design, they enable unambiguous description of requirements; in development, formal specifications can be verified against requirements; software components may be synthesised from verified specifications; and behaviour can be monitored at runtime and compared to its original specification. Modern Formal Methods often include highly automated tool support, which enables exhaustive checking of a system’s state space. This paper argues that Formal Methods are a powerful tool for the repertoire of development techniques for safe autonomous systems, alongside other robust software engineering techniques.

    Item Type: Article
    Additional Information: Cite as: 1. Luckcuck M. Using formal methods for autonomous systems: Five recipes for formal verification. Proceedings of the Institution of Mechanical Engineers, Part O: Journal of Risk and Reliability. 2023;237(2):278-292. doi:10.1177/1748006X211034970
    Keywords: Autonomous systems; automated tool support; software engineering techniques
    Academic Unit: Faculty of Science and Engineering > Computer Science
    Item ID: 17468
    Identification Number: https://doi.org/10.1177/1748006X211034970
    Depositing User: Mr Matthew Luckcuck
    Date Deposited: 31 Aug 2023 09:19
    Journal or Publication Title: Proceedings of the Institution of Mechanical Engineers, Part O: Journal of Risk and Reliability
    Publisher: Sage Journals
    Refereed: Yes
    URI:
    Use Licence: This item is available under a Creative Commons Attribution Non Commercial Share Alike Licence (CC BY-NC-SA). Details of this licence are available here

    Repository Staff Only(login required)

    View Item Item control page

    Downloads

    Downloads per month over past year

    Origin of downloads