基于形式化方法的统一软件模型及其应用

摘要

随着计算机应用的不断发展，在信息社会中发挥着至关重要的作用。但是软件的生产现状不能令人满意，软件安全事故、软件质量问题、软件扩展问题已经带来了巨大的损失。国内外专家及行业巨头已经将软件的可信性作为软件的一个重要属性，然而，目前多数研究主要还是针对安全性。
　　 本文将软件可信性做一个多维的评估指标，通过软件工程方法论的角度，针对软件的功能性、可靠性、安全性、可维护性、可扩展性等性质进行了研究，主要工作包括：
　　 1)提出了基于形式化语言Z规格和UML视图的统一软件模型，基于该模型，构建了软件可信工程方法，该方法将形式化方法融入传统软件工程，继承了形式化模型可验证的优点，并一定程度降低了形式化模型在大型项目中较高的复杂度、和传统软件工程大量的人为不确定因素。
　　 2)基于课题组软件安全缺陷知识库，实现了统一软件模型在设计阶段的软件安全缺陷形式化检测，从而在缺陷引入的最早阶段快速发现并给出具体缓和方案，避免了设计阶段的软件安全缺陷在软件生命周期后期非常高昂的缓和成本、降低了软件安全性保障对安全专家个人经验和知识的依赖。
　　 3)设计了软件可信工程支持平台，从工具角度提高了软件可信工程的可实施性，并引入了结合统一软件模型的项目管理机制降低了工程管理所引入的开发不确定性。
　　 本文搭建了一个结合了形式化方法的软件工程理论体系，实现了软件设计的一致性、有效性、安全性验证，集成了课题组其他工作如模型驱动的单元测试、可信性评估等，同时，为将来的研究工作提供了理论基础。