反應(yīng)式和并發(fā)系統(tǒng)的時(shí)序邏輯

 
 
 
第Ⅰ部分并 發(fā) 模 型
第1章基本模型
1.1通用模型
1.1.1基礎(chǔ)語言
1.1.2基本轉(zhuǎn)換系統(tǒng)
1.1.3轉(zhuǎn)換關(guān)系ρτ
1.1.4使能與非使能轉(zhuǎn)換
1.1.5空轉(zhuǎn)換與勤勉轉(zhuǎn)換
1.1.6計(jì)算
1.1.7具體模型
1.2模型1： 轉(zhuǎn)換圖
1.2.1聲明
1.2.2進(jìn)程
1.2.3基本轉(zhuǎn)換系統(tǒng)圖
1.2.4用交錯表示并發(fā)性
1.2.5調(diào)度
1.3模型2： 共享變量文本
1.3.1簡單語句
1.3.2復(fù)合語句
1.3.3程序
1.3.4文本程序中的標(biāo)記
1.3.5標(biāo)記等價(jià)關(guān)系
1.3.6文本語言中的位置
1.4共享變量文本語義
1.4.1狀態(tài)變量和狀態(tài)
1.4.2轉(zhuǎn)換
1.4.3初始條件
1.4.4計(jì)算
1.4.5下標(biāo)變量
1.5語句間的結(jié)構(gòu)關(guān)系
1.5.1子語句
1.5.2控制謂詞at、after和in
1.5.3語句的使能性
1.5.4進(jìn)程和并行語句
1.5.5競爭語句
1.6行為等價(jià)
1.6.1初步近似
1.6.2可觀測和可簡化的行為
1.6.3轉(zhuǎn)換系統(tǒng)的等價(jià)性
1.6.4語句一致性
1.6.5例子
1.6.6模擬與實(shí)現(xiàn)
1.7分組語句
1.7.1分組語句
1.7.2與分組語句關(guān)聯(lián)的轉(zhuǎn)換
1.8信號量語句
1.8.1信號量需求
1.8.2信號量語句
1.8.3互斥信號量的應(yīng)用
1.8.4信號量的其他應(yīng)用
1.9區(qū)域語句
1.9.1比較信號量和區(qū)域語句
1.9.2選擇語句中的同步
1.10模型3： 消息傳遞文本
1.10.1通信語句
1.10.2緩沖能力
1.10.3例子
1.10.4條件通信語句
1.10.5同步模型和異步模型的比較
1.10.6公平服務(wù)器
1.11模型4： Petri網(wǎng)
1.11.1網(wǎng)
1.11.2標(biāo)記
1.11.3圖形化表示
1.11.4點(diǎn)火
1.11.5Petri系統(tǒng)
1.11.6例子
問題
文獻(xiàn)注釋
 
