嵌入式實時系統：調度分析和驗證

內容簡介

本書面向嵌入式實時系統，較系統地論述基本的實時調度算法、調度性分析方法，說明引入形式化方法的要性，並為實時系統設計提供一個清晰的形式化方法基礎.其核心是面向實時系統的形式化分析(formalanalysis)及驗證.全書特別列舉了大量關於安全關鍵系統的工程實例，從簡單系統(如溫度控制系統、麵包機和電飯煲)到高度複雜系統(如飛機和太空梭)，通過將上述形式化方法成功套用於這些工程項目，有助於加深讀者對嵌入式實時系統分析和驗證方法的理解和運用。

本書面向高等院校本科生和研究生，作為“嵌入式系統”、“實時系統”相關專業課程教材或教學參考書使用;也可面向業界從業者和研究人員，作為參考書使用。

圖書目錄

第1章　簡　介………………………………………………………………………… 1

1．1　什麼是時間…………………………………………………………………… 2

1．2　仿　真………………………………………………………………………… 3

1．3　測　試………………………………………………………………………… 4

1．4　驗　證…………………………………………企墊漿……………………………… 5

1．5　運行時期監測………………………懂寒蒸………………………………………… 5

1．6　相關資源……………………………………………………………………… 6

第2章　非實時系統的分析與驗證…………………………………………………… 8

2．1　符號邏輯……………………………………………………………………… 8

2．1．1　命題邏輯………………………………………………………………… 8

2．1．2　謂詞邏輯………………………………………………………………… 15

2．2　自動機和語言………………………………………………………………… 22

2．2．1　語言和表示……………………………………………………………… 22

2．2．2　有限自動機……………………………………………………………… 23

2．2．3　非定時系統的規範指定和驗證………………………………………… 25

2．3　歷歸熱店辣史回顧和相關研究………………………………………………………… 29

2．4　總　結………………………………………………………………………… 30

習　題……………………………………………………………………………… 31

第3章　實時調度和調度性分析…………………………………………………… 33

3．1　確定計算時間………………………………………………………………… 34

3．2　單處理器調度………………………………………………………………… 35

3．2．1　獨立可搶占任務的調度………………………………………………… 35

3．2．2　不可搶占任務的調度…………………………………………………… 47

3．2．3　帶前後次序約束的不可搶占任務……………………………………… 48

3．2．4　周期任務間的通信:確定的會合模型………………………………… 50

3．2．5　帶臨界區域的周期任務:核心化監測模型…………………………… 51

3．3　多處理器調度………………………………………………………………… 53

3．3．1　調度表示………………………………………………………………… 53

3．3．2　單實例任務調度………………………………………………………… 54

3．3．3　周期任務調度…………………………………………………………… 56

3．4　可用的調度工具……………………………………………………………… 57

3．4．1　PERTS/RAPIDRMA ……………………………………辯汗幾舟…………… 58

3．4．2　PerfoRMAx ………………捉槓…………………………………………… 59

3．4．3　TimeWiz ……………………………………………………………… 59

3．5　可用的實時作業系統…………………………幾墊櫻……………………………… 60

3．6　歷史回顧和相關研究………………………………………………………匪雄灶… 61

3．7　總　結………………………………………………………………………… 62

習　題……………………………………………………………………………… 67

第4章　有限狀態系統的模型檢測………………………………………………… 70

4．1　系統規範……………………………………………………………………… 70

4．2　CLARKE EMERSON SISTLA 模型檢測器…………………………… 72

4．3　CTL的擴展………………………………………………………………… 76

4．4　應　用………………………………………………………………………… 76

4．5　用C實現的完整的CTL模型檢測器程式………………………………… 79

4．6　符號化模型檢測…………………………………………………………… 101

4．6．1　二元決策圖BDDs …………………………………………………… 101

4．6．2　符號模型檢測器……………………………………………………… 104

4．7　實時CTL ………………………………………………………………… 105

4．7．1　最小和最大延遲……………………………………………………… 105

4．7．2　條件發生的最小和最大數量………………………………………… 107

4．7．3　非單位轉移時間……………………………………………………… 108

4．8　可用的工具………………………………………………………………… 109

4．9　歷史回顧和相關研究……………………………………………………… 110

4．10　總　結……………………………………………………………………… 112

習　題……………………………………………………………………………… 114

第5章　可視形式化、狀態圖和STATEMATE …………………………………… 116

5．1　狀態圖……………………………………………………………………… 117

5．1．1　狀態圖的基本功能…………………………………………………… 117

