發(fā)布時(shí)間：2017-12-09 09:37

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

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

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

本文編號(hào)：1269944