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

人与工业机器人安全交互的形式规范和验证

• 批准号: 2496876
• 金额: --
• 依托单位: University of Sheffield
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2021
• 资助国家: 英国
• 起止时间: 2021 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2496876
• 关键词: Formal; Specification; Verification; Safe; Interaction

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.

该项目的目的是：1。了解如何以现实且有用的方式制定人类安全特性。将在AMRC开发的具体案例研究，包括用于合作机器人的数字双胞胎的研究原型。研究的主要组成部分将是（1）通过与AMRC专家的互动，各种情况下的安全问题，以及（2）将这些关注点纳入适当形式主义表达的完全正式要求，以识别这些系统。除了受到AMRC特定系统启发的要求外，还可以考虑来自国际标准的通用要求来源，例如“机器人和机器人设备：工业机器人的安全要求”（ISO 10218）和“机器人和机器人设备：协作机器人：协作机器人”（ISO-TS 15066）。这些标准的安全指令的形式化对于AMRC案例研究将很有用，同时也代表了对标准正式清晰度的潜在独立贡献。尤其是对于配乐机器人（协作机器人），这些标准仍在开发中很大程度上，并且早期的正式观点不仅可以帮助澄清，而且可以完善和丰富它们。 2。设计此类安全性在运行系统上的正式验证框架。在这里，通过与AMRC案例研究开发人员合作，可以根据所采用的软件和可用工具探索几种选项：从代码的仪器到动态监控所需的属性，到从代码中的合成和静态验证属性的综合和静态验证。除了软件级验证之外，还将挑战是考虑有助于安全功能的不同设备的行为，其中包括电子挡板，轻门和地板扫描仪。为了正确处理此类混合系统，也可以探索混合方法，其中验证了某些组件，而其他组件只经过测试。