5．1．2　語　義………………………………………………………………… 120

5．2　活動圖……………………………………………………………………… 121

5．3　模組圖……………………………………………………………………… 121

5．4　STATEMATE …………………………………………………………… 122

5．4．1　形式語言……………………………………………………………… 122

5．4．2　信息檢索和文檔……………………………………………………… 122

5．4．3　代碼的執行和分析…………………………………………………… 122

5．5　可用的工具………………………………………………………………… 123

5．6　歷史回顧和相關研究……………………………………………………… 124

5．7　總　結……………………………………………………………………… 125

習　題……………………………………………………………………………… 126

第6章　實時邏輯、圖論分析與模式圖…………………………………………… 127

6．1　規範和安全聲明…………………………………………………………… 127

6．2　事件動作模型……………………………………………………………… 128

6．3　實時邏輯…………………………………………………………………… 128

6．4　限制性RTL公式………………………………………………………… 130

6．5　不可滿足性的檢測………………………………………………………… 133

6．6　高效的不可滿足性檢測…………………………………………………… 134

6．7　工業例子:美國航空航天局X 38機組返回艙………………………… 137

6．7．1　X 38航空電子體系結構…………………………………………… 137

6．7．2　時序特性……………………………………………………………… 138

6．7．3　使用RTL進行時序和安全分析…………………………………… 138

6．7．4　RTL規範……………………………………………………………… 138

6．7．5　將RTL表示轉化成Presburger算術……………………………… 142

6．7．6　約束圖的分析………………………………………………………… 145

6．8　模式圖規範語言…………………………………………………………… 145

6．8．1　模　式………………………………………………………………… 146

6．8．2　轉　移………………………………………………………………… 147

6．9　驗證模式圖規範的時間屬性……………………………………………… 148

6．9．1　系統運算……………………………………………………………… 148

6．9．2　運算圖………………………………………………………………… 149

6．9．3　時間屬性……………………………………………………………… 149

6．9．4　節點之間的最小和最大距離………………………………………… 150

6．9．5　終點和間隔的排除與納入…………………………………………… 151

6．10　可用的工具………………………………………………………………… 152

6．11　歷史回顧和相關研究……………………………………………………… 152

6．12　總　結……………………………………………………………………… 152

習　題……………………………………………………………………………… 155

第7章　利用時間自動機進行驗證………………………………………………… 158

7．1　Lynch Vaandrager自動機理論方法…………………………………… 158

7．1．1　定時執行……………………………………………………………… 159

7．1．2　定時軌跡……………………………………………………………… 159

7．1．3　時間自動機的組合…………………………………………………… 160

7．1．4　MMT自動機………………………………………………………… 160

7．1．5　驗證技術……………………………………………………………… 161

7．1．6　通過仿真證明時間界限……………………………………………… 163

7．2　AlurGDill自動機理論方法………………………………………………… 163

7．2．1　非定時軌跡…………………………………………………………… 164

7．2．2　定時軌跡……………………………………………………………… 164

7．2．3　Alur Dill時間自動機……………………………………………… 167

7．3　Alur Dill域自動機和驗證……………………………………………… 169

7．3．1　時鐘域………………………………………………………………… 170

7．3．2　域自動機……………………………………………………………… 171

7．3．3　驗證算法……………………………………………………………… 172

7．4　可用的工具………………………………………………………………… 173

7．5　歷史回顧和相關研究……………………………………………………… 174

7．6　總　結……………………………………………………………………… 175

習　題……………………………………………………………………………… 178

第8章　時間相關的Petri網……………………………………………………… 179

8．1　非定時Petri網…………………………………………………………… 179

8．2　帶有時間擴展的Petri網………………………………………………… 181

8．2．1　定時Petri網………………………………………………………… 181

8．2．2　時間Petri網………………………………………………………… 181

8．2．3　高階定時Petri網…………………………………………………… 184

8．3　時間ER網………………………………………………………………… 185

8．4　高階Petri網的屬性……………………………………………………… 189

8．5　TPN 網的BerthomieuGDiaz分析算法…………………………………… 190

8．5．1　從狀態類出發的變遷的可發生性確定……………………………… 191

8．5．2　導出可達類…………………………………………………………… 192

8．6　Milano研究團隊的HLTPN 分析方法…………………………………… 193

8．7　可用的工具………………………………………………………………… 195

8．8　歷史回顧和相關研究……………………………………………………… 195

8．9　總　結……………………………………………………………………… 196

習　題……………………………………………………………………………… 199

