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