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

Luckcuck, Matt ORCID: 0000-0002-6444-9312 (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.

Access the full-text of this item by clicking on the Open Access link.

Text
2012.00856v3.pdf - Author Accepted Manuscript
Download (308kB) | Preview

Official URL: http://dx.doi.org/10.1177/1748006X211034970

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:	Accepted at Journal of Risk and Reliability
Uncontrolled Keywords:	Formal methods, autonomous systems, robotic systems, verification, validation
Divisions:	Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User:	Symplectic Admin
Date Deposited:	28 Jul 2022 15:29
Last Modified:	16 May 2023 20:23
DOI:	10.1177/1748006X211034970
Open Access URL:	https://arxiv.org/abs/2012.00856v3
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3159766