第2章真并發(fā)模型
2.1交錯和并發(fā)
2.1.1重疊執(zhí)行
2.1.2交錯計(jì)算
2.1.3細(xì)粒度
2.2限制臨界引用
2.2.1臨界引用
2.2.2語句的LCR約束
2.2.3LCR程序
2.2.4需要額外保護(hù)
2.2.5每個程序都有一個LCR精化
2.2.6每個程序都有一個LCR等價(jià)
2.2.7語義臨界引用
2.2.8合并語句
2.2.9with語句
2.3弱公平性
2.3.1公平性需求
2.3.2不公平計(jì)算
2.3.3弱公平性
2.3.4弱公平性需求
2.4弱公平性需求的含義
2.4.1不能保證選擇公平性
2.4.2轉(zhuǎn)換弱公平性與進(jìn)程弱公平性
2.4.3弱公平性調(diào)度
2.4.4不能檢測弱公平性
2.4.5非公平轉(zhuǎn)換
2.5強(qiáng)公平性
2.5.1弱公平性不足
2.5.2強(qiáng)公平性需求
2.5.3強(qiáng)公平性調(diào)度
2.6同步語句
2.7通信語句
2.7.1同步通信互斥
2.7.2異步通信互斥
2.8總結(jié): 公平轉(zhuǎn)換系統(tǒng)
2.9Petri網(wǎng)公平性
2.9.1弱公平性
2.9.2非一元網(wǎng)轉(zhuǎn)換的強(qiáng)公平性
2.9.3互斥
2.10公平性語義
2.10.1公平性防止有限區(qū)分
2.10.2公平性和隨機(jī)選擇
問題
文獻(xiàn)注釋
第Ⅱ部分規(guī)約
第3章時(shí)序邏輯
3.1狀態(tài)公式
3.1.1狀態(tài)語言
3.1.2狀態(tài)公式語義
3.2時(shí)序公式： 將來算子
3.3時(shí)序公式： 過去算子
3.3.1簡單例子
3.3.2可滿足性和有效性
3.3.3等價(jià)性、一致性和蘊(yùn)涵性
3.3.4可替換性
3.3.5過去公式和將來公式
3.3.6的較弱形式
3.3.7算子的基本集合
3.3.8限制型算子
3.4時(shí)序算子的基本屬性
3.4.1模式及其有效性
3.4.2單調(diào)性
3.4.3自反性
3.4.4限制性
3.4.5擴(kuò)展性
3.4.6對偶性
3.4.7強(qiáng)算子和弱算子
3.4.8冪等性
3.4.9吸收性
3.4.10上一時(shí)刻和下一時(shí)刻的交換性
3.4.11全稱算子和存在算子
3.4.12引用變量的下一個值和前一個值
3.4.13語義弱公平性
3.5證明系統(tǒng)
3.6證明系統(tǒng)公理
3.6.1將來公理
3.6.2過去公理
3.6.3混合公理
3.6.4狀態(tài)重言式公理
3.7基本推理規(guī)則
3.7.1泛化規(guī)則和特指規(guī)則
3.7.2替換規(guī)則
3.7.3分離規(guī)則
3.8導(dǎo)出規(guī)則
3.8.1指定規(guī)則
3.8.2命題推理規(guī)則
3.8.3蘊(yùn)涵分離規(guī)則
3.8.4蘊(yùn)涵命題推理規(guī)則
3.8.5從蘊(yùn)涵到規(guī)則
3.8.6證明舉例
3.9等詞和量詞
3.9.1參數(shù)化的句子符號
3.9.2帶參數(shù)模式的規(guī)則GEN
3.9.3帶量詞公式的規(guī)則INST
3.9.4變量替換
3.9.5等詞公理
3.9.6框架公理
3.9.7證明舉例
3.9.8變量的下一個值和前一個值
3.9.9量詞公理
3.9.10量詞規(guī)則
3.9.11證明舉例
3.10從一般有效性到程序有效性
3.10.1計(jì)算對應(yīng)的模型
3.10.2程序有效性和狀態(tài)有效性
3.10.3擴(kuò)展演繹系統(tǒng)
3.10.4建立P狀態(tài)有效性
3.10.5建立P有效性
3.10.6程序依賴規(guī)則
3.10.7導(dǎo)出規(guī)則
3.10.8時(shí)序語義公理
問題
文獻(xiàn)注釋
第4章程序?qū)傩?br />4.1局部語言
4.1.1位置謂詞
4.1.2轉(zhuǎn)換的使能性
4.1.3終止謂詞
4.1.4轉(zhuǎn)換謂詞
4.1.5通信謂詞
4.1.6規(guī)約變量
4.2屬性分類
4.2.1安全性
4.2.2保證性
4.2.3義務(wù)性
4.2.4響應(yīng)性
4.2.5持續(xù)性
4.2.6反應(yīng)性
4.2.7反應(yīng)性類是最大的類
4.2.8分類
4.2.9標(biāo)準(zhǔn)公式
4.2.10安全性活性分類
4.3安全性例子： 狀態(tài)不變性
4.3.1全局不變性
4.3.2部分正確性
4.3.3無死鎖性
4.3.4局部無死鎖性
4.3.5容錯性
4.3.6互斥性
4.3.7通信事件的不變性
4.4安全性例子： 過去不變性
4.4.1單調(diào)性
4.4.2缺乏主動響應(yīng)
4.4.3無重復(fù)輸出
4.4.4先進(jìn)先出
4.4.5嚴(yán)格優(yōu)先性
4.4.6有界超越
4.5進(jìn)展性例子： 從保證性到反應(yīng)性
4.5.1終止性和完全正確性
4.5.2保證性事件
4.5.3間歇斷言
4.5.4無個體饑荒和無活鎖
4.5.5可訪問性
4.5.6確保響應(yīng)
4.5.7最終有界性
4.5.8表示公平性需求
4.5.9最終可靠性
4.6例子： 資源分配
4.6.1消息傳遞方式
4.6.2消息傳遞方式的安全性
4.6.3消息傳遞方式的進(jìn)展性
4.6.4共享變量方式
4.6.5共享變量方式的安全性
4.6.6共享變量方式的進(jìn)展性
4.7規(guī)約語言表達(dá)能力
4.7.1觀察奇偶性
4.7.2量詞公式描述奇偶性
4.7.3有重復(fù)輸入的緩沖
4.7.4量詞公式描述緩沖
4.7.5通信歷史變量
4.8反應(yīng)模塊規(guī)約
4.8.1模塊語句
4.8.2模塊規(guī)約
4.8.3執(zhí)行模塊的任務(wù)
4.8.4模塊實(shí)現(xiàn)的障礙
4.8.5模塊的計(jì)算
4.9復(fù)合模塊規(guī)約
4.9.1層次分解
4.9.2更改超越一次的變量
4.9.3分解安全性規(guī)約
4.9.4異步通信模塊
4.9.5同步通信模塊
4.9.6資源重新分配
問題
文獻(xiàn)注釋
參考文獻(xiàn)