安全攸关软件系统的可靠性保障研究

Safety critical systems require high reliability and correctness, since failure of these systems will result in significant loss of life and property, or serious damages to the environment. Softwares running on safety critical systems are called safety critical software systems. As a matter of fact, most of the main functions of safety critical systems are realized in softwares. Therefore, reliability of safety critical systems depends mainly on the reliability of the softwares in them. In this project, we propose to investigate formal methods based theories and methodologies for ensuring reliability of safety critical software systems. First, with respect to different features, e.g. real-time, concurrency, and openness, of safety critical software systems, modeling theories and technologies will be investigated in this project. Second, on different kinds of system models, how safety critical properties can be efficiently verified will be studied in detail and supporting tools will also be implemented. Third, in order to ensure the reliability of safety critical software systems in large scale, theories and methodologies for reducing state space to be explored throughout the verification will also be investigated. Finally, this project intents to evaluate the effectiveness of the proposed theories and methodologies by the real-world space control software systems.

安全攸关系统对可靠性和正确性要求极高，系统失效会导致生命和财产的重大损失或对环境的严重破坏。运行在安全攸关系统上的软件称为安全攸关软件系统。软件已成为安全攸关系统使能部件，因此，保障软件的可靠性是保障安全攸关系统可靠性的关键。项目研究基于形式化验证的安全攸关软件系统的可靠性保障理论和方法。拟首先针对安全攸关软件系统的实时性、并发性和开放性等特征，研究系统的形式化建模理论与方法。进而针对不同的模型，研究系统安全攸关属性的高效验证理论和方法。为了支持大规模安全攸关软件系统的验证，拟研究针对导致状态空间爆炸的关键问题的状态空间缩减理论和方法。最后，项目拟以航天控制软件系统为应用示范，展示所提出的验证方法的有效性。

安全攸关系统失效会导致生命和财产的重大损失或对环境的严重破坏，而软件已成为安全攸关系统使能部件，因此，保障软件的可靠性是保障安全攸关系统可靠性的关键。项目研究了基于形式化验证的安全攸关软件系统的可靠性保障理论和方法，取得了一些国际领先的研究成果，包括：提出了一种实现建模、仿真和验证语言MSVL编译器的方法，可以编译MSVL程序，同时集成了MSVL程序的建模和验证的功能。基于MSVL，提出了新的运行时验证程序时序性质的方法，以及验证程序是否满足上下文无关文法的方法。为了检测安全套接字层/传输层安全进协议（SSL/TLS）实现中的漏洞，提出了一种新的证书标准制导的对SSL/TLS实现进行差异测试的方法。为了验证大数据的可靠性，提出了基于统一模型检测的代码级运行时验证方法。针对Craig插值的不足，提出了错误插值和安全插值，缩减了模型检测中的状态空间，提高了检测的规模。针对大规模并行程序验证中的状态空间爆炸问题，提出了将条件插值与CEGAR相结合的方法，缩减了并行验证任务的状态空间。为了缓解并发程序验证中由线程调度的不确定性所导致的路径空间爆炸问题，提出了一种“优先探索+约束辅助”的偏序约简方法。针对系统模型的不确定性问题，提出了关于非确定Streett自动机最优的确定化数据结构，降低了其确定化的状态复杂度。完善了安全攸关软件资源共享和协同验证平台MSV，开发了基于插值、循环摘要的模型检测工具，以及针对并发程序的模型检测工具。项目以航天控制软件系统为应用示范，展示了所提出的验证方法的有效性。在TOSEM, TKDE, TR, TCS等著名国际期刊，以及LICS, ICSE, ASE, FSE等著名国际会议发表论文60篇；获西安市软件可信认证关键技术重点实验室(2021)；陕西省安全攸关智能软件创新团队(2018)；培养“长江学者”特聘教授1名，博士11名、硕士72名；授权专利13项（含美国专利2项）；组织国内会议2次、合作组织国际会议5次、邀请国内外知名学者讲学16人次、参加国际会议20次。