Systematic development of process-control systems for ultra-high dependability assurance based on independently developable end-user assessable logical aspects.

摘要

Process-control systems are usually very complicated and safety-critical. For the development of these systems, it is necessary to be able not only to achieve high quality but also to rigorously demonstrate that high quality has in fact been achieved, i.e., to make them highly dependable. However, since process-control systems are usually very complex and have very huge state spaces, it is too difficult and costly to exhaustively test the state space of these systems to achieve high assurance. Considering this problem, we propose a novel model in which a system is composed from several aspects through pre-defined composition patterns. Each aspect can be not only designed and implemented independently of the other aspects in the system, but can also be tested or verified at the end-user level independently of all the other aspects. We refer to these aspects as Independently Developable End-user Assessable Logical (IDEAL) aspects. The composition pattern consists of three categories, namely, composers, coordinators, and fairness handlers. These composition patterns are pre-defined and can be hardware supported. The system properties (reliability, safety, and stability) can be mathematically inferred from the properties of the individual IDEAL aspects so that conventional integration testing and verification of the entire system is not needed. Based on this model, we present a systematic development technique, i.e., the IDEAL aspects of a process-control system and their composition patterns can be automatically synthesized through the specification of the system guided by several principles developed by us. These principles are evolved to automated tool support. This systematic development method is applied to several examples and a case study involving the control of a future version of the Bay Area Rapid Transit (BART) system.