信息系統(tǒng)融合系統(tǒng)的網(wǎng)絡化、系統(tǒng)化和信息化等特性使得軟件系統(tǒng)的復雜程度不斷增加。尤其是時間和空間等物理元素的引入使得經(jīng)典的建模方法無法滿足其時空一致性需求,最近陳儀香教授引入了實時系統(tǒng)的規(guī)范語言Spatio-temporal Consistence Language for Real-time Systems(STeC)對時空一致性進行建模和分析。 本文從形式化角度對STeC語言進行研究,使用重寫邏輯建立了STeC語言的Maude語義,利用Maude解釋器對STeC模型進行仿真,開發(fā)了工具對STeC模型進行時空一致性的靜態(tài)分析,搭建了STeC語言的一體化工具,在此基礎上對中國高鐵等例子進行建模分析和邏輯推理。 首先,本文提出了STeC語言的Maude語義模型。Maude語義主要使用關(guān)系等式理論和重寫邏輯理論進行定義,其中對離散時間進行建模分析。通過有效的拓展,本文將STeC語言轉(zhuǎn)化為可執(zhí)行的基于Maude的形式化描述,使用Maude自動推導功能,驗證STeC模型的邏輯正確性。 其次,本文對STeC模型進行靜態(tài)分析,包括詞法、語法分析,時空一致性分析和時鐘滿足性分析。借助目前主流的詞法分析...

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

【學位級別】：碩士

【文章目錄】：
論文摘要
ABSTRACT
第一章 緒論
    1.1 選題的背景和意義
    1.2 研究現(xiàn)狀
    1.3 論文主要研究內(nèi)容和章節(jié)安排
    1.4 本章小結(jié)
第二章 預備知識
    2.1 實時系統(tǒng)規(guī)范語言STeC
    2.2 重寫邏輯理論
    2.3 Maude語言
    2.4 本章小結(jié)
第三章 STeC語言的Maude語義模型
    3.1 STeC語言的Maude語義
    3.2 用例研究
    3.3 本章小結(jié)
第四章 STeC語言的靜態(tài)分析
    4.1 STeC語言解釋器
    4.2 STeC詞法分析
    4.3 STeC語法分析
    4.4 STeC性質(zhì)分析
    4.5 本章小結(jié)
第五章 STeC一體化工具的設計與實現(xiàn)
    5.1 工具總體情況介紹
    5.2 用例分析
    5.3 本章小結(jié)
第六章 總結(jié)與未來展望
    6.1 總結(jié)
    6.2 進一步工作
附錄
    附錄一 STeC語言語法的Maude語義
    附錄二 STeC語言操作語義的Maude語義
    附錄三 實時系統(tǒng)規(guī)范語言STeC靜態(tài)分析工具軟件設計書
參考文獻
后記
攻讀碩士學位期間發(fā)表論文和科研情況



本文編號：3942088