论文标题
使用形式的自主系统方法：五个用于正式验证的食谱
Using Formal Methods for Autonomous Systems: Five Recipes for Formal Verification
论文作者
论文摘要
正式方法是用于软件设计和工程的基于数学上的技术，它可以对系统行为的明确描述和推理。自主系统使用软件在没有人类控制的情况下做出决策，通常嵌入机器人系统中，通常是安全至关重要的，并且越来越多地被引入日常环境中。自主系统需要强大的开发和验证方法，但是通常会问正式方法：为什么要为自主系统使用正式方法？为了回答这个问题，该立场论文描述了从文献中收集的自主系统正式验证自主系统方面的五个食谱。食谱是形式方法如何成为自治系统开发和验证的有效工具的例子。在设计过程中，它们可以明确描述要求；在开发中，可以根据要求验证形式规格；软件组件可以根据经过验证的规格合成；可以在运行时监视行为，并将其与其原始规范进行比较。现代形式的方法通常包括高度自动化的工具支持，可以详尽地检查系统的状态空间。本文认为，正式方法是安全自主系统开发技术曲目以及其他强大的软件工程技术的强大工具。
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.
