【摘要】：信息物理融合系統(tǒng)CPS是通過計(jì)算、通信與控制技術(shù)有機(jī)和深度的融合實(shí)現(xiàn)計(jì)算資源與物理資源緊密結(jié)合的下一代智能系統(tǒng),體系結(jié)構(gòu)分析與設(shè)計(jì)語言AADL是一種基于構(gòu)件的體系結(jié)構(gòu)建模語言,是嵌入式實(shí)時(shí)系統(tǒng)體系結(jié)構(gòu)描述語言標(biāo)準(zhǔn),廣泛應(yīng)用于航空電子等安全關(guān)鍵領(lǐng)域的系統(tǒng)建模分析。本文基于AADL將形式化建模與驗(yàn)證方法引入CPS的分析與設(shè)計(jì)中,提出了一套面向CPS的模型建立、模型轉(zhuǎn)換及模型驗(yàn)證的完整框架。首先,對(duì)AADL的基本建模元素、建模流程及CPS系統(tǒng)特點(diǎn)、建模需求進(jìn)行研究分析,總結(jié)AADL對(duì)CPS軟硬件體系結(jié)構(gòu)建模的優(yōu)點(diǎn),以及對(duì)CPS中大量數(shù)據(jù)和并發(fā)、不確定關(guān)系缺乏形式化描述的不足,基于形式化規(guī)格說明語言Z和進(jìn)程演算對(duì)AADL進(jìn)行擴(kuò)充,為AADL添加對(duì)變量約束的Z模式和并發(fā)、不確定以及動(dòng)作約束算子的描述,對(duì)數(shù)據(jù)進(jìn)行形式化的描述來對(duì)其進(jìn)行約束,對(duì)動(dòng)態(tài)并發(fā)、不確定的因素進(jìn)行建模,提出一種能夠描述CPS系統(tǒng)行為的體系結(jié)構(gòu)建模規(guī)范CPS-AADL。其次,由于AADL不支持直接的形式化驗(yàn)證,本文在構(gòu)件交互自動(dòng)機(jī)研究的基礎(chǔ)上提出一種帶數(shù)據(jù)約束并支持系統(tǒng)構(gòu)件交互描述的形式化規(guī)范,帶數(shù)據(jù)約束的構(gòu)件交互自動(dòng)機(jī)Z-COIA,同時(shí)給出Z-COIA的組合驗(yàn)證算法,并將CPS-AADL模型轉(zhuǎn)換到Z-COIA形式化規(guī)范,給出了模型轉(zhuǎn)換規(guī)則及其正確性說明。最后,在經(jīng)典時(shí)序邏輯的基礎(chǔ)上提出了面向Z-COIA的時(shí)序邏輯系統(tǒng)CIA-CTL,并給出其具體的語法語義定義和模型檢測(cè)算法,從而實(shí)現(xiàn)了對(duì)CPS-AADL模型檢測(cè)和驗(yàn)證分析,并通過一個(gè)典型的CPS系統(tǒng)——噴氣飛機(jī)的飛行導(dǎo)航系統(tǒng)的模型建立、模型轉(zhuǎn)換以及模型驗(yàn)證的具體過程和對(duì)本文給出的形式化建模與驗(yàn)證的整體框架進(jìn)行分析實(shí)踐,驗(yàn)證了提出的形式化建模方法的可行性和有效性。
[Abstract]:The information physics fusion system (CPS) is the next generation intelligent system which combines the computing resources with the physical resources through the organic and deep fusion of computing, communication and control technology. Architecture Analysis and Design language (AADL) is a component-based architecture modeling language, which is the standard of embedded real-time system architecture description language. It is widely used in avionics and other key areas of system modeling and analysis. Based on AADL, the formal modeling and verification method is introduced into the analysis and design of CPS, and a complete framework of model building, model transformation and model verification for CPS is proposed. First of all, the basic modeling elements of AADL, modeling process and characteristics of CPS system, modeling requirements are analyzed, and the advantages of AADL in modeling CPS hardware and software architecture are summarized, as well as a large amount of data and concurrency in CPS. Due to the lack of formal description of uncertain relations, AADL is extended based on formal specification language Z and process calculus, and the description of Z schema and concurrency, uncertainty and action constraint operators for variable constraints are added to AADL. Data is formally described to constrain it, and dynamic concurrency and uncertainty factors are modeled. An architecture modeling specification CPS-AADL., which can describe the behavior of CPS system, is proposed. Secondly, because AADL does not support direct formal verification, this paper proposes a formal specification with data constraints and supporting component interaction description based on the research of component interactive automata. The component interactive automata Z-COIAA with data constraints is given, and the combination verification algorithm of Z-COIA is given. The CPS-AADL model is converted to the formal specification of Z-COIA, and the rules of model transformation and its correctness are given. Finally, on the basis of the classical temporal logic, a temporal logic system (CIA-CTL,) oriented to Z-COIA is proposed, and its specific syntax and semantic definition and model checking algorithm are given, so that the CPS-AADL model detection and verification analysis are realized. And through a typical CPS system, the model establishment, model transformation and model verification of the jet aircraft flight navigation system, and the analysis and practice of the formal modeling and verification of the overall framework given in this paper. The feasibility and validity of the proposed formal modeling method are verified.
【學(xué)位授予單位】：南京航空航天大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2017
【分類號(hào)】：TP29

