本文主要討論一個(gè)框架時(shí)序邏輯程序設(shè)計(jì)語(yǔ)言FTLL （Framed Temporal Logic Programming Language）的解釋器及一個(gè)基于命題投影時(shí)序邏輯PPTL （Proposition Projection Temporal Logic）進(jìn)行性質(zhì)描述的模型檢測(cè)工具的實(shí)現(xiàn)。文中首先介紹了實(shí)現(xiàn)解釋器的基于范式的基本方法,然后給出了解釋器的基本框架并詳細(xì)說明了各個(gè)模塊的功用。此外還對(duì)FTLL中幾個(gè)重要的結(jié)構(gòu)的實(shí)現(xiàn)做了詳細(xì)說明,包括框架、等待、投影、指針等操作。作為該解釋器應(yīng)用,它可以作為由OWL-S描述的抽象模型的模擬器,文中給出了一個(gè)詳細(xì)的例子。隨后,本文介紹了用FTLL為系統(tǒng)建模,PPTL進(jìn)行性質(zhì)描述,然后分別將系統(tǒng)和性質(zhì)的非轉(zhuǎn)換為各自的范式,接著對(duì)范式求交,并找它們的模型,看能否找到反例,從而進(jìn)行模型檢測(cè)的方法。并介紹了一個(gè)以此實(shí)現(xiàn)的模型檢測(cè)工具,并給出了算法和一個(gè)例子。文章最后回顧了現(xiàn)有的模型檢測(cè)工具。 

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

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

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

【部分圖文】：

Present與Remains的輸出例子

})這個(gè)程序的執(zhí)行結(jié)果如圖3.6所示。圖3.6 程序執(zhí)行結(jié)果3.4.2 電路仿真時(shí)序邏輯可以用來(lái)模擬邏輯電路的運(yùn)行過程，部分基本的門電路用邏輯公式模擬如下：28

第三章 解釋器的設(shè)計(jì)與實(shí)現(xiàn)，一旦有溢出，控制器就會(huì)終止運(yùn)算并報(bào)路可以由時(shí)序邏輯公式來(lái)描述，而上面例子的門電路構(gòu)成，所以我們可以用時(shí)序邏輯塊，并組成一個(gè)完整的程序。邏輯電路就是驗(yàn)證輸入任何一個(gè)整數(shù)，在結(jié)果1，此處，為了不至于程序執(zhí)中行過程行過程，如圖3.8所示。圖中左邊中括號(hào)內(nèi)右邊為高位，括號(hào)右邊的整數(shù)為十進(jìn)制的過程中，值不能超過255，否則就會(huì)溢出。16，8，4，2，1這幾個(gè)數(shù)的變化，最終變想的正確性。


本文編號(hào)：3450452