Certifying Autonomous Systems

D-RisQ有限公司和蓝熊系统研究有限公司(BBSR)正在合作一个名为“认证自主”的项目。该项目将开发由BBSR提供的基于海事的系统，该系统将接受设计角度的验证，使用D-RisQ开发的技术来满足自主系统认证的需要。验证技术建立在自动形式化方法的基础上，这些方法允许对设计进行全面的探索，并根据文本要求进行检查。自动化是为了降低成本，并使设计工程师能够经常接触到使用正式方法施加的严格要求。在适当的形式语义的支持下，使用常用的设计工具，我们可以定义自治系统的行为边界，并证明它在任何正常情况下都符合要求。在可能的情况下，我们还将展示在故障条件下发生的情况，例如，其他自动系统或意外的环境输入。我们将探讨认证要求以及设计的软件实现，并试图展示如何满足海事领域中自主的、基于软件的系统的认证要求，并确保证据可以应用于其他更具挑战性的领域，如民用航空航天。

D-RisQ Ltd and Blue Bear Systems Research Ltd (BBSR) are collaborating on a project called ‘Certifying Autonomy’. The project will develop a maritime based system provided by BBSR that will be subject to validation from a design perspective using technologies developed by D-RisQ to meet the needs of autonomous systems certification. The validation technology is founded on automated formal methods which allow fully exhaustive exploration of design and checking it against textual requirements. The automation is required to reduce cost and enable design engineers regular access to the rigour imposed by the use of formal methods. Using commonly available design tools underpinned by appropriate formal semantics, we can define the boundary of the behaviour of an autonomous system and prove that it conforms to requirements under every normal circumstance. Where possible, we will also involve showing what happens under failure conditions of, for example, other automatic systems or unanticipated environmental inputs. We will explore the certification requirements and also the software implementation of the design and attempt to show how to meet certification requirements for autonomous, software based systems in not only the maritime domain, but ensure that the evidence can be applied to other more challenging domains such as civil aerospace