混成系統(tǒng)是一種既包含離散成分又包含連續(xù)成分的計算系統(tǒng)，數(shù)控系統(tǒng)等一些與其外 部連續(xù)變化的物理環(huán)境不斷交互的嵌入式系統(tǒng)就是其典型的代表．實時系統(tǒng)是一類特殊的 混成系統(tǒng)，其連續(xù)成分是一組用來表示時間約束條件的時鐘．由于這些系統(tǒng)在工業(yè)及國防 領域有著重要而廣泛的應用，它們的安全性和可靠性越來越引起人們的關注，因而對這些 系統(tǒng)進行形式化分析以確保其安全性和可靠性也成為近年來的一個研究熱點． 為了描述實時及混成系統(tǒng)的性質和行為，十多年來，各種不同的時序邏輯如：Metric Interval Temporal Logic，Real-Time Temporal Logic,Integrator Computation Tree Logic和Hybrid Temporal Logic 等相繼提出，盡管這些時序邏輯作為規(guī)范語言用于描述 實時及混成系統(tǒng)的性質時都還比較合適，但它們不適合用來表示實時及混成系統(tǒng)的實現(xiàn)， 因為它們缺乏表示系統(tǒng)狀態(tài)的動態(tài)變化的能力． 在現(xiàn)有文獻中，實時和混成系統(tǒng)通常是用時間自動機、混成自動機、時間轉換系統(tǒng)和 相位轉換系統(tǒng)等來表示的．但這些系統(tǒng)刻畫語言卻不適合作為規(guī)范語言來使用，因為它們 不能表示實時和混成系統(tǒng)的一些重要性質（如安全性和活性等）．這樣在基于邏輯方法的實 時和混成系統(tǒng)的研究中，系統(tǒng)和它的性質通常是用兩個不同的語言來表示的． 本文定義了一個具有連續(xù)語義的線性時序邏輯，記為 LTLC，它是 Manna和Pnueli 所提出的線性時序邏輯LTL的一個推廣．LTLC既能表示實時和混成系統(tǒng)的性質，又能 很方便地表示實時和混成系統(tǒng)的實現(xiàn)，它能在統(tǒng)一的語義框架中表示出從高級的需求規(guī)范 到低級的實現(xiàn)模型之間的不同抽象層次上的系統(tǒng)描述，并且能用邏輯蘊涵來表示不同抽象 層次的系統(tǒng)描述之間的語義一致性． 本文還定義了LTLC的三個子語言：LTLC/B、LTLC/R及LTLC/H，并證明了 前兩者的可滿足性問題是可判定的．這三個子語言可分別用來表示有窮狀態(tài)反應系統(tǒng)、有窮 控制狀態(tài)實時系統(tǒng)以及混成系統(tǒng)．本文所給的關于 LTLC/B－公式的可滿足性判定過程可 用于檢查有窮狀態(tài)反應系統(tǒng)之間的一致性以及有窮狀態(tài)反應系統(tǒng)與其規(guī)范之間的一致性； 所給的關于LTLC/R-公式的可滿足性判定過程可用于檢查有窮控制狀態(tài)實時系統(tǒng)之間的 一致性以及有窮控制狀態(tài)實時系統(tǒng)與其規(guī)范之間的一致性． 此外，本文還給出了在樣本控制模式下（在此模式下，混成系統(tǒng)的跳躍轉換只發(fā)生在 整數(shù)時間點上）多速率混成系統(tǒng)關于 LTLC/H－公式的一個模型檢查過程．
【學位單位】：中國科學院軟件研究所
【學位級別】：博士
【學位年份】：2001
【中圖分類】：TP302.1;TP302.2
【文章目錄】：
'>

第一章 引 言
    1.1 反應系統(tǒng)
    1.2 實時和混成系統(tǒng)
    1.3 本文的目標、貢獻和組成
第二章 線性時序邏輯LTL簡介
    2.1 線性時序邏輯LTL
    2.2 LTL公式的可滿足性的判定
