基于仿真的可達(dá)集一致性測試

1、基于仿真的可達(dá)集一致性測試2016 SAVE目錄一致性測試問題一致性關(guān)系的選取可達(dá)集一致性測試基于仿真的可達(dá)集計算與驗證案例研究及總結(jié)41235一致性測試問題一致？ 一致性測試問題真實系統(tǒng)抽象模型安全性質(zhì) 驗證 一致 跡一致性關(guān)系 強(qiáng)一致性關(guān)系 保持多種性質(zhì)對于只關(guān)心安全性質(zhì)的非確定混成系統(tǒng)保持了不關(guān)心的性質(zhì)為保證測試覆蓋度，需要采樣系統(tǒng)非確定情況下的跡跡一致性關(guān)系：Traces(Sr) Traces(Sa)可達(dá)集一致性關(guān)系可達(dá)集定義：Reacht(S)=(t)| Traces(S)可達(dá)集一致性關(guān)系：Reacht(Sr) Reacht(Sa) Reacht(Sr) Unsafeset = Re

2、acht(Sa) Unsafeset = 弱一致性關(guān)系 保持安全性質(zhì)兩種一致性關(guān)系可達(dá)集一致性測試方法真實系統(tǒng)的可達(dá)集無法獲取可達(dá)集一致性測試方法抽象模型可達(dá)集過近似計算基于Zonotope靜態(tài)計算效率低基于仿真動態(tài)仿真效率高基于仿真的抽象模型可達(dá)集過近似計算采用有限個半徑為的區(qū)域?qū)Τ跏紖^(qū)域進(jìn)行劃分覆蓋系統(tǒng)初始狀態(tài)集合基于仿真的抽象模型可達(dá)集過近似計算從每一個區(qū)域中心點處進(jìn)行仿真通過誤差控制函數(shù)保證系統(tǒng)行為在一定范圍之內(nèi)基于仿真的抽象模型可達(dá)集過近似計算誤差控制函數(shù)(x,x,t)需滿足對于系統(tǒng)|(t)- (t)| (x,x,t) 給定系統(tǒng)可能行為的上界當(dāng)xx時，(x,x,t) 0 當(dāng)初始系統(tǒng)誤

3、差趨近0時，誤差控制函數(shù)也趨近于0若系統(tǒng)微分方程滿足Lipschitz連續(xù)，且Lipschitz常數(shù)為L，則誤差控制函數(shù)為： (x,x,t) = |x-x|eLt抽象模型性質(zhì)驗證驗證系統(tǒng)安全性質(zhì)：Reachot(Sa) Unsafeset = 系統(tǒng)安全若對于當(dāng)前劃分，Reachot(Sa) Unsafeset 系統(tǒng)不安全若沒有明確結(jié)果則縮小，繼續(xù)進(jìn)行計算案例研究系統(tǒng)安全性質(zhì)在運行過程中不能超過頂棚限速及EBD曲線收到緊急制動命令后立即進(jìn)行緊急制動操作，并在目標(biāo)位置前停車案例研究列車按照允許速度進(jìn)行牽引運行，在一定時間后收到緊急制動命令，進(jìn)行緊急制動結(jié)果分析紅色十字為真實系統(tǒng)輸出藍(lán)色區(qū)域為抽象模型可達(dá)集過近似灰色線條為仿真真實系統(tǒng)輸出耗時：2分10秒（基于仿真） 10小時+（基于zonotope）總結(jié)使用基于仿真的方法計算了抽象模型可達(dá)集過近似，并通過過近似驗證了抽象模型滿足安全性質(zhì)，相比基于zonotope計算而言效率通過可達(dá)集一致性測試方法判