本文關(guān)鍵詞：基于PAT工具的智能家居平臺(tái)形式化分析與檢驗(yàn)，由筆耕文化傳播整理發(fā)布。

【摘要】：形式化方法是建立在嚴(yán)密數(shù)學(xué)邏輯基礎(chǔ)上的系統(tǒng)研究方法,其嚴(yán)謹(jǐn)、精確的特性適合發(fā)現(xiàn)系統(tǒng)設(shè)計(jì)與開發(fā)過程中并發(fā)性、安全性等方面的問題。PAT(Process Analysis Toolkit)平臺(tái)是功能較為全面、易于使用的形式化建模與自動(dòng)檢驗(yàn)工具,已成功對(duì)特定的智能家居復(fù)合行為進(jìn)行建模和驗(yàn)證,發(fā)現(xiàn)和改善了智能家居系統(tǒng)中的潛在錯(cuò)誤和不足,但還未形成智能家居系統(tǒng)形式化驗(yàn)證的描述和驗(yàn)證一般模型。智能家居平臺(tái)是指將智能設(shè)備、控制程序、操作系統(tǒng)等復(fù)合成為用戶提供服務(wù)的綜合系統(tǒng),其設(shè)備異構(gòu)性與安全重要性對(duì)平臺(tái)的運(yùn)行正確性、安全性等提出了嚴(yán)苛的要求,如何高效檢測運(yùn)行規(guī)則異常和安全缺陷也成為亟待解決的問題。針對(duì)以上問題,本文提出一種描述智能家居平臺(tái)的形式化模型,通過對(duì)平臺(tái)整體及各模塊的形式化建模,用PAT工具對(duì)系統(tǒng)的功能和相關(guān)特性進(jìn)行驗(yàn)證,發(fā)現(xiàn)潛在的異常與沖突,為改進(jìn)系統(tǒng)提供依據(jù)。實(shí)驗(yàn)表明該模型能夠有效地對(duì)智能家居平臺(tái)進(jìn)行特性模擬,并結(jié)合PAT平臺(tái)對(duì)系統(tǒng)進(jìn)行檢驗(yàn)。本文主要內(nèi)容包括以下幾個(gè)部分:分析智能家居平臺(tái)構(gòu)成中的各組成部分(控制程序、設(shè)備控制框架、通用數(shù)據(jù)庫、智能設(shè)備),明確其功能和結(jié)構(gòu)特性以及通信控制方法,提出智能家居平臺(tái)架構(gòu)模型;結(jié)合實(shí)際應(yīng)用中平臺(tái)所應(yīng)具備的性質(zhì),確定系統(tǒng)需求。給出智能家居平臺(tái)模型的形式化定義,實(shí)現(xiàn)對(duì)智能家居平臺(tái)的模型描述,包括平臺(tái)各模塊及其并行通信的模型描述。結(jié)合應(yīng)用場景對(duì)系統(tǒng)需求進(jìn)行說明,明確智能家居平臺(tái)所需檢驗(yàn)的相關(guān)特性,并使用形式化語言對(duì)特性進(jìn)行準(zhǔn)確描述。在PAT平臺(tái)上對(duì)智能家居平臺(tái)模型進(jìn)行形式化檢驗(yàn),實(shí)驗(yàn)包括對(duì)平臺(tái)對(duì)象和平臺(tái)運(yùn)行過程兩方面的檢驗(yàn)與改進(jìn),實(shí)驗(yàn)表明,借助于PAT工具可以高效地對(duì)智能家居平臺(tái)進(jìn)行正確性和實(shí)用性的驗(yàn)證。
【關(guān)鍵詞】：智能家居 架構(gòu)模型 形式化方法 性質(zhì)檢驗(yàn)
【學(xué)位授予單位】：太原理工大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2016
【分類號(hào)】：TP311.52;TU855
【目錄】：

