As a general trend in industrial robotics, an increasing number of safety functions are being developed or re-engineered to be handled in software rather than by physical hardware such as safety relays or interlock circuits. This trend reinforces the importance of supplementing traditional, input-based testing and quality procedures which are widely used in industry today, with formal verification and model-checking methods. To this end, this paper focuses on a representative safety-critical system in an ABB industrial paint robot, namely the High-Voltage electrostatic Control system (HVC). The practical convergence of the high-voltage produced by the HVC, essential for safe operation, is formally verified using a novel and general co-verification framework where hardware and software models are related via platform mappings. This approach enables the pragmatic combination of highly diverse and specialised tools. The paper's main contribution includes details on how hardware abstraction and verification results can be transferred between tools in order to verify system-level safety properties. It is noteworthy that the HVC application considered in this paper has a rather generic form of a feedback controller. Hence, the co-verification framework and experiences reported here are also highly relevant for any cyber-physical system tracking a setpoint reference.
翻译:作为工业机器人的一般趋势,正在开发或重新设计越来越多的安全功能,以便用软件而不是安全继电器或隔锁电路等实物硬件来处理。这一趋势更加突出了以正式的核查和模式检查方法补充当今工业广泛使用的传统、基于投入的测试和质量程序的重要性。为此,本文件侧重于ABB工业油漆机器人中具有代表性的安全临界系统,即高压电子控制系统(高压电子控制系统)。对于安全操作至关重要的HVC产生的高压集成,使用新颖和一般的共同核查框架进行正式核查,其中硬件和软件模型通过平台绘图相互关联。这种方法使得高度多样化和专业化的工具能够务实地结合起来。本文件的主要贡献包括如何在各种工具之间转让硬件抽象和核查结果,以核实系统安全特性。值得注意的是,本文件所考虑的HVC应用程序有一个相当通用的反馈控制器形式。因此,共同核查框架和此处所报告的经验对于任何网络跟踪也具有高度相关性。