C-to-MSVL转换系统关键技术研究

发布时间：2022-01-08 19:13

　　C语言是一门通用的高级程序设计语言。C语言以其灵活高效、功能丰富和可移植性强等优点,广泛应用于系统软件与应用软件的开发中。然而程序错误在C程序中屡见不鲜,有些错误甚至会导致严重的后果。随着软件规模日益庞大,提高C程序的正确性和可靠性变得愈发重要。MSVL是基于投影时序逻辑的时序逻辑编程语言。可以用于较大规模的软硬件系统建模、仿真和验证。MSVL语言执行效率高,逻辑表达能力强,提供了一种程序验证的新途径。通过将C程序转化为同语义的MSVL程序,再对MSVL程序进行建模、仿真和验证,可以间接验证源C程序的正确性。本文主要研究C-to-MSVL转换系统实现中的关键问题,主要工作如下:1.研究了C语言和MSVL语言的异同,定义了适用于转换系统的C语言标准——Xd-C,并对Xd-C与ANSI C主要的差别进行了阐述,为后续转换提供了理论基础。2.对转换系统的设计框架和执行流程进行优化,并对优化后的转换系统进行了详细的介绍。依照功能将C-to-MSVL转换系统分成预处理模块、词法分析和语法分析模块、转换模块、后期处理模块和集成模块五大模块,并对各个模块的功能及实现细节进行了详尽的说明。3.解决了转... 

【文章来源】：西安电子科技大学陕西省 211工程院校 教育部直属院校

【文章页数】：90 页

【学位级别】：硕士

【部分图文】：

C语言预预处理可执行文件第

第六章 应用示例与测试第六章 应用示例与测试1 C-to-MSVL 转换系统的使用C-to-MSVL 转换系统运行在 Windows 平台上，通过命令行（Command ProceD）使用。在命令行工具中进入到 C2MSVL 的根目录，通过调用 C2MSVL.e指令来运行转换系统。命令格式如下：C2MSVL.exe [参数指令] [文件路径]参数指令及功能在本文 4.6 小节中集成模块已经介绍。图 6.1 展示了参数-行结果：

参数指令及功能在本文 4.6 小节中集成模块已经介绍。图 6.1 展示了参数-行结果：图6.1 C2MSVL 工具帮助说明输入的文件地址是需要转换的 C 语言程序 main 函数入口所在的文件名地址以是相对路径，也可以是绝对路径。下面以快速排序为例，展示 C-to-MSV统的使用方法。

【参考文献】：
期刊论文
[1]Model checking concurrent systems with MSVL[J]. Nan ZHANG,Zhenhua DUAN,Cong TIAN.  Science China（Information Sciences）. 2016(11)
[2]按需时隙分配RFID防碰撞协议研究[J]. 陈毅红,冯全源.  电子学报. 2014(02)
[3]框架时序逻辑语言MSVL中面向对象机制的实现[J]. 王小兵,段振华.  西安电子科技大学学报. 2010(03)
[4]XYZ系统的目的、意义、作用与应用[J]. 唐稚松.  软件学报. 1999(04)

博士论文
[1]面向对象MSVL语言及其在组合Web服务验证中的应用[D]. 王小兵.西安电子科技大学 2009

硕士论文
[1]基于Linux的MSVL编译器和集成开发环境的研究与实现[D]. 张健.西安电子科技大学 2018
[2]MSVL编译器中建模方法的研究与实现[D]. 时一防.西安电子科技大学 2017



本文编号：3577122