摘要
面向对象的形式化规格说明语言Object Z在软件开发中的规格需求方面已广泛应用,但在安全关键系统开发中的应用还是空白。容忍入侵是一种全新的系统安全防护手段,是实现系统可生存性的一种方法,可用于安全关键性基础设施以及系统的基本服务的保护。显然,在容忍入侵系统的开发过程中应用形式化的规格说明方法,保证所开发的系统能够满足系统的安全需求,可增强用户对所实现系统的信任。以Object Z方法对我们所设计的一个容忍入侵的会议密钥系统进行规格说明为例,将Object Z的应用扩展到安全关键系统的开发和设计领域。
The academic literature concerning the object-oriented specification language Object Z relates almost entirely to the specification and design of large software system. However, nothing is done in these literatures to apply Object Z to the security-critical systems to structure them to fulfill their security requirement and so to win the confidence of users of the secured systems. Taking an intrusion-tolerant system as an example, we illustrate how Object Z can be used to specify and model the security-critical systems. The specification is useful and helpful not only for improving the quality of intrusion-tolerant system, but also for implementing more strict system testing.
出处
《系统仿真学报》
EI
CAS
CSCD
2004年第12期2837-2841,2846,共6页
Journal of System Simulation
基金
国家自然科学基金重大计划 (90204012)
国家863计划(2002AA143021)
教育部优秀青年骨干教师资助计划
教育部科学技术重点研究项目。
