RIVERAS: Robust Integrated Verification of Autonomous Systems

任何用于安全关键任务的系统，如污染监测无人机、检查核电站的机器人或医院或家中的人类辅助护理机器人，在我们使用它之前，必须有足够的证据证明其安全性。收集这些证据涉及验证，即证明系统的实施符合其规格要求的过程。人们在开发微电子设计和软件验证的工具和方法方面做了大量工作，当我们试图用现有的方法验证一个自治的智能系统（AIS）时，出现了两个问题：第一，传统的验证技术依赖于一个完全定义待验证系统功能行为的规范。但是，我们希望使用一个智能系统--一个能够适应环境的系统，在没有被告知具体如何做的情况下决定做什么--这样我们就可以避免为每一种可能的情况指定一个反应。通常有太多可能的情况，这是实际的。相反，我们需要灵活的规格表示的可接受的和所需的行为与相关的精确限制的关键属性补充更模糊的指示所需的actions.Second，控制软件来实现动态自适应是非常复杂的，使用迭代优化算法结合联合收割机离散和连续的决策。虽然已经有很多关于如何设计这些算法的研究，但是它们的验证仍然是一个开放的研究问题。首先，我们将开发一种验证具有灵活规范的系统的方法。这将需要一种正式的方式来编写规范，使用可以捕获这些灵活需求的建模语言。然后，模糊概念将被用来分析我们如何满足规范。模糊概念是分级的，涉及它们的属性或陈述在某种程度上是真的（或假的）。这意味着规格可能只能部分满足，这在验证它们时引入了新的挑战。其次，我们还将开发验证使用优化的控制软件的方法，这是一种通用的决策方法。给定一个成本模型和一组定义允许限制的约束，优化器会找到一组最佳决策，以最大化或最小化成本，同时保持在允许的限制内。智能系统的大多数规划问题都可以用优化的形式来表达，控制理论的研究证明了帮助我们理解它应该如何工作的特性。我们将使用控制理论建立的属性作为规范来证明优化器软件做了它应该做的事情。此外，我们将这些属性集成到软件中。这使我们能够检测、控制和纠正发生的故障。最后，我们将把所有这些发展整合到一个创新的“验证设计”（DFV）方法中。在指定和设计智能系统以及生产基于优化的控制软件时，使用我们的DFV方法的工程师将立即能够使用我们的验证方法来确定他们是否做对了。这将比先设计它要容易得多，效率也高得多，而不考虑验证，然后再弄清楚如何验证。为了帮助改进我们的方法并在事后进行评估，Riveras将在真实的机器人上进行试验。例如，我们将为火星探测器设计一个智能探测系统，在地球上的机器人上实现它，并提供所有验证证据来证明它按预期工作。

Any system used for a safety-critical task, like a pollution-monitoring unmanned aerial vehicle, a robot inspecting a nuclear plant or a human assistive nursebot in a hospital or at home, must have enough evidence to demonstrate its safety before we can use it. Gathering such evidence involves verification, the process of demonstrating that the implementation of a system meets the requirements laid down in its specification. Much work has been done to develop tools and methods for verification of microelectronic designs and software.When we try to verify an autonomous, intelligent system (AIS), with existing methods, two problems arise: First, traditional verification techniques rely on a specification that fully defines the functional behaviour of the system to be verified. But, we want to use an intelligent system - one that can adapt to circumstances, deciding what to do without being told exactly how - precisely so we can avoid having to specify a response for every possible scenario. There are usually far too many possible scenarios for this to be practical. Instead, we need flexible specifications expressed in terms of acceptable and required behaviour with associated precise limits for critical properties complemented by more vague indications of desired actions.Second, the control software to achieve dynamic adaptation is very complex, using iterative optimization algorithms to combine discrete and continuous decision-making. Although there has been much research on how to design these algorithms, their verification is still an open research question.The RIVERAS project aims to tackle both of these problems. First, we will develop a way of verifying a system with a flexible specification. This will require a formal way to write a specification, using a modelling language that can capture these flexible requirements. Then, fuzzy concepts will be used to analyse how well we meet the specification. Fuzzy concepts are graded and properties or statements involving them are true (or false) to some degree. This means that specifications may only be partialy satisfied which introduces new challenges when verifying them.Second, we will also develop ways of verifying control software that uses optimization, which is a general approach for making decisions. Given a cost model and a set of constraints that define permitted limits, an optimizer finds the best set of decisions to maximize or minimize the cost while staying within permitted limits. Most planning problems for intelligent systems can be expressed in the form of optimization and research on control theory proves properties that help us understand how well it should work. We will use the properties established with control theory as a specification to demonstrate that the optimizer software does what it should. Moreover, we will integrate these properties into the software. This allows us to detect, contain and correct failures should they occur. Finally, we will integrate all these developments into an innovative "Design for Verification" (DFV) method. Engineers who use our DFV methods when specifying and designing an intelligent system, and when producing its optimization-based control software, will immediately be able to use our verification methods to determine if they have done it right. This will be far easier and a lot more efficient than designing it first, without thinking about verification, and then figuring out how to verify afterwards.To help refine our methods and to evaluate them afterwards, RIVERAS will try them out on real robots. For example, we will design an intelligent exploration system for a Mars rover, implement it on a robot on Earth, and produce all the verification evidence to demonstrate it works as intended.