隨著現(xiàn)代計算機系統(tǒng)的規(guī)模越來越大、復雜性越來越高,如何開發(fā)可信的軟硬件系統(tǒng)已經(jīng)成為計算機科學發(fā)展的巨大挑戰(zhàn)。形式化方法是以數(shù)學理論為基礎,對計算機系統(tǒng)進行嚴格地規(guī)約、建模與驗證,實現(xiàn)系統(tǒng)的可信驗證。形式化方法已經(jīng)成為軟件開發(fā)過程中不可或缺的一個環(huán)節(jié),如何使用交互式的定理證明器對軟件系統(tǒng)進行機械定義與驗證是其中的一個研究重點。通過機械證明模型中的定理可以找出模型中存在的問題和漏洞,從而進一步提高模型的可靠性。本文的工作致力于研究軟件開發(fā)過程中不同層次的形式語義驗證,以代碼層面的多線程離散事件仿真語言和系統(tǒng)建模層面的統(tǒng)一建模語言為研究對象,提出了將基于定理證明器Coq的機械驗證引入到形式語義驗證的研究中,使得基于Coq的機械驗證涵蓋整個軟件開發(fā)生命周期。多線程離散事件仿真語言MDESL是一種類似于Verilog的底層硬件描述語言,在定理證明器Coq中實現(xiàn)了從MDESL代數(shù)語義中機械生成操作語義的過程,并且機械驗證了生成操作語義的正確性和完備性�；诔绦蚪y(tǒng)一理論（UTP）,使用Coq中的高階邏輯特性對MDESL的指稱語義進行機械刻畫,對代數(shù)定律的正確性進行機械驗證。統(tǒng)一建模語言UML是一種通... 

【文章來源】：華東師范大學上海市 211工程院校 985工程院校 教育部直屬院校

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

【學位級別】：博士

【部分圖文】：

查找當前活動子進程的示例

UML的發(fā)展歷史[5]

CoqIDE中的交互式證明會話

【參考文獻】：
期刊論文
[1]形式化方法概貌[J]. 王戟,詹乃軍,馮新宇,劉志明.  軟件學報. 2019(01)

博士論文
[1]移動分布式系統(tǒng)的進程演算BigrTiMo及其形式語義研究[D]. 謝宛玲.華東師范大學 2019
[2]UML動態(tài)行為圖的機械語義形式驗證與精化研究[D]. 竇亮.華東師范大學 2015

碩士論文
[1]UML模型一致性檢測的研究與設計[D]. 朱晨.上海交通大學 2007



本文編號：3000318