一种软件功能性安全验证理论和方法

Software has become an infrastructure in national defense construction, economy and people's livelihood. How to improve software safety has been an essential problem in the area of computer science. This project aims at studying the theory and methodology to verify software functional safety based on Modeling, Simulation, and Verification Language (MSVL). First, the safety extension rules of UML are defined to get UMLs models, so as to construct semi-formal models of software functional safety. Then, the semi-formal model is formally characterized by MSVL. Furthermore, the safety properties to be verified are specified by Propositional Projection Temporal Logic (PPTL), the property description language of MSVL. Through the unified model checking method based on MSVL, it is checked whether there are safety flaws in the software model. Finally, a supporting tool is developed based on the theoretical framework.

软件已成为国防建设和国计民生的基础设施，如何提高软件的安全性是目前计算机软件领域面临的一个重要问题。本项目拟研究基于MSVL的软件功能性安全验证理论和方法。首先，定义UML的安全扩展规则得到UMLs模型，以建立软件功能性安全的半形式化模型。其次，采用建模、仿真和验证语言MSVL给出软件功能性安全半形式化模型的形式化描述。然后，使用MSVL的性质描述语言命题投影时序逻辑PPTL公式描述待验证的安全性质，通过基于MSVL的统一模型检测方法验证设计模型是否存在安全缺陷。最后，在理论研究的基础上，设计、开发UMLs建模工具和UMLs到MSVL的模型转换工具。

软件已成为国防建设和国计民生的基础设施，提高软件的安全性是目前计算机软件领域面临的一个重要问题。本项目研究了基于MSVL的软件功能性安全验证理论和方法。首先，定义UML的安全扩展规则得到UML扩展模型，以建立软件功能性安全的半形式化模型。其次，采用建模、仿真和验证语言MSVL给出软件功能性安全半形式化模型的形式化描述。然后，使用MSVL的性质描述语言命题投影时序逻辑PPTL公式描述待验证的安全性质，通过基于MSVL的统一模型检测方法验证设计模型是否存在安全缺陷。并以航空电子系统的设计、实现为特定应用领域，研究了系统功能和体系结构的建模、验证方法，模型之间的转换规则。最后，在理论研究的基础上，设计、开发了相关建模工具和模型转换工具。