【參考文獻(xiàn)】

相關(guān)期刊論文 前10條

1 朱晨曦;張立臣;羅崇偉;;基于AADL的CPS系統(tǒng)分析與設(shè)計(jì)[J];計(jì)算機(jī)應(yīng)用與軟件;2015年08期

2 倪水妹;曹子寧;;面向概率ZIA時(shí)序及度量性質(zhì)的檢測(cè)研究[J];小型微型計(jì)算機(jī)系統(tǒng);2015年03期

3 倪水妹;曹子寧;李心磊;;帶數(shù)據(jù)約束實(shí)時(shí)系統(tǒng)的模型檢測(cè)[J];計(jì)算機(jī)科學(xué);2014年05期

4 苗德成;奚建清;蘇錦鈿;;AADL進(jìn)程子集行為語義研究[J];計(jì)算機(jī)工程與科學(xué);2012年07期

5 溫景容;武穆清;宿景芳;;信息物理融合系統(tǒng)[J];自動(dòng)化學(xué)報(bào);2012年04期

6 黎作鵬;張?zhí)祚Y;張菁;;信息物理融合系統(tǒng)(CPS)研究綜述[J];計(jì)算機(jī)科學(xué);2011年09期

7 賈仰理;張振領(lǐng);李舟軍;;基于自動(dòng)機(jī)的構(gòu)件實(shí)時(shí)交互行為的形式化模型[J];計(jì)算機(jī)科學(xué);2010年09期

8 楊志斌;皮磊;胡凱;顧宗華;馬殿富;;復(fù)雜嵌入式實(shí)時(shí)系統(tǒng)體系結(jié)構(gòu)設(shè)計(jì)與分析語言:AADL[J];軟件學(xué)報(bào);2010年05期

9 任洪敏,錢樂秋;構(gòu)件組裝及其形式化推導(dǎo)研究[J];軟件學(xué)報(bào);2003年06期

10 孫昌愛,金茂忠,劉超;軟件體系結(jié)構(gòu)研究綜述[J];軟件學(xué)報(bào);2002年07期

相關(guān)碩士學(xué)位論文 前5條

1 吳育春;基于AADL的嵌入式軟件形式化驗(yàn)證研究[D];陜西師范大學(xué);2014年

2 朱晨曦;基于AADL的信息物理融合系統(tǒng)的分析與設(shè)計(jì)方法[D];廣東工業(yè)大學(xué);2014年

3 錢宇清;Hybrid AADL：混成系統(tǒng)體系結(jié)構(gòu)分析與設(shè)計(jì)語言[D];華東師范大學(xué);2014年

4 倪水妹;面向混成系統(tǒng)的ZIA形式化模型及其自動(dòng)驗(yàn)證方法研究[D];南京航空航天大學(xué);2014年

5 錢磊;信息物理融合系統(tǒng)的形式化建模與討論[D];華東師范大學(xué);2013年

，

本文編號(hào)：2267938