本書主要介紹信息物理融合系統(tǒng)的基本理論，包括系統(tǒng)設計、規(guī)約、建模和分析方法。針對基于模型的設計、并發(fā)理論、分布式算法、規(guī)約和驗證的形式化方法、控制理論、實時系統(tǒng)和混成系統(tǒng)等分支學科，從不同側面對信息物理融合系統(tǒng)進行描述。本書采用數(shù)學化的建模、基于模型的設計，以及規(guī)約與分析等概念，并配以案例研究圖解來闡述信息物理系統(tǒng)所涉及的分布式算法、網(wǎng)絡協(xié)議、控制設計和機器人等理論。本書適合作為計算科學、計算機工程和電子工程相關學科的高年級本科生或一年級研究生的教材。
PrinciplesofCyber-PhysicalSystems信息物理融合系統(tǒng)由能夠相互通信的計算設備組成，這些計算設備借助傳感器和作動器實現(xiàn)與物理世界的交互�，F(xiàn)實生活中，這樣的系統(tǒng)越來越多，從智能建筑到醫(yī)療設備再到汽車都可以看作信息物理融合系統(tǒng)。在過去的十多年中，開發(fā)確保信息物理融合系統(tǒng)可靠性的設計和分析工具是一項具有挑戰(zhàn)性的工作，它吸引了眾多學術界和工業(yè)界的研究人員開展卓有成效的跨學科研究。
本書的目標是為信息物理融合系統(tǒng)的設計、規(guī)約、建模和分析提供一套基本理論，這些理論勾畫了開發(fā)信息物理融合系統(tǒng)所涉及的眾多分支學科，包括基于模型的設計方法、并發(fā)理論、分布式算法、規(guī)約和驗證的形式化方法、控制理論、實時系統(tǒng)和混成系統(tǒng)。我試圖為信息物理融合系統(tǒng)設計和分析方法相關的研究主題提供一套脈絡清晰的理論思想。全書采用數(shù)學化的建模、規(guī)約與分析等概念，并配以案例研究圖解來闡述信息物理系統(tǒng)所涉及的分布式算法、網(wǎng)絡協(xié)議、控制設計和機器人等多學科分支理論。
本教材自成體系，適合作為計算科學、計算機工程和電子工程相關學科的高年級本科生或一年級研究生一學期課程的教材。第1章討論了幾種可供選擇的課程組合。
我對信息物理融合系統(tǒng)的研究興趣萌生于20世紀90年代和TomHenzinger合作研究混成系統(tǒng)協(xié)同性。另外，本教材的結構基于我與Tom合作撰寫但未出版的課堂講義《Computer-AidedVerification》（計算機輔助驗證），其中，第２章和第３章中的一些例子和圖例也來自該講義，并得到Tom的同意。因此，Tom對本教材的貢獻是不可估量的，我對他表達崇高的敬意。
我對信息物理融合系統(tǒng)的理解和本書的內容深受賓夕法尼亞大學工程學院RECISE信息物理融合系統(tǒng)研究中心的學生和同事的影響。在此，我對我的同事VijayKumar、InsupLee、RahulMangharam、GeorgePappas、LinhPhan、OlegSokolsky和UfukTopcu給予的合作與支持表示敬意。同時，我還要感謝DARPA和NSF在信息物理融合系統(tǒng)研究項目上對我的持續(xù)資助。
在過去的５年中，我已經(jīng)勾畫出了本教材的草稿，取名《PrinciplesofEmbeddedComputation》（嵌入式計算的基本原理），最初目標是在賓夕法尼亞大學開設一門嵌入式系統(tǒng)碩士研究生課程。定期教授這門課程是促使我完成本書的關鍵動因，學生的反饋也極大地促進了本教材內容的完善。感謝所有的學生和勤勉的助教，他們是SanjianChen、ZhihaoJiang、SalarMoarref、TruongNghiem、NimitSinghania和RahulVasist。
我也很幸運地收到了其他大學的研究者對本教材手稿的反饋建議。特別是根據(jù)SriramSankaranarayanan和PauloTabuada的建議，對第6章和第9章的內容進行了很多修改。特別感謝ChristosStergiou對最新版本進行了仔細的推敲，并對第9章的例子用Matlab工具進行模擬。
借此機會感謝出版商（MIT出版社）對本項目的支持，特別是VirginiaCrossman、MarieLufkinLee和MarcLowenthal在本書出版過程中提供了大量的幫助和鼓勵。本書的寫作耗時多年，如果沒有家人的支持也是不可能完成的，我要特別感謝我妻子Mona的友善、愛和耐心。
RajeevAlur美國費城賓夕法尼亞大學2015年1月
譯者序PrinciplesofCyber-PhysicalSystems進入21世紀，以計算機科學為代表的信息技術發(fā)展迅猛，一些代表新技術發(fā)展的計算技術名詞泉涌而出，如物聯(lián)網(wǎng)、互聯(lián)網(wǎng)+、云計算、大數(shù)據(jù)、工業(yè)4.0等，而信息物理融合系統(tǒng)（Cyber-PhysicalSystem，CPS）是其中最為引人關注的技術熱詞之一。CPS作為一個正式的概念于2006年由美國國家自然基金委員會科學家HelenGates提出后，就被美國、歐盟和中國等各國政府定位為影響未來科技研究、國家信息技術與產(chǎn)業(yè)融合發(fā)展的國家戰(zhàn)略目標，并制定了一系列的CPS技術研究和產(chǎn)業(yè)發(fā)展計劃。
從技術上講，CPS是為解決信息技術對傳統(tǒng)產(chǎn)品數(shù)字化后所帶來的問題進行的一次系統(tǒng)性思考。這些問題包括：數(shù)值計算誤差積累、跨平臺的計算時序性、開環(huán)控制的不確定性、分布式計算的網(wǎng)絡時延、多核計算的調度性以及長生命周期產(chǎn)品的運維等。這些問題逐步成為一道阻礙新一代智能計算技術發(fā)展必須跨越的鴻溝。這就要求計算技術專家必須另辟計算科學的方法論和實踐工程技術，指導工程技術人員在產(chǎn)品的策劃和設計之初就用系統(tǒng)工程的觀點，考慮貫穿于產(chǎn)品全生命周期的兩類因素——物理過程和計算過程，以及它們之間的相互影響。
CPS技術的發(fā)展不僅要繼承嵌入式系統(tǒng)、網(wǎng)絡通信和控制論的技術和方法，同時還要對現(xiàn)有理論、技術框架進行突破和創(chuàng)新。CPS系統(tǒng)集成了計算過程和物理過程，并且物理過程與計算過程相互影響、深度融合。CPS的概念也指出了CPS的兩條發(fā)展路徑：物理系統(tǒng)的信息化和計算系統(tǒng)的物理化。這兩條道路是將導致CPS的研究、開發(fā)和應用的多樣化發(fā)展，還是將殊途同歸、形成一套統(tǒng)一的理論和方法，還有待于廣大的CPS技術研究開發(fā)人員通過進一步的努力來驗證，我們將拭目以待。
本書從計算理論的角度總結了CPS技術必須考慮的理論方法，并綜合了分布式控制和網(wǎng)絡通信等相關技術，是一本系統(tǒng)介紹信息物理融合系統(tǒng)理論基礎的教材或者工具書，不僅適合初學者，還適用于有相關經(jīng)驗的研究人員和工程技術人員。本書不但概述了信息物理融合系統(tǒng)的基本原理，而且詳細介紹了對此類系統(tǒng)的規(guī)約、設計、建模和分析等一套理論，包括基于模型的設計方法、并發(fā)理論、分布式算法、形式化規(guī)約和驗證方法、控制理論、實時系統(tǒng)和混成系統(tǒng)等，并配以案例分析來闡述信息物理系統(tǒng)所涉及的分布式算法、網(wǎng)絡協(xié)議、控制設計和機器人等多學科分支理論。本書的選材和作為教材的特點在前言和第1章中已有詳述，被世界名校采納作為教材也充分說明了其價值，此處不再贅述。
本書的翻譯主要由董云衛(wèi)博士和張雨博士共同完成，西北工業(yè)大學嵌入式系統(tǒng)實驗室的葛永琪、吳婷婷、魏曉敏、孫鵬鵬、賀媛媛、姜臻穎、魏昕和李峰等研究生也參與了本書的部分翻譯和校對，他們?yōu)楸緯某霭娓冻隽诵燎趧趧印?
由于中西方文化背景上的差異以及我們的學術和語言水平的限制，譯文中難免有不妥甚至錯誤之處，歡迎讀者及專家批評指正。
譯者2016年10月1日于西安
目 錄
Principles of Cyber-Physical Systems
出版者的話
譯者序
前言
第1章 簡介1
1.1 什么是信息物理融合系統(tǒng)1
1.2 信息物理融合系統(tǒng)的主要特征1
1.3 研究主題概述3
1.4 課程組織指南5
第2章 同步模型8
2.1 反應式構件8
2.1.1 變量、值和表達式8
2.1.2 輸入、輸出和狀態(tài)9
2.1.3 初始化9
2.1.4 更新10
2.1.5 執(zhí)行11
2.1.6 擴展狀態(tài)機12
2.2 構件屬性13
2.2.1 有限狀態(tài)構件13
2.2.2 復合構件14
2.2.3 事件觸發(fā)構件*14
2.2.4 非確定性構件16
2.2.5 輸入使能構件17
2.2.6 任務圖和等待依賴關系18
2.3 構件構成22
2.3.1 方框圖22
2.3.2 輸入/輸出變量重命名23
2.3.3 并行組合23
2.3.4 輸出隱藏29
2.4 同步設計30
2.4.1 同步電路30
2.4.2 巡航控制系統(tǒng)33
2.4.3 同步網(wǎng)絡*36
參考文獻說明38
第3章 安全性需求40
3.1 安全性規(guī)約40
3.1.1 遷移系統(tǒng)的不變量40
3.1.2 需求在系統(tǒng)設計中的作用43
3.1.3 安全監(jiān)控器46
3.2 驗證不變量48
3.2.1 證明不變量48
3.2.2 不變量的自動驗證*52
3.2.3 基于模擬的分析54
3.3 枚舉搜索*55
3.4 符號搜索60
3.4.1 符號遷移系統(tǒng)60
3.4.2 符號廣度優(yōu)先搜索63
3.4.3 約簡有序二叉判定圖*67
參考文獻說明75
第4章 異步模型77
4.1 異步進程77
4.1.1 狀態(tài)、輸入和輸出77
4.1.2 輸入、輸出和內部動作78
4.1.3 執(zhí)行80
4.1.4 擴展的狀態(tài)機82
4.1.5 進程操作83
4.1.6 安全性需求87
4.2 異步設計原語88
4.2.1 阻塞同步與非阻塞同步88
4.2.2 死鎖88
4.2.3 共享存儲器90
4.2.4 公平性假設*95
4.3 異步協(xié)調協(xié)議100
4.3.1 領導選舉100
4.3.2 可靠傳輸103
4.3.3 等待無關共識*105
參考文獻說明110
第5章 活性需求111
5.1 時序邏輯111
5.1.1 線性時序邏輯111
5.1.2 LTL規(guī)約116
5.1.3 異步進程的LTL規(guī)約*118
5.1.4 超越LTL*121
5.2 模型檢查122
5.2.1 Büchi自動機123
5.2.2 從LTL到Büchi自動機*126
5.2.3 嵌套深度優(yōu)先搜索*130
5.2.4 符號重復性檢查132
5.3 活性證明*136
5.3.1 eventuality屬性136
5.3.2 條件response屬性137
參考文獻說明140
第6章 動態(tài)系統(tǒng)142
6.1 連續(xù)時間模型142
6.1.1 連續(xù)變化的輸入和輸出142
6.1.2 擾動模型148
6.1.3 構件構成148
6.1.4 穩(wěn)定性149
6.2 線性系統(tǒng)151
6.2.1 線性度152
6.2.2 線性微分方程的解154
6.2.3 穩(wěn)定性159
6.3 控制器設計161
6.3.1 開環(huán)控制器與反饋控制器162
6.3.2 穩(wěn)定化控制器162
6.3.3 PID控制器*165
6.4 分析技術*170
6.4.1 數(shù)值模擬170
6.4.2 柵欄函數(shù)172
參考文獻說明176
第7章 時間模型177
7.1 時間進程177
7.1.1 基于時間的電燈開關177
7.1.2 有界延遲的緩沖器178
7.1.3 多個時鐘179
7.1.4 形式化模型180
7.1.5 時間進程組合182
7.1.6 不完全時鐘的建模184
7.2 基于時間的協(xié)議184
7.2.1 基于時間的分布式協(xié)調184
7.2.2 音頻控制協(xié)議186
7.2.3 雙腔植入式心臟起搏器190
7.3 時間自動機194
7.3.1 時間自動機的模型194
7.3.2 區(qū)域等價*195
7.3.3 基于矩陣表示的符號分析201
參考文獻說明207
第8章 實時調度208
8.1 調度概念208
8.1.1 調度器架構208
8.1.2 周期作業(yè)模型209
8.1.3 可調度性211
8.1.4 其他的作業(yè)模型215
8.2 EDF調度216
8.2.1 周期作業(yè)模型的EDF217
8.2.2 EDF的最優(yōu)性219
8.2.3 基于利用率的可調度性測試220
8.3 固定優(yōu)先級調度223
8.3.1 單調截止期策略和單調速率策略223
8.3.2 單調截止期策略的最優(yōu)性*225
8.3.3 單調速率策略的可調度性測試*229
參考文獻說明234
第9章 混成系統(tǒng)235
9.1 混成動態(tài)模型235
9.1.1 混成進程235
9.1.2 進程組合239
9.1.3 奇諾行為241
9.1.4 穩(wěn)定性243
9.2 混成系統(tǒng)設計244
9.2.1 自動駕駛車輛244
9.2.2 多機器人協(xié)調的障礙規(guī)避246
9.2.3 多跳控制網(wǎng)絡*251
9.3 線性混成自動機*256
9.3.1 追趕游戲例子256
9.3.2 形式化模型258
9.3.3 符號可達性分析260
參考文獻說明266
參考文獻267
索引274
書單推薦
