防危核一致性保障技术的研究

Research on assurance technology of safety kernel consistency

通过理想防危策略及其制定算法把防危策略的制定与一致性险证集为一体,从而解决防危策略与系统防危需求之间一致性问题;然后研究了以Z语言为桥梁,用数学证明来解决防危核与防危策略之间一致性证明的方法。以十字路口的交通控制为例,全过程地实现和验证了所提出的思想和算法的正确性。

Safety-critical real time systems （SCRTS） often operate in harsh environmental conditions that necessitate fault tolerant computing and safety assurance techniques. By defining the concept of ideal safety policy and setting up its structuring algorithm, a solution based on formal description is put forward. We use it to assure the consistence between safety policies and system safety requirements. Furthermore, using Z language, a feasibility method to prove the consistency between the safety kernel and safety policies is constructed. At last, taking the control system in the traffic lights as an example, the whole process and its correctness is proved.