第9章　進程代數…………………………………………………………………… 200

9．1　非定時進程代數…………………………………………………………… 200

9．2　Milner的通信系統演算…………………………………………………… 201

9．2．1　行為程式的直接等價………………………………………………… 202

9．2．2　行為程式的全等……………………………………………………… 203

9．2．3價關係:互模擬……………………………………………………… 203

9．3　定時進程代數……………………………………………………………… 204

9．4　通信共享資源的進程代數………………………………………………… 204

9．4．1　ACSR的語法………………………………………………………… 205

9．4．2　ACSR的語義:操作規則……………………………………………… 206

9．4．3　機場雷達系統的例子………………………………………………… 210

9．5　分析和驗證………………………………………………………………… 211

9．5．1　分析的例子…………………………………………………………… 213

9．5．2　VERSA 的使用……………………………………………………… 214

9．5．3　實用性………………………………………………………………… 215

9．6　與其他方法的關係………………………………………………………… 215

9．7　可用的工具………………………………………………………………… 216

9．8　歷史回顧和相關研究……………………………………………………… 216

9．9　總　結……………………………………………………………………… 217

習　題……………………………………………………………………………… 218

第10章　基於命題邏輯規則系統的設計與分析…………………………………… 219

10．1　實時決策系統……………………………………………………………… 219

10．2　實時專家系統……………………………………………………………… 221

10．3　基於命題邏輯規則的程式———EQL語言……………………………… 222

10．3．1　聲明部分……………………………………………………………… 223

10．3．2　初始化部分———初始化INIT和輸入INPUT …………………… 223

10．3．3　規則部分———RULES ……………………………………………… 224

10．3．4　輸出部分……………………………………………………………… 226

10．4　狀態空間表示……………………………………………………………… 228

10．5　計算機輔助設計工具……………………………………………………… 230

10．6　分析問題…………………………………………………………………… 237

10．6．1　有限域………………………………………………………………… 238

10．6．2　特殊形式:對於常量的相容性賦值，L 和T 不相交……………… 239

10．6．3　通用分析策略………………………………………………………… 241

10．7　工業例子:太空梭壓力控制系統的低溫氫壓力故障處理過程分析

……………………………………………………………………………… 242

10．8　綜合問題…………………………………………………………………… 252

10．8．1　調度基於等式規則程式的時間複雜性……………………………… 254

10．8．2　拉格朗日乘子法求解時間預算問題………………………………… 255

10．9　在ESTELLA 中規定終止條件………………………………………… 257

10．9．1　分析方法概述………………………………………………………… 258

10．9．2　規定行為約束斷言的工具…………………………………………… 260

10．9．3　用於Estella的與語境無關的語法………………………………… 267

10．10　兩個工業例子…………………………………………………………… 272

10．10．1　為分析ISA 專家系統而規定循環和退出條件…………………… 272

10．10．2　為分析FCE專家系統而規定斷言………………………………… 274

10．11　Estella———通用分析工具……………………………………………… 278

10．11．1　通用分析算法……………………………………………………… 279

10．11．2　獨立規則集的選擇………………………………………………… 279

10．11．3　相容條件的檢查…………………………………………………… 283

10．11．4　循環退出條件的檢查……………………………………………… 284

10．12　定量時序分析算法……………………………………………………… 286

10．12．1　概　述……………………………………………………………… 286

10．12．2式邏輯語言……………………………………………………… 287

10．12．3　互斥和相容………………………………………………………… 288

10．12．4　高階依賴圖………………………………………………………… 289

10．12．5　程式執行和回響時間……………………………………………… 291

10．12．6　狀態空間圖………………………………………………………… 292

10．12．7　回響時間分析問題和特殊形式…………………………………… 293

10．12．8　特殊形式A 和Algorithm_A ……………………………………… 293

10．12．9　特殊形式A ………………………………………………………… 293

10．12．10　特殊形式D和Algorithm_D …………………………………… 295

10．12．11　通用分析算法……………………………………………………… 302

10．12．12　一些證明…………………………………………………………… 304

10．13　歷史回顧和相關研究…………………………………………………… 308

10．14　總　結…………………………………………………………………… 310

習　題……………………………………………………………………………… 312

第11章　基於謂詞邏輯規則系統的時序分析…………………………………… 314

第12章　基於規則系統的最佳化…………………………………………………… 377

參考文獻　…………………………………………………………………………… 404

嵌入式實時系統：調度分析和驗證

基本介紹

內容簡介

圖書目錄

相關詞條

熱門詞條