贊譽
譯者序
推薦序
致謝
第1章　信息物理系統(tǒng)概述1
　1.1　引言1
　　1.1.1　舉例分析信息物理系統(tǒng)1
　　1.1.2　應(yīng)用領(lǐng)域2
　　1.1.3　意義2
　　1.1.4　安全的重要性3
　1.2　混成系統(tǒng)與信息物理系統(tǒng)4
　1.3　多動態(tài)系統(tǒng)5
　1.4　如何學習信息物理系統(tǒng)6
　1.5　信息物理系統(tǒng)的計算思維7
　1.6　學習目標8
　1.7　本書的結(jié)構(gòu)9
　1.8　總結(jié)12
　參考文獻12
部分　初等信息物理系統(tǒng)
第2章　微分方程與域18
　2.1　引言18
　2.2　作為連續(xù)物理過程模型的微分方程18
　2.3　微分方程的含義20
　2.4　微分方程示例的簡短綱要21
　2.5　微分方程的域26
　2.6　連續(xù)程序的語法27
　　2.6.1　連續(xù)程序28
　　2.6.2　項28
　　2.6.3　一階公式29
　2.7　連續(xù)程序的語義30
　　2.7.1　項30
　　2.7.2　一階公式31
　　2.7.3　連續(xù)程序34
　2.8　總結(jié)35
　2.9　附錄35
　　2.9.1　存在性定理35
　　2.9.2　性定理36
　　2.9.3　常系數(shù)線性微分方程37
　　2.9.4　延拓與連續(xù)依賴38
　習題39
　參考文獻41
第3章　選擇與控制42
　3.1　引言42
　3.2　混成程序的逐步介紹43
　　3.2.1　混成程序的離散變化43
　　3.2.2　混成程序的合成44
　　3.2.3　混成程序中的決策45
　　3.2.4　混成程序中的選擇45
　　3.2.5　混成程序中的測試47
　　3.2.6　混成程序中的重復48
　3.3　混成程序50
　　3.3.1　混成程序的語法50
　　3.3.2　混成程序的語義51
　3.4　混成程序設(shè)計54
　　3.4.1　制動還是不制動，這是個問題54
　　3.4.2　選擇的問題55
　3.5　總結(jié)56
　3.6　附錄：機器人彎道運動建模56
　習題58
　參考文獻61
第4章　安全性與契約63
　4.1　引言63
　4.2　CPS契約的逐步介紹64
　　4.2.1　彈跳球Quantum歷險記64
　　4.2.2　Quantum如何在時間結(jié)構(gòu)中發(fā)現(xiàn)裂縫67
　　4.2.3　Quantum怎樣學會放氣68
　　4.2.4　CPS的后置條件契約69
　　4.2.5　CPS的前置條件契約70
　4.3　混成程序的邏輯公式71
　4.4　微分動態(tài)邏輯73
　　4.4.1　微分動態(tài)邏輯的語法73
　　4.4.2　微分動態(tài)邏輯的語義75
　4.5　邏輯形式的CPS契約77
　4.6　查明CPS的需求78
　4.7　總結(jié)82
　4.8　附錄82
　　4.8.1　順序合成證明的中間條件82
　　4.8.2　選擇的證明84
　　4.8.3　測試的證明85
　習題86
　參考文獻90
第5章　動態(tài)系統(tǒng)與動態(tài)公理92
　5.1　引言92
　5.2　CPS的中間條件93
　5.3　動態(tài)系統(tǒng)的動態(tài)公理95
　　5.3.1　非確定性選擇的動態(tài)公理95
　　5.3.2　公理的可靠性97
　　5.3.3　賦值的動態(tài)公理98
　　5.3.4　微分方程的動態(tài)公理99
　　5.3.5　測試的動態(tài)公理101
　　5.3.6　順序合成的動態(tài)公理102
　　5.3.7　循環(huán)的動態(tài)公理104
　　5.3.8　尖括號模態(tài)的公理105
　5.4　短暫彈跳球的證明105
　5.5　總結(jié)107
　5.6　附錄108
　　5.6.1　模態(tài)肯定前件在方括號模態(tài)中的蘊涵108
　　5.6.2　如果沒有任何相關(guān)變化，則為空虛狀態(tài)變化109
　　5.6.3　哥德爾將永真性泛化到方括號模態(tài)中109
　　5.6.4　后置條件的單調(diào)性110
　　5.6.5　自由變量和約束變量111
　　5.6.6　自由變量和約束變量分析111
　習題113
　參考文獻116
第6章　真理與證明118
　6.1　引言118
　6.2　真理和證明119
　　6.2.1　相繼式120
　　6.2.2　證明122
　　6.2.3　命題證明規(guī)則122
　　6.2.4　證明規(guī)則的可靠性126
　　6.2.5　動態(tài)的證明127
　　6.2.6　量詞證明規(guī)則129
　6.3　派生證明規(guī)則131
　6.4　單跳彈跳球的相繼式證明132
　6.5　實算術(shù)證明規(guī)則133
　　6.5.1　實數(shù)量詞消除法134
　　6.5.2　實例化實算術(shù)量詞136
　　6.5.3　通過去除假設(shè)來弱化實算術(shù)137
　　6.5.4　相繼式演算中的結(jié)構(gòu)證明規(guī)則138
　　6.5.5　在公式中代入等式139
　　6.5.6　縮寫項以降低復雜性139
　　6.5.7　創(chuàng)造性地切割實算術(shù)轉(zhuǎn)化問題140
　6.6　總結(jié)140
　習題141
　參考文獻143
第7章　控制回路與不變式145
　7.1　引言145
　7.2　控制循環(huán)146
　7.3　循環(huán)回路147
　　7.3.1　循環(huán)的歸納公理147
　　7.3.2　循環(huán)的歸納規(guī)則149
　　7.3.3　循環(huán)不變式150
　　7.3.4　上下文可靠性需求153
　7.4　一個歡快重復的彈跳球的證明154
　7.5　將后置條件拆分為單獨的情況158
　7.6　總結(jié)159
　7.7　附錄159
　　7.7.1　證明的循環(huán)159
　　7.7.2　打破證明循環(huán)161
　　7.7.3　循環(huán)的不變式證明163
　　7.7.4　歸納公理的替代形式163
　習題165
　參考文獻166