权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

RIVERAS: Robust Integrated Verification of Autonomous Systems

RIVERAS：自主系统的鲁棒集成验证

基本信息

批准号：
EP/J01205X/1
负责人：
Kerstin Eder
金额：
$ 104.1万
依托单位：
University of Bristol
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2013
资助国家：
英国
起止时间：
2013 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FJ01205X%2F1
关键词：
RIVERAS Robust Integrated Verification Autonomous

项目摘要

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.

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