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.