由设计瑕疵引起的安全问题占据了系统开发过程中出现的安全性问题的50%,因此,无论在多么坚实的软件安全程序中,对于系统体系结构的风险分析都显得十分重要。安全性风险分析是一种将技术问题和数据考量等相联系的自然方法,是在软件系统开发生命周期的初期阶段就需要完成的步骤。安全风险分析的结果和风险类别同时也驱动了软件安全性需求分析和安全性测试。系统安全性需求分析与建模是将风险分析的过程放在了软件生命周期的早期需求层,这是进行软件体系结构风险分析的最佳选择。现有的软件安全分析与建模方法主要包括：创建安全对象及分析评估故障树；在软件生命周期的整个个过程中跟踪关键安全需求；在软件质量模型基础上添加安全标准和度量等。而这些方法和模型与传统的软件设计模型存在一定差异。系统的安全模型往往需要进行严格的形式化分析与验证,因此有必要使用更为严格的过程管理及形式化的设计与分析方法对软件安全性进行验证。使用Unified Modeling Language (UML)统一建模语言来对软件系统进行建模是现在最流行的建模方式,但是对于要求严格的系统安全模型,有必要对UML建立的模型进行形式化来分析其可行性。论文在自动机理论基础上提出了描述UML视图的形式化机制,并将其映射到模型语言Promela,从而实现对使用UML建立的软件安全模型的形式化,使得由非形式化的UML语言建立的软件安全模型能够得到更清晰严格的描述。过程中使用线性时序逻辑语言LTL定义软件安全属性,描述直观并具有良好的兼容性。最后以形式化后的模型和LTL语言描述的系统安全属性作为输入,使用目前流行的模型检测工具Spin来验证安全模型的可行性。论文基于实际的系统设计过程,针对面向客户的风机选型软件的继续开发,使用UMLsec建立了在线选型服务系统的安全模型,使用线性时序逻辑语言定义了系统相关安全属性,经过模型检测工具Spin验证通过。实践证明实现过程能够较好地描述并检测软件模型安全性,使系统安全性在设计阶段得到较好的优化验证