一种容忍入侵结构的Z规格说明  

Object Z Specification of the Intrusion-tolerant System

作　　者：郭渊博[1,2] 史庭俊[1] 马建峰[1,3] 

机构地区：[1]西安电子科技大学教育部计算机网络与信息安全重点实验室 [2]解放军信息工程大学电子技术学院,河南郑州450004 [3]天津工业大学计算机与自动化学院,天津300160

出　　处：《系统仿真学报》2004年第12期2837-2841,2846,共6页Journal of System Simulation

基　　金：国家自然科学基金重大计划 (90204012); 国家863计划(2002AA143021); ;教育部优秀青年骨干教师资助计划;教育部科学技术重点研究项目。

摘　　要：面向对象的形式化规格说明语言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.

关 键 词：形式化规格说明 ONect Z语言 容忍入侵 建模 

分 类 号：TP391.9[自动化与计算机技术—计算机应用技术]