發(fā)布時(shí)間：2022-01-08 19:13

　　C語言是一門通用的高級(jí)程序設(shè)計(jì)語言。C語言以其靈活高效、功能豐富和可移植性強(qiáng)等優(yōu)點(diǎn),廣泛應(yīng)用于系統(tǒng)軟件與應(yīng)用軟件的開發(fā)中。然而程序錯(cuò)誤在C程序中屢見不鮮,有些錯(cuò)誤甚至?xí)䦟?dǎo)致嚴(yán)重的后果。隨著軟件規(guī)模日益龐大,提高C程序的正確性和可靠性變得愈發(fā)重要。MSVL是基于投影時(shí)序邏輯的時(shí)序邏輯編程語言�？梢杂糜谳^大規(guī)模的軟硬件系統(tǒng)建模、仿真和驗(yàn)證。MSVL語言執(zhí)行效率高,邏輯表達(dá)能力強(qiáng),提供了一種程序驗(yàn)證的新途徑。通過將C程序轉(zhuǎn)化為同語義的MSVL程序,再對(duì)MSVL程序進(jìn)行建模、仿真和驗(yàn)證,可以間接驗(yàn)證源C程序的正確性。本文主要研究C-to-MSVL轉(zhuǎn)換系統(tǒng)實(shí)現(xiàn)中的關(guān)鍵問題,主要工作如下:1.研究了C語言和MSVL語言的異同,定義了適用于轉(zhuǎn)換系統(tǒng)的C語言標(biāo)準(zhǔn)——Xd-C,并對(duì)Xd-C與ANSI C主要的差別進(jìn)行了闡述,為后續(xù)轉(zhuǎn)換提供了理論基礎(chǔ)。2.對(duì)轉(zhuǎn)換系統(tǒng)的設(shè)計(jì)框架和執(zhí)行流程進(jìn)行優(yōu)化,并對(duì)優(yōu)化后的轉(zhuǎn)換系統(tǒng)進(jìn)行了詳細(xì)的介紹。依照功能將C-to-MSVL轉(zhuǎn)換系統(tǒng)分成預(yù)處理模塊、詞法分析和語法分析模塊、轉(zhuǎn)換模塊、后期處理模塊和集成模塊五大模塊,并對(duì)各個(gè)模塊的功能及實(shí)現(xiàn)細(xì)節(jié)進(jìn)行了詳盡的說明。3.解決了轉(zhuǎn)... 

【文章來源】：西安電子科技大學(xué)陜西省 211工程院校 教育部直屬院校

【文章頁數(shù)】：90 頁

【學(xué)位級(jí)別】：碩士

【部分圖文】：

C語言預(yù)預(yù)處理可執(zhí)行文件第

第六章 應(yīng)用示例與測(cè)試第六章 應(yīng)用示例與測(cè)試1 C-to-MSVL 轉(zhuǎn)換系統(tǒng)的使用C-to-MSVL 轉(zhuǎn)換系統(tǒng)運(yùn)行在 Windows 平臺(tái)上，通過命令行（Command ProceD）使用。在命令行工具中進(jìn)入到 C2MSVL 的根目錄，通過調(diào)用 C2MSVL.e指令來運(yùn)行轉(zhuǎn)換系統(tǒng)。命令格式如下：C2MSVL.exe [參數(shù)指令] [文件路徑]參數(shù)指令及功能在本文 4.6 小節(jié)中集成模塊已經(jīng)介紹。圖 6.1 展示了參數(shù)-行結(jié)果：

參數(shù)指令及功能在本文 4.6 小節(jié)中集成模塊已經(jīng)介紹。圖 6.1 展示了參數(shù)-行結(jié)果：圖6.1 C2MSVL 工具幫助說明輸入的文件地址是需要轉(zhuǎn)換的 C 語言程序 main 函數(shù)入口所在的文件名地址以是相對(duì)路徑，也可以是絕對(duì)路徑。下面以快速排序?yàn)槔�，展�?C-to-MSV統(tǒng)的使用方法。

【參考文獻(xiàn)】：
期刊論文
[1]Model checking concurrent systems with MSVL[J]. Nan ZHANG,Zhenhua DUAN,Cong TIAN.  Science China（Information Sciences）. 2016(11)
[2]按需時(shí)隙分配RFID防碰撞協(xié)議研究[J]. 陳毅紅,馮全源.  電子學(xué)報(bào). 2014(02)
[3]框架時(shí)序邏輯語言MSVL中面向?qū)ο髾C(jī)制的實(shí)現(xiàn)[J]. 王小兵,段振華.  西安電子科技大學(xué)學(xué)報(bào). 2010(03)
[4]XYZ系統(tǒng)的目的、意義、作用與應(yīng)用[J]. 唐稚松.  軟件學(xué)報(bào). 1999(04)

博士論文
[1]面向?qū)ο驧SVL語言及其在組合Web服務(wù)驗(yàn)證中的應(yīng)用[D]. 王小兵.西安電子科技大學(xué) 2009

碩士論文
[1]基于Linux的MSVL編譯器和集成開發(fā)環(huán)境的研究與實(shí)現(xiàn)[D]. 張健.西安電子科技大學(xué) 2018
[2]MSVL編譯器中建模方法的研究與實(shí)現(xiàn)[D]. 時(shí)一防.西安電子科技大學(xué) 2017



本文編號(hào)：3577122