Formal Specification and Verification of the Safe Interaction between Humans and Industrial Robots

该项目的目标是：1。了解如何以现实和有用的方式制定人类安全属性。将提供在AMRC开发的具体案例研究，包括用于协作机器人的数字双胞胎研究原型。研究的主要组成部分将是(1)通过与AMRC专家的互动，确定这些系统在各种情况下的安全问题，以及(2)将这些问题提炼成以合适的形式表达的完全正式的需求。除了AMRC的特定系统所激发的需求外，人们还可以考虑来自国际标准的通用需求来源，例如“机器人和机器人设备：工业机器人的安全要求”（ISO 10218）和“机器人和机器人设备：协作机器人”（ISO- ts 15066）。这些标准的安全指令的形式化将对AMRC案例研究有用，同时也代表了对标准形式化清晰度的潜在独立贡献。特别是对于协作机器人，这些标准仍处于开发阶段，早期的正式观点不仅可以帮助澄清，还可以完善和丰富它们。2. 为运行系统的安全特性设计一个正式的验证框架。在这里，在与AMRC案例研究开发人员的合作中，可以根据所使用的软件和可用的工具探索几种选择：从代码的仪表化到动态监视所需的属性，到代码的属性规范的合成和静态验证，再到通过证明助手验证的规范生成代码。除了软件层面的验证之外，一个挑战将是考虑不同设备的行为，这些设备有助于安全功能，包括电子停车、光门和地板扫描仪。为了正确处理这种混合系统，人们还可以探索混合方法，其中某些组件经过验证，而其他组件仅经过测试。

The project aims are:1. To understand how to formulate human-safety properties in a realistic and useful manner. Concrete case studies developed at AMRC will be available, including research prototypes of digital twins for collaborating robots. Main components of the research will be (1) to identify for these systems, via interaction with AMRC experts, safety concerns in various scenarios, and (2) to distil these concerns into fully formal requirements expressed in a suitable formalism. Besides the requirements inspired by specific systems at AMRC, one could also consider the general-purpose source of requirements coming from international standards such as "Robots and robotic devices: Safety requirements for industrial robots" (ISO 10218) and "Robots and robotic devices: Collaborative robots" (ISO-TS 15066). The formalization of these standards' safety directives will be useful for the AMRC case studies, while also representing a potential standalone contribution to the formal clarity of the standards. Especially for cobots (collaborative robots), these standards are still very much under development, and an early formal perspective could help not only clarify, but also refine and enrich them. 2. To design of a formal verification framework for such safety properties on running systems. Here, in collaboration with the AMRC case study developers, one could explore several options based on the employed software and the available tools: ranging from the instrumentation of the code to dynamically monitor the desired property, to the synthesis and static verification of property specifications from code, to code generation from specifications verified with a proof assistant. Beyond software-level verification, a challenge will be to factor in the behaviour of different devices that contribute to the safety functionality - which include e-stops, light gates and floor scanners. To properly deal with such hybrid systems, one could also explore mixed approaches, in which certain components are verified and others are only tested.