發(fā)布時(shí)間：2021-01-26 02:34

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

【文章來(lái)源】：華東師范大學(xué)上海市 211工程院校 985工程院校 教育部直屬院校

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

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

【部分圖文】：

查找當(dāng)前活動(dòng)子進(jìn)程的示例

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

CoqIDE中的交互式證明會(huì)話

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

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

碩士論文
[1]UML模型一致性檢測(cè)的研究與設(shè)計(jì)[D]. 朱晨.上海交通大學(xué) 2007



本文編號(hào)：3000318