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

结题报告

项目介绍

AI项目解读

基本信息

批准号：
91418201
项目类别：
重大研究计划
资助金额：
160.0万
负责人：
段振华
依托单位：
西安电子科技大学
学科分类：
F0203.软件理论、软件工程与服务
结题年份：
2016
批准年份：
2014
项目状态：
已结题
起止时间：
2015-01-01 至2016-12-31

项目参与者：
张南；赵亮；张琛；黄伯虎；杨凯；王猛；于斌；刘瑾；王德奎；
关键词：
语义 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的统一限界和抽象模型检测器。最后，以航天器控制系统软件的验证为应用示范，展示本项目所建立的理论与方法在国家重大工程中的应用。