【摘要】 软件的大量应用,使控制系统面临严峻的安全考验,陷入了安全危机中,迫切需要新的安全保障技术。安全核就是应运而生的一种安全保障新概念,其可信性直接关系到安全核的有效性和系统的安危。面对安全核可信性问题,测试和限制安全核尺寸是当前采用的方法,它们极大地制约了安全核技术在复杂系统中的应用。本文分析了安全核可信性的本质;结合安全关键系统的基本构架,提出了从安全需求分析开始到安全核生成过程中,如何通过形式化的方法来提高安全核可信性的方法,为安全核技术在复杂系统中的应用提供了一种新思路;以交通灯控制为例全过程地实现和验证了所提出思想的正确性和可行性。更多还原

【Abstract】 Since software is being used in the control system largely,the possibility of serious damage resulting from a software defect is considerable and growing,and then the control systems are plunging into safety crisis.In fact,control systems are in urgent need of new safety assurance technologies.Safety kernel is a new concept of safety assurance.It e- merges,as the time requires.Of course,its dependability plays an important role on system.The present methods to im- prove the dependability of safety kernel are to limit its size and test.These methods prevent largely safety kernel from being used in complex systems.This paper at first analyzes comprehensively correctness requirements of safety kernel and the basis frame of safety-critical system.Then,based on all of these,a method that how to construct and improve the dependability of safety kernel is put forward from the safety requirements.Also This paper is a demonstration that safety kernel is a feasible and desirable technique for software in complex safety-critical systems.At last,taking the con trol system for the traffic lights as example,the whole process and its correctness have been achieved and proved.更多还原