基于动态符号执行的MSVL程序模型检测

Software has become the core of infrastructure of the national economy and national defense construction. It is a grand challenge for people to improve the reliability, safety and security of software systems. This proposal aims at investigating the method of model checking MSVL programs based on dynamic symbolic execution so that C/Verilog programs can be verified since they can be transformed to MSVL programs. To this end, the theory and method of dynamic symbolic execution of MSVL programs will be investigated. Then, a symbolic execution tree can be used as a system model and a PPTL formula can be used to describe the desired property. Futher, the theories and methods of the offline model checking and on-the-fly model checking will be investigated respectively. Moreover, based on the theories above, the offline model checker and the on-the-fly model checker will be developed. Finally, a case study regarding verification of spacecraft control software will be given to illustrate the feasibility of the proposed theories and methods.

软件已成为国防建设和国计民生基础设施的核心，如何构造安全可靠的软件系统是目前计算机软件领域面临的重大挑战。本项目拟通过动态符号执行对MSVL程序进行模型检测，从而实现对C/Verilog等程序的验证。首先，研究MSVL程序的动态符号执行理论和方法。然后，以得到的符号执行树作为模型，以PPTL公式描述待验证的性质，研究MSVL程序的offline和on-the-fly模型检测理论与方法。进而，在上述研究的基础上，开发MSVL程序的offline和on-the-fly模型检测器。最后，以航天器控制系统软件的验证为应用示范，以检验该理论和方法的可行性。

软件已成为国防建设和国计民生基础设施的核心，如何构造安全可靠的软件系统是目前计算机软件领域面临的重大挑战。本项目建立了MSVL程序的动态符号执行理论和方法；建立了MSVL程序的offline和on-the-fly模型检测理论与方法，并开发了MSVL程序的offline和on-the-fly模型检测器；提出了基于动态符号执行的程序完全正则时序性质的验证方法；建立了MSVL中的函数调用机制；研究了Timed MSVL的语法和语义，并开发相应支持工具并将其用于实时系统验证；研究了PPTL的不动点问题，证明了PPTL的表达能力强于LTL。..投影时序逻辑（Projection Temporal Logic, PTL）是一种区间时序逻辑，包含 next，projection，projection-star等时序操作符，具备比其他时序逻辑较强的表达能力，同时支持有穷模型和无穷模型。建模仿真和验证语言（Modeling, Simulation and Verification Language, MSVL）是PTL的一个可执行子集，该语言支持整型、布尔型、数组、列表等常规数据结构及指针类型；支持赋值、顺序、循环、选择、并行等语法结构，支持await同步操作和异步操作控制语句，实现了结构化和部分面向对象程序设计。目前，已经为MSVL开发了一个验证平台MSV，该平台集成了MSVL的解释器、编译器和不同种类的MSVL模型检测器等形式化验证工具。在验证模式下，通过MSVL程序来为系统建模，使用PPTL描述系统期望的性质，然后验证模型是否满足性质，在不满足的情况下给出反例。另外，已经开发了C/Verilog程序到MSVL程序的转化工具。因此，对C/Verilog程序的验证也可转化为对MSVL程序的验证。在基于动态符号执行的方法中，将MSVL程序进行动态符号执行生成的符号执行树作为它的抽象模型，用PPTL公式描述待验证MSVL程序的性质，建立了基于动态符号执行的MSVL抽象模型检测理论和方法是具有创新性的研究，可用于硬件芯片、航天飞行器控制软件等安全攸关系统的验证，以提高系统的正确性、可靠性和安全性，因此该项研究具有重要的理论意义和应用价值。