【摘要】：模型檢測最重要的特性之一是能夠為不滿足的時態(tài)屬性生成反例。反例可以為工程師提供調試信息,以進一步解釋屬性的違反情況。然而,在模型檢測的發(fā)展中,迄今為止對反例的研究依然很少。已有的最先進的符號化模型檢測工具在規(guī)范描述上表達力不足,僅能驗證實時時態(tài)認知邏輯的小部分子集,而且產(chǎn)生的反例相對簡單、不完整、并且缺乏便于理解的注釋。為此,本文首次提出了一種新的實時分支時態(tài)認知邏輯RTCTL~*K,它是計算樹邏輯CTL~*結合了實時區(qū)間和認知的擴展,使得實時相關性質、智能體認知狀態(tài)及兩者共同作用下,即某時間區(qū)間內智能體的認知可達關系可以被方便地描述和驗證。然后我們給出了基于測試器的符號化反例生成算法,深度改進并實現(xiàn)了新的模型檢測工具,使其能夠自動為RTCTL~*K生成足夠簡潔的圖形化反例,更易于直觀分析。本文主要研究工作包括定義RTCTL~*K的語法語義,給出反例生成算法并實現(xiàn)符號化模型檢測工具—MCTK2,具體如下:(1)我們定義了表達能力更強的實時分支時態(tài)認知邏輯RTCTL~*K,它是CTL~*的一個擴展,同時具有離散的時間區(qū)間和認知邏輯。(2)基于公平性離散系統(tǒng)JDS,我們設計了RTCTL~*K的反例生成算法。生成的反例是具有分支結構的有向狀態(tài)遷移圖。為便于理解,在圖中的狀態(tài)和遷移關系上附有一些滿足的子公式來加以注釋,每個強連通的分量都是一個循環(huán),對應的分量圖是樹狀結構。而且,為避免產(chǎn)生龐大的樹狀模型圖,子公式的證據(jù)將依據(jù)用戶需要而交互式產(chǎn)生。由于圖上每個節(jié)點均是可交互的,對于附加在狀態(tài)上的每個未解釋的子公式(前面含有路徑量詞或認知算子),當用戶單擊該狀態(tài)時,從當前狀態(tài)會創(chuàng)建出新的分支。而且對于JDS上RTCTL~*K的全稱片段,我們證明了其反例生成算法的完備性。(3)開發(fā)了一個符號化模型檢測工具MCTK2,并實現(xiàn)了RTCTL~*K的反例生成算法。通過與著名的模型檢驗器nuXmv和MCMAS進行一系列實驗比較,分析結果表明,相比于nuXmv,MCTK2在驗證RTLTL公式并產(chǎn)生反例的時間效率上優(yōu)于nuXmv,在易用性以及驗證CTL~*K、RTLTL、RTCTL~*公式并產(chǎn)生反例的時間消耗和內存占用方面均優(yōu)于MCMAS。
【學位授予單位】：華僑大學
【學位級別】：碩士
【學位授予年份】：2019
【分類號】：TP274
【圖文】：

RTCTL*K的模型檢測流程

公式的樹狀證據(jù)對于本例中的公式來說，它是無法由CTL*(包括其子集CTL和LTL)來表

【參考文獻】

相關期刊論文 前2條

1 部德振;;帶時間約束的LTL性質的模型檢測的實現(xiàn)[J];計算機工程與設計;2011年02期

2 駱翔宇;蘇開樂;顧明;;一種求解認知難題的模型檢測方法[J];計算機學報;2010年03期

本文編號：2729087