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.


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

0
下载
关闭预览

相关内容

Linux导论,Introduction to Linux,96页ppt
专知会员服务
78+阅读 · 2020年7月26日
Stabilizing Transformers for Reinforcement Learning
专知会员服务
59+阅读 · 2019年10月17日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
量化金融强化学习论文集合
专知
13+阅读 · 2019年12月18日
CCF A类 | 顶级会议RTSS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年4月17日
人工智能 | SCI期刊专刊信息3条
Call4Papers
5+阅读 · 2019年1月10日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
RL 真经
CreateAMind
5+阅读 · 2018年12月28日
美国化学会 (ACS) 北京代表处招聘
知社学术圈
11+阅读 · 2018年9月4日
机器人开发库软件大列表
专知
10+阅读 · 2018年3月18日
【推荐】直接未来预测:增强学习监督学习
机器学习研究会
6+阅读 · 2017年11月24日
【计算机类】期刊专刊/国际会议截稿信息6条
Call4Papers
3+阅读 · 2017年10月13日
Arxiv
24+阅读 · 2021年6月25日
VIP会员
相关VIP内容
Linux导论,Introduction to Linux,96页ppt
专知会员服务
78+阅读 · 2020年7月26日
Stabilizing Transformers for Reinforcement Learning
专知会员服务
59+阅读 · 2019年10月17日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
相关资讯
量化金融强化学习论文集合
专知
13+阅读 · 2019年12月18日
CCF A类 | 顶级会议RTSS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年4月17日
人工智能 | SCI期刊专刊信息3条
Call4Papers
5+阅读 · 2019年1月10日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
RL 真经
CreateAMind
5+阅读 · 2018年12月28日
美国化学会 (ACS) 北京代表处招聘
知社学术圈
11+阅读 · 2018年9月4日
机器人开发库软件大列表
专知
10+阅读 · 2018年3月18日
【推荐】直接未来预测:增强学习监督学习
机器学习研究会
6+阅读 · 2017年11月24日
【计算机类】期刊专刊/国际会议截稿信息6条
Call4Papers
3+阅读 · 2017年10月13日
Top
微信扫码咨询专知VIP会员