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.
翻译:正规方法是软件设计和工程的数学基础技术,有助于对系统的行为进行明确的描述和推理; 自主系统使用软件,在没有人控制的情况下作出决定,往往嵌入机器人系统,往往具有安全性,而且越来越多地引入日常环境; 自主系统需要强有力的开发和核查方法,但正规方法从业人员经常被问到:为什么使用正规的自动系统方法? 为了回答这个问题,本立场文件介绍了从文献中收集的五种正式核实自主系统各个方面的秘方; 预言是正规方法如何成为开发和核查自主系统的有效工具的范例; 设计期间,它们使人们能够明确描述各种要求; 开发过程中,正式的规格可以根据要求进行核查; 软件组件可以根据经核实的规格进行合成; 行为可以在运行时加以监测,并与原始规格进行比较; 现代正规方法通常包括高度自动化的工具支持,以便能够彻底检查系统的状态空间; 本文指出,正规方法是安全自主系统开发技术的有力工具。