Rigorous development of a safety-critical system based on coordinated atomic actions
Rigorous development of a safety-critical system based on coordinated atomic actions
复制标题
基于协调原子行动的安全关键系统的严格开发
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
F. V. Henke
中科院分区：
文献类型：
--
作者：
Jie Xu;B. Randell;A. Romanovsky;R. Stroud;A. Zorzo;E. Canver;F. V. Henke
本文介绍了我们的经验，使用协调原子（CA）的行动作为一个系统的结构化工具，设计和验证一个复杂的控制系统的复杂的工业应用，具有高可靠性和安全性的要求。我们的研究是基于“容错生产单元”，这代表了一个制造过程，涉及冗余的机械设备（提供，以便能够在机器故障的存在下继续生产）。模型规范所带来的挑战是设计一种控制系统，即使在存在大量和各种设备和传感器故障的情况下，也能保持指定的安全性和活性特性。我们在本文中讨论：i）一个控制程序的设计，使用CA行动，以处理安全相关的和容错的关注，和ii）正式验证这种设计的基础上使用的模型检查。我们发现，CA动作结构通过独立处理各种安全问题（例如移动机械的冲突）来促进设计和验证任务。正式验证活动与设计活动同时进行，它们之间的相互作用导致了“确认设计”的综合练习。
This paper describes our experience using coordinated atomic (CA) actions as a system structuring tool to design and validate a sophisticated control system for a complex industrial application that has high reliability and safety requirements. Our study is based on the "Fault-Tolerant Production Cell", which represents a manufacturing process involving redundant mechanical devices (provided in order to enable continued production in the presence of machine faults). The challenge posed by the model specification is to design a control system that maintains specified safety and liveness properties even in the presence of a large number and variety of device and sensor failures. We discuss in this paper: i) a design for a control program that uses CA actions to deal with both safety-related and fault tolerance concerns, and ii) the formal verification of this design based on the use of model-checking. We found that CA action structuring facilitated both the design and verification tasks by enabling the various safety problems (e.g. clashes of moving machinery) to be treated independently. The formal verification activity was performed in parallel with the design activity the interaction between them resulted in a combined exercise in "design for validation".