發(fā)布時間：2021-04-09 15:27

　　智能系統(tǒng)是當(dāng)前研究熱點(diǎn),在一些安全攸關(guān)的智能系統(tǒng)中,時間和空間信息需具有一致性,即在規(guī)定的時間到達(dá)規(guī)定的位置。為確保智能系統(tǒng)的時空一致性,需對系統(tǒng)的時間和空間信息進(jìn)行規(guī)約。時鐘通常有物理時鐘和邏輯時鐘兩種類型,將兩者融合在一起形成的混成時鐘（Hybrid Clock）能夠同時對物理時鐘和邏輯時鐘進(jìn)行規(guī)約,其物理時鐘包含了智能系統(tǒng)的空間與時間信息,規(guī)約了時空一致性。本論文構(gòu)建混成時鐘邏輯（Hybrid Clock Logic,HCL）系統(tǒng)對智能系統(tǒng)的時空性質(zhì)進(jìn)行規(guī)約,通過HCL模型檢測驗(yàn)證系統(tǒng)的性質(zhì),保證系統(tǒng)的安全性與可靠性。具體研究內(nèi)容如下:1.建立了混成時鐘邏輯系統(tǒng)的語法結(jié)構(gòu)。為了滿足系統(tǒng)性質(zhì)描述的需要,本文在已有混成時鐘運(yùn)算和關(guān)系的基礎(chǔ)上提出了一些新的運(yùn)算和關(guān)系,定義了HCL的語法,給出了具體的高鐵實(shí)例對混成時鐘運(yùn)算和關(guān)系進(jìn)行解釋,并研究了混成時鐘關(guān)系的相關(guān)性質(zhì)。2.構(gòu)建了混成時鐘邏輯模型檢測方法。首先,通過定義時空一致性規(guī)范語言STeC設(shè)計與HCL公式之間的可滿足關(guān)系,給出了 HCL公式的語義;然后,基于STeC設(shè)計轉(zhuǎn)換成的混成時鐘進(jìn)行模型檢測,設(shè)計了 HCL模型檢測算法;最后,... 

【文章來源】：華東師范大學(xué)上海市 211工程院校 985工程院校 教育部直屬院校

【文章頁數(shù)】：83 頁

【學(xué)位級別】：碩士

【部分圖文】：

高鐵G43運(yùn)行時刻圖

華東師范大學(xué)碩士學(xué)位論文第五章STEC模型檢測工具5.1.2本工具使用Java語言開發(fā)，其開發(fā)和運(yùn)行環(huán)境如表5.1所示。表5.1:程序開發(fā)及運(yùn)行環(huán)境類型相關(guān)軟硬件參數(shù)開發(fā)平臺IntelliJIDEACommunityEdition2018.1.2x64版本開發(fā)語言Java軟件運(yùn)行環(huán)境Windows10，jdk9運(yùn)行硬件條件CPU：Intel(R)Core(TM)i5-2400或以上，主頻在2.10GHz或以上內(nèi)存：1GB以上顯卡：支持DirectX5.1.3能STeC模型檢測工具的用例圖如圖5.1所示，系統(tǒng)的主要參與者為用戶，用例為系統(tǒng)的主要功能，主要包含以下功能：圖5.1:系統(tǒng)用例圖51

華東師范大學(xué)碩士學(xué)位論文第五章STEC模型檢測工具1.提供友好的用戶界面，方便用戶選擇和輸入相應(yīng)參數(shù)；2.根據(jù)打開的不同環(huán)境下的STeC設(shè)計，依據(jù)轉(zhuǎn)換規(guī)則對STeC語句進(jìn)行解析并轉(zhuǎn)換成相應(yīng)的混成時鐘；3.在模型檢測界面，輸入HCL公式，首先對公式的合法性進(jìn)行檢測，若合法則進(jìn)行可滿足性檢測。5.2工具這一小節(jié)將會對工具的軟件架構(gòu)、處理流程以及詳細(xì)設(shè)計進(jìn)行闡述。5.2.1軟件構(gòu)理程本軟件的整體架構(gòu)如圖5.2所示，分為兩個部分：圖5.2:系統(tǒng)架構(gòu)圖52

【參考文獻(xiàn)】：
期刊論文
[1]智能時代的信息物理融合系統(tǒng)[J]. 管曉宏.  網(wǎng)信軍民融合. 2020(01)
[2]形式化驗(yàn)證方法淺析[J]. 陳波,李夫明.  電腦知識與技術(shù). 2019(34)
[3]智能系統(tǒng)在城市道路管理中的應(yīng)用[J]. 朱永森.  科學(xué)技術(shù)創(chuàng)新. 2019(16)
[4]人工智能的歷史、現(xiàn)狀和未來[J]. 譚鐵牛.  智慧中國. 2019(Z1)
[5]信息物理融合系統(tǒng)研究[J]. 李馥娟,王群,錢煥延.  電子技術(shù)應(yīng)用. 2018(09)
[6]電力系統(tǒng)信息物理融合建模與綜合安全評估:驅(qū)動力與研究構(gòu)想[J]. 郭慶來,辛蜀駿,孫宏斌,王劍輝.  中國電機(jī)工程學(xué)報. 2016(06)
[7]工業(yè)4.0和智能制造[J]. 張曙.  機(jī)械設(shè)計與制造工程. 2014(08)
[8]實(shí)時系統(tǒng)規(guī)范語言STeC的Maude重寫系統(tǒng)[J]. 欒天驕,陳儀香,王江濤.  計算機(jī)工程. 2013(10)
[9]基于STeC-Stateflow轉(zhuǎn)換系統(tǒng)的實(shí)時系統(tǒng)仿真與驗(yàn)證方法[J]. 紀(jì)政,李慧勇,陳儀香.  計算機(jī)應(yīng)用研究. 2014(02)
[10]信息-物理融合系統(tǒng)若干關(guān)鍵問題綜述[J]. 李仁發(fā),謝勇,李蕊,李浪.  計算機(jī)研究與發(fā)展. 2012(06)

博士論文
[1]面向同步系統(tǒng)的時鐘約束動態(tài)邏輯系統(tǒng)研究[D]. 張元睿.華東師范大學(xué) 2019
[2]時空邏輯PPTLSL及其應(yīng)用研究[D]. 陸旭.西安電子科技大學(xué) 2017
[3]分布式系統(tǒng)的時間化通信行為模型[D]. 陳艷文.華東師范大學(xué) 2014

碩士論文
[1]信息物理融合系統(tǒng)的時空大數(shù)據(jù)的建模與分析[D]. 朱藝偉.廣東工業(yè)大學(xué) 2019
[2]參數(shù)化時空規(guī)范語言的語義模型及其應(yīng)用[D]. 王士忠.華東師范大學(xué) 2018
[3]基于STeC的空天地一體化地球觀測的驗(yàn)證與仿真[D]. 楊志華.華東師范大學(xué) 2016
[4]基于STeC的時空一致性智能體建模與調(diào)控仿真驗(yàn)證[D]. 紀(jì)政.華東師范大學(xué) 2014
[5]實(shí)時系統(tǒng)規(guī)范語言STeC的Maude語義模型和靜態(tài)分析設(shè)計及其工具實(shí)現(xiàn)[D]. 欒天驕.華東師范大學(xué) 2013



本文編號：3127868