论文标题
从需求到自动飞行：监视项目的概述
From Requirements to Autonomous Flight: An Overview of the Monitoring ICAROUS Project
论文作者
论文摘要
无人系统（ICAROUS）可靠操作的独立配置体系结构是一种软件体系结构，结合了一组算法，可实现无人飞机应用程序的自主操作。本文概述了监视Icarous的概述，该项目的目标是从用结构化的自然语言编写的要求提供正式的方法来为自动系统生成运行时监视器。这种方法集成了FRET，这是一种正式的需求启发和创作工具，以及运行时验证框架的Copilot。 FRET用于指定结构化自然语言的正式要求。这些要求转化为时间逻辑公式。然后使用Copilot从这些时间逻辑规范中生成可执行的运行时监视器。生成的监视器直接集成到ICAROUS中，以在飞行过程中执行运行时验证。
The Independent Configurable Architecture for Reliable Operations of Unmanned Systems (ICAROUS) is a software architecture incorporating a set of algorithms to enable autonomous operations of unmanned aircraft applications. This paper provides an overview of Monitoring ICAROUS, a project whose objective is to provide a formal approach to generating runtime monitors for autonomous systems from requirements written in a structured natural language. This approach integrates FRET, a formal requirement elicitation and authoring tool, and Copilot, a runtime verification framework. FRET is used to specify formal requirements in structured natural language. These requirements are translated into temporal logic formulae. Copilot is then used to generate executable runtime monitors from these temporal logic specifications. The generated monitors are directly integrated into ICAROUS to perform runtime verification during flight.