• 摘要3-5
• ABSTRACT5-10
• 第一章 緒論10-16
• 1.1 引言10-11
• 1.2 研究現(xiàn)狀11-14
• 1.3 研究內(nèi)容14-15
• 1.4 論文結(jié)構(gòu)15
• 1.5 本章小結(jié)15-16
• 第二章 相關(guān)背景介紹16-26
• 2.1 物聯(lián)網(wǎng)技術(shù)的應(yīng)用16
• 2.2 智能家居16-18
• 2.3 智能家居平臺(tái)18
• 2.4 智能家居平臺(tái)的檢驗(yàn)方法18-20
• 2.5 形式化方法20-24
• 2.5.1 形式化方法簡述20
• 2.5.2 形式化方法的發(fā)展過程20-21
• 2.5.3 形式化方法的研究內(nèi)容及分類21-22
• 2.5.4 PAT平臺(tái)與CSP#建模語言22-24
• 2.6 本章小結(jié)24-26
• 第三章 智能家居平臺(tái)分析與設(shè)計(jì)26-36
• 3.1 智能家居平臺(tái)需求分析26-29
• 3.1.1 平臺(tái)需求描述26-28
• 3.1.2 核心需求確定與分類28-29
• 3.2 智能家居平臺(tái)組件設(shè)計(jì)29-34
• 3.2.1 控制程序30
• 3.2.2 設(shè)備控制框架30-32
• 3.2.3 通用數(shù)據(jù)庫32-33
• 3.2.4 智能設(shè)備33-34
• 3.3 智能家居平臺(tái)系統(tǒng)架構(gòu)設(shè)計(jì)34-35
• 3.4 本章小結(jié)35-36
• 第四章 形式化定義與建模36-50
• 4.1 形式化定義36-42
• 4.1.1 控制程序模塊36-38
• 4.1.2 設(shè)備控制框架模塊38-40
• 4.1.3 通用數(shù)據(jù)庫模塊40-41
• 4.1.4 設(shè)備模塊41
• 4.1.5 智能家居平臺(tái)形式化定義41-42
• 4.2 形式化建模42-48
• 4.2.1 CSP#建模43-46
• 4.2.2 斷言設(shè)計(jì)46-48
• 4.3 本章小結(jié)48-50
• 第五章 模型實(shí)現(xiàn)與實(shí)驗(yàn)驗(yàn)證50-62
• 5.1 實(shí)驗(yàn)環(huán)境50
• 5.2 模型簡述50-60
• 5.2.1 對(duì)象建模實(shí)驗(yàn)50-56
• 5.2.2 過程建模實(shí)驗(yàn)56-60
• 5.3 結(jié)果分析60-62
• 第六章 總結(jié)與展望62-64
• 6.1 論文總結(jié)與意義62-63
• 6.2 研究展望63-64
• 參考文獻(xiàn)64-68
• 致謝68-70
• 攻讀學(xué)位期間發(fā)表的學(xué)術(shù)論文目錄70

【相似文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前10條

1 廖壯嘉;智能家居的黃金時(shí)代[J];智能建筑與城市信息;2004年02期

2 廖壯嘉;20歲 智能家居的青春年華[J];智能建筑與城市信息;2004年03期

3 ;比爾·蓋茨的智能家居[J];中華建設(shè);2005年05期

4 陳鵬;;智能家居的系統(tǒng)分類和設(shè)計(jì)[J];儀器儀表標(biāo)準(zhǔn)化與計(jì)量;2006年02期

5 王偉光;;走近國外智能化家居[J];數(shù)字社區(qū)&智能家居;2007年02期

6 張鼎盛;;享受生活 享受智能家居[J];建材與裝修情報(bào);2007年05期

7 張鼎盛;;享受生活 享受智能家居[J];建材與裝修情報(bào);2007年07期

8 李磊;林曉杰;;智能家居的標(biāo)準(zhǔn)與協(xié)議[J];數(shù)字社區(qū)&智能家居;2008年01期

9 ;專注、專業(yè)、專心——打造智能家居行業(yè)第一媒體[J];數(shù)字社區(qū)&智能家居;2008年01期

10 戚振興;;淺議我國智能家居發(fā)展[J];廣西輕工業(yè);2009年10期

中國重要會(huì)議論文全文數(shù)據(jù)庫 前10條

1 吳效明;趙錦萌;吳劍波;;智能家居的醫(yī)療監(jiān)測技術(shù)研究[A];中國生物醫(yī)學(xué)工程學(xué)會(huì)成立30周年紀(jì)念大會(huì)暨2010中國生物醫(yī)學(xué)工程學(xué)會(huì)學(xué)術(shù)大會(huì)壁報(bào)展示論文[C];2010年

2 榮蓉;吳文p，

本文編號(hào)：259798