复杂需求场景驱动的软件安全防护模型检测技术研究

项目名称： 复杂需求场景驱动的软件安全防护模型检测技术研究

项目编号： No.61462034

项目类型： 地区科学基金项目

立项/批准年度： 2015

项目学科： 自动化技术、计算机技术

项目作者： 王曦

作者单位： 江西理工大学

项目金额： 46万元

中文摘要： 在航空航天、交通运输等高可信系统领域，系统的实际运营场景非常复杂，其安全性至关重要，如何对系统进行安全防护并确保其运营安全日益成为关注焦点。传统的安全性分析方法与安全保障技术都不能从根本上确保系统安全，模型检测是验证和分析系统行为属性的有效途径，但目前的模型检测技术存在形式化建模难、安全性分析不充分、状态空间爆炸、通用性与实用性不强等问题。本课题根据安全苛求系统的安全性特点与复杂需求场景，研究统一语义框架下的系统形式化模型自动生成方法，提出适合于系统安全性分析的通用模型检测算法，并针对不同的故障模式，提出相应的故障注入算法与系统安全性分析方法，自动获得形式化安全需求与软件安全性设计的形式化模型，并研制相应的支撑工具软件。本课题的研究为安全苛求系统的安全防护、安全性分析与评估、系统可信性的提高、安全需求与软件设计模型的获取提供理论指导与技术支撑，丰富了基于模型的高可信软件形式化开发方法。

中文关键词： 模型检测；软件安全性；形式化验证；安全性分析与评估

英文摘要： Safety is the most important property for high dependable systems,such as in aerospace, transportation and nuclear energy areas, whose actual operational scenarios is very complex, in order to ensure the whole system's safety, some methods and technologies should be adopted for system's safety analysis and design. Conventional methods for safety analysis and assurance technology have problems in terms of correctness and efficiency. It is prone to make errors because the result of safety analysis and software design are come from natural language, and the manual work is very labor intensive and time consuming. Model checking is an effective way to verify and analyze whether behaviors of the system meet its properties. Using Model checking methods and fault injection techniques can improve consistency and correctness for safety process throughout the system's safety lifecycle. Yet existed methods for fault injection and model checking mainly think about single faults injection and qualitative safety analysis, seldom do with fault injection for multiple faults and quantitative safety analysis, so the procedure for safety analysis and the result for safety verification is inadequate. It is difficult to build formal model according to system requirement specification, and the problems for state space explosion in model checking is prone to happen. In our subject, we research model checking methods on safety analysis and automatic formal design model generation for safety critical system,whose safety features and actual operational scenarios system are considered, by definition of a unified semantic framework and consistent analysis for system requirement scenarios, a method for automatic generating formal system model from requirement scenarios is provided, in order to analyze the safety property for safety critical system, we propose suitable model checking algorithm, and provide corresponding fault injection-based model checking methods according to different type of fault failure mode, then automatically form the minimal cut sets of fault trees and get formal safety requirements, finally, according to safety requirements, modification and refinement is adopted for system requirement scenarios step by step, the formal design model is formed and consistent with the safety requirements, it can be used for safety design model of safety criticial system. some relevant supporting software tools for proposed model checking and fault injection algorithms are developmented, and dynamic simulation for formal safety design model is provided. Through the studies in the project, some theoretical and methodological guidance is offered for the technologies on safety assurance, such as safety analysis and assessment of safety critical system, the improvement for system dependability, automatic safety requirements acquisition and formal safety design model generation, which can enrich the method for model-based system formal development.

英文关键词： model checking;software safety;formal verification;safety analysis and assessment