C/Verilog程序的MSVL验证理论与方法

Software is an indispensable part in national defense construction, economy and people's livelihood. How to build reliable and secure software systems has been a big challenge in the field of computer software. With this motivation, this project will investigate model checking approach of C/Verilog programs with MSVL. To do so, transformation rules from C/Verilog to MSVL programs will be studied and equivalence of transformation will be proved. On this basis, a supporting toolkit will be developed for automatic C/Verilog programs model checking which includes translators from C and Verilog programs, respectively, to MSVL programs, as well as unifiedly bounded and abstract model checkers of MSVL. Finally, spaceflight control software systems will be verified to show how the proposed approach are utilized in practice.

软件已成为国防建设和国计民生的基础设施，如何构造安全可靠的软件系统是目前计算机软件领域面临的重大挑战。本项目拟通过C/Verilog程序的MSVL模型检测理论与方法，提高使用C/Verilog语言开发的网络和嵌入式软件系统的可靠性和安全性。首先，研究C/Verilog程序到MSVL程序的转换规则和转换的语义等价性。然后，以得到的MSVL程序作为模型，研究MSVL的统一限界和抽象模型检测理论与方法。进而，在上述研究的基础上，开发C/Verilog程序的MSVL自动模型检测平台，包括C/Verilog到MSVL程序转换器，以及MSVL的统一限界和抽象模型检测器。最后，以航天器控制系统软件的验证为应用示范，展示本项目所建立的理论与方法在国家重大工程中的应用。

软件已成为国防建设和国计民生的基础设施，如何构造安全可靠的软件系统是目前计算机软件领域面临的重大挑战。本项目通过C/Verilog程序的MSVL模型检测理论与方法，提高了使用C/Verilog语言开发的网络和嵌入式软件系统的可靠性和安全性。为此，首先研究了C/Verilog程序到MSVL程序的转换规则和转换的语义等价性。然后，以得到的MSVL程序作为模型，研究MSVL的统一限界和抽象模型检测理论与方法。进而，在上述研究的基础上，开发了C/Verilog程序的MSVL自动模型检测平台，包括C/Verilog到MSVL程序转换器，以及MSVL的统一限界和抽象模型检测器。最后，以航天器控制系统软件的验证为应用示范，展示本项目所建立的理论与方法在国家重大工程中的应用。