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

项目名称： C/Verilog程序的MSVL验证理论与方法

项目编号： No.91418201

项目类型： 重大研究计划

立项/批准年度： 2015

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

项目作者： 段振华

作者单位： 西安电子科技大学

项目金额： 160万元

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

中文关键词： 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.

英文关键词： MSVL；Model Checking；Program Verification；Semantics；Abstraction-Refinement