软件安全分析的有穷自动机模型  

Finite automata models of software safety analysis

作　　者：陈峰[1,2] 李伟华[1] 

机构地区：[1]西北工业大学计算机学院,陕西西安710072 [2]西北大学信息科学与技术学院,陕西西安710069

出　　处：《西北大学学报（自然科学版）》2011年第1期22-26,共5页Journal of Northwest University（Natural Science Edition）

基　　金：国家自然科学基金资助项目(60803150,60803151);国家自然科学基金委员会-广东联合基金重点资助项目(U0835004);国家“863”计划基金资助项目(2008AA01Z411);陕西省自然科学基金资助项目(2009jm8012);陕西省教育厅自然科学专项基金资助项目(09JK736);陕西省科技攻关基金资助项目(2009k08-04)

摘　　要：目的为在软件设计与开发早期阶段对软件安全模型进行有效分析和验证。方法软件安全分析验证法与形式化建模方法。结果提出了一种安全扩展确定有限自动机(safety extended deterministic finite automata,SEDFA)。在使用UMLsec建立软件安全相关的非形式化模型基础上,通过SEDFA准确的描述能够表达安全交互的序列图。首先创建序列图中单个对象的自动机,其次构造对象积自动机,从而得到表示系统整体交互的SEDFA。结论为系统安全属性的验证提供了基础,可作为下一步生成软件安全测试用例。Aim To analyze and verify the software safety models effectively in the early stage of software design and development.Methods The methods for software safety analysis,derification and fomal modeling prooide that.Results A safety extended deterministic finite automata,SEDFA,is introduced.On the base of establishing security-related non-formal model by UMLsec,the sequence diagram,which expresses the security interaction,can be depicted by SEDFA.Firstly,the automata of signal object are created.Secondly,the product automaton of objects is constructed,and the SEDFA which indicates the complete interaction of the system is obtained.Conclusion It provides the foundation for the system safety property verification and achieving software safety test sases is the fatare work.

关 键 词：软件安全分析 UML安全扩展 确定有限自动机 形式化建模 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]