第三章 連續(xù)語義線性時序邏輯LTLC
    3.1 預備概念
    3.2 LTLC的語法
    3.3 LTLC的語義
    3.4 利用LTLC/B－公式表示有窮狀態(tài)反應系統(tǒng)
    3.5 LTLC/B－公式的可滿足性判定
    3.6 小結
第四章 實時系統(tǒng)
    4.1 基本概念
    4.2 時間模塊及其驗證
    4.3 時間模塊的模型檢查與LTLC/R公式的可滿足性判定
    4.4 小結
第五章 混成系統(tǒng)
    5.1 基本概念
    5.2 混成模塊
    5.3 使用LTLC驗證混成系統(tǒng)的性質
    5.4 多速率成模塊的樣本模型檢查
    5.5 小結
第六章 相關工作
    6.1 實時邏輯
    6.2 實時和混成系統(tǒng)的驗證
第七章 總結
攻讀博士學位期間發(fā)表和錄用的文章
致 謝
'>

【相似文獻】

相關期刊論文 前10條

1 李林輝;劉東;楊冬亮;孫希意;;基于Web計算框架的調度日報系統(tǒng)[J];電力系統(tǒng)自動化;2011年15期

2 吳永剛;陸慧娟;程倬;陳江;;基于時間自動機的實時系統(tǒng)建模及驗證[J];計算機時代;2011年06期

3 ;[J];;年期

4 ;[J];;年期

5 ;[J];;年期

6 ;[J];;年期

7 ;[J];;年期

8 ;[J];;年期

9 ;[J];;年期

10 ;[J];;年期

相關博士學位論文 前10條

1 李廣元;LTLC：面向實時與混成系統(tǒng)的連續(xù)時序邏輯[D];中國科學院軟件研究所;2001年

2 趙劍;混成系統(tǒng)基于模型診斷的若干問題研究[D];吉林大學;2012年

3 田聰;命題投影時序邏輯的判定性、復雜性、表達性及模型檢測[D];西安電子科技大學;2010年

4 舒新峰;投影時序邏輯的完備公理系統(tǒng)與形式驗證[D];西安電子科技大學;2010年

5 楊琛;打結不變的命題投影時序邏輯與模型檢測[D];西安電子科技大學;2010年

6 萬良;基于行為時序邏輯TLA的系統(tǒng)、規(guī)則與協(xié)議檢測的研究[D];貴州大學;2009年

7 陳冬火;超協(xié)調時序邏輯及其模型檢測方法[D];中國科學院研究生院（成都計算機應用研究所）;2006年

8 張海賓;混合系統(tǒng)的形式化驗證[D];西安電子科技大學;2007年

9 龍士工;串空間理論及其在安全協(xié)議分析中的應用研究[D];貴州大學;2007年

10 徐鳴;程序驗證與系統(tǒng)分析中的若干符號計算問題[D];華東師范大學;2010年

相關碩士學位論文 前10條

1 楊琳琳;基于時序邏輯的安全協(xié)議驗證方法的研究[D];南京航空航天大學;2010年

2 費麗娟;構件組裝中“特征干擾問題”的時序邏輯檢測方法研究[D];華中師范大學;2004年

3 尹紅麗;基于時序邏輯的協(xié)商公理體系多Agent系統(tǒng)的形式化模型[D];云南師范大學;2004年

4 伍曉敏;基于VSK-t邏輯的Agent形式化模型[D];云南師范大學;2004年

5 王帆;基于UML的形式化規(guī)范說明研究[D];天津大學;2004年

6 黎吾平;模型檢測在軟件方面的應用[D];吉林大學;2008年

7 劉凱;混成電力系統(tǒng)及其靜態(tài)電壓穩(wěn)定性研究[D];貴州大學;2008年

8 李根;基于SPIN的命題投影時序邏輯模型檢查[D];西安電子科技大學;2008年

9 董護斌;面向實時系統(tǒng)的實時區(qū)域時態(tài)邏輯：RRTL[D];西北大學;2002年

10 吳宏;基于LSC的模型檢驗研究與實現(xiàn)[D];國防科學技術大學;2004年

本文編號：2885776

boshi