首页 | 本学科首页   官方微博 | 高级检索  
     检索      

一种容忍入侵结构的Z规格说明
引用本文:郭渊博,史庭俊,马建峰.一种容忍入侵结构的Z规格说明[J].系统仿真学报,2004,16(12):2837-2841,2846.
作者姓名:郭渊博  史庭俊  马建峰
作者单位:1. 西安电子科技大学教育部计算机网络与信息安全重点实验室,陕西,西安,710071;解放军信息工程大学电子技术学院,河南,郑州,450004
2. 西安电子科技大学教育部计算机网络与信息安全重点实验室,陕西,西安,710071
3. 西安电子科技大学教育部计算机网络与信息安全重点实验室,陕西,西安,710071;天津工业大学计算机与自动化学院,天津,300160
基金项目:国家自然科学基金重大计划 (90204012),国家863计划(2002AA143021),教育部优秀青年骨干教师资助计划,教育部科学技术重点研究项目。
摘    要:面向对象的形式化规格说明语言Obiectz在软件开发中的规格需求方面已广泛应用,但在安全关键系统开发中的应用还是空白。容忍入侵是一种全新的系统安全防护手段,是实现系统可生存性的一种方法,可用于安全关键性基础设施以及系统的基本服务的保护。显然,在容忍入侵系统的开发过程中应用形式化的规格说明方法,保证所开发的系统能够满足系统的安全需求,可增强用户对所实现系统的信任。以Obiectz方法对我们所设计的一个容忍入侵的会议密钥系统进行规格说明为例,将Obiectz的应用扩展到安全关键系统的开发和设计领域。

关 键 词:形式化规格说明  ONect  Z语言  容忍入侵  建模
文章编号:1004-731X(2004)12-2837-05

Object Z Specification of the Intrusion-tolerant System
GUO Yuan-bo,SHI Ting-jun,MA Jian-feng.Object Z Specification of the Intrusion-tolerant System[J].Journal of System Simulation,2004,16(12):2837-2841,2846.
Authors:GUO Yuan-bo    SHI Ting-jun  MA Jian-feng
Institution:GUO Yuan-bo1,2,SHI Ting-jun1,MA Jian-feng1,3
Abstract: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.
Keywords:formal specification  Object Z  intrusion-tolerant system  modeling
本文献已被 CNKI 维普 万方数据 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号