The Process of Model Checking Software Security in UML Models with SPIN

摘要：

This paper describes a method of detecting design security vulnerability with the model checker SPIN. Known security properties are expressed in LTL formulae. Software design is converted into PROMELA. A case study shows feasibility and principles of the method. This paper focuses only on temporal security properties. Future work includes to create more LTL security patterns and to experiment them with more models of software design. Another issue is the automatic generation of PROMELA from software design concerning security requirements.

关键词： model checking software security UML SPIN

作者: LIU xin CAI Wan-Dong

作者单位: College of Computer Science Northwestern Polytechnical University

会议类型: 国际会议

会议名称: 2010 Third Pacific-Asia Conference on Web Mining and Web-based Application(2010年第三届web挖掘和基于web应用亚太会议 WMWA 2010)

会议地点: 桂林

会议语种:英文

页码: 195-198

在线出版日期: 2010-11-17（万方平台首次上网日期，不代表论文的发表时间）