本文關(guān)鍵詞：基于時鐘約束和信號約束的信息物理融合系統(tǒng)的建模、分析與驗證

  更多相關(guān)文章： 信息物理融合系統(tǒng) 時鐘約束 信號約束 模型檢查 形式化驗證 調(diào)度分析

【摘要】：信息物理融合系統(tǒng)(Cyber-Physical Systems, CPS)是一種通過融合計算、通信和控制與物理過程實現(xiàn)計算機世界與物理世界深度協(xié)作的復雜系統(tǒng)。相較于一般傳統(tǒng)系統(tǒng),信息物理融合系統(tǒng)具有以下突出特性：信息世界與物理世界的高度耦合、異構(gòu)性、并發(fā)性、時間攸關(guān)性,以及要求較高的可預(yù)測性和安全性。這些特性帶來了以下挑戰(zhàn)：需要整合異構(gòu)的計算通信模型,需要異構(gòu)的時間模型以及時間模型與行為語義的融合,需要以分析、驗證等手段保證系統(tǒng)具有較高的可預(yù)測性和安全性。本文提供針對這三大挑戰(zhàn),為信息物理融合系統(tǒng)提供建模、驗證和調(diào)度性分析的支持,主要工作包括：·提出了針對信息物理融合系統(tǒng)特性的聲明式建模語言-信號約束語言Signal Con-straint Modeling Language (SCML),以及使用SCML的建模方法。SCML的時間模型是異構(gòu)的,包括邏輯時間和超稠密時間,支持邏輯時間、連續(xù)物理時間和離散物理時間的整合。在異構(gòu)時間模型基礎(chǔ)上,SCML提供多樣的信號支持異構(gòu)的行為的描述,包括連續(xù)動態(tài)行為、離散動態(tài)行為、實時行為和(非實時)邏輯行為。SCML還提供豐富的信號約束用于描述信號之間的關(guān)系,包括不同類型信號之間的交互和轉(zhuǎn)換,并支持多種計算通信規(guī)則。SCML具有操作語義,在計算通信模型理論的基礎(chǔ)上實現(xiàn)異構(gòu)計算通信模型的整合以及異構(gòu)時間與行為的融合。本文提出將SCML作為伴隨約束語言與SysML并PUML-MARTE協(xié)作建模的方法,建模所得的SCML規(guī)約將為模型提供顯式的形式化的行為語義,從而支持后續(xù)的形式化分析和驗證�！ぬ岢隽藢Ｋ玫腟CML規(guī)約進行調(diào)度分析的方法。為提高系統(tǒng)的可預(yù)測性和安全性,定義了要檢查的屬性,包括可采納調(diào)度的條件、定性的調(diào)度分類和調(diào)度時間不敏感性、定量的調(diào)度衡量標準(例如調(diào)度成功率、錯失率和平均響應(yīng)時間)等,并識別出了這些屬性在SCML規(guī)約的語境下的表現(xiàn)形式以及檢查所需的信息。為表達以上內(nèi)容,擴展了時鐘約束語言Clock Constraint Specification Language(CCSL),引入了對時鐘終結(jié)和物理時間的支持,得到了擴展的時鐘約束語言eCCSL,并為eCCSL提供了基于狀態(tài)的操作語義。給出了從SCML規(guī)約中提取檢查屬性所需信息的方法,并將其構(gòu)成了eCCSL規(guī)約。根據(jù)eCCSL的語義,提供了使用模型檢查器SPIN, NuSMV和UPPAAL檢查eCCSL規(guī)約的以上屬性的方法。為識別eCCSL規(guī)約的可采納調(diào)度,定義了基于遷移的廣義Buchi自動機及其語境下的可采納調(diào)度的識別條件,給出了識別可采納調(diào)度的算法。該算法還可以約簡規(guī)約的狀態(tài)空間,約簡后的自動機的所有運行都能產(chǎn)生可采納調(diào)度。分析了規(guī)約規(guī)定的時鐘時刻的依賴關(guān)系,提供了算法探查導致規(guī)約調(diào)度失敗的選擇,當有其他選擇時規(guī)避引發(fā)調(diào)度失敗的選擇�！ぬ岢隽藢Ｋ玫腟CML規(guī)約進行形式化驗證的方法。定義了針對系統(tǒng)可預(yù)測性和安全性進行驗證要檢查的屬性,包括安全性和活性等通用屬性、系統(tǒng)業(yè)務(wù)邏輯相關(guān)屬性等,并識別出了這些屬性在SCML規(guī)約的語境下的表現(xiàn)形式以及檢查所需的信息。采用與調(diào)度分析時類似的方法,從SCML規(guī)約中提取所需信息、并將其構(gòu)成eCCSL規(guī)約。將構(gòu)建的eCCSL規(guī)約轉(zhuǎn)換為了Promela模型和UPPAAL時間自動機,定義了用時序邏輯LTL和TCTL表達待檢查屬性,提供了觀察者模版收集所需信息,利用模型檢查器SPIN和UPPAAL實施了驗證。為證明驗證方法的正確性,定義了帶檢測點的標號遷移系統(tǒng)、基于動作和檢測點的線性時態(tài)邏輯和基于檢測點的互模擬關(guān)系,以此為基礎(chǔ)給出了正確性的證明。本文將提出的方法應(yīng)用于軌道交通領(lǐng)域,以智能交通控制系統(tǒng)在道口問題上的應(yīng)用為案例,表明了提出的方法和過程的可行性與有效性。
【學位授予單位】：華東師范大學
【學位級別】：博士
【學位授予年份】：2016
【分類號】：TP202
，

本文編號：1269944