帶有數(shù)據(jù)約束的信息物理融合系統(tǒng)的建模方法

卜星晨，曹子寧，胡名光

(南京航空航天大學(xué) 計算機(jī)科學(xué)與技術(shù)學(xué)院，江蘇 南京 211106)

0 引 言

信息物理融合系統(tǒng)(cyber-physical system，CPS)[1]是一種集成的動態(tài)系統(tǒng)，系統(tǒng)同時具有離散動態(tài)性的計算單元和連續(xù)動態(tài)性的物理系統(tǒng)。CPS將物理系統(tǒng)的連續(xù)變化引入到計算單元的離散狀態(tài)變遷中，物理系統(tǒng)中變量的演變可以觸發(fā)計算單元中的離散事件，而計算單元中的離散事件也可以改變物理系統(tǒng)中變量的變化模式，這種系統(tǒng)間的相互關(guān)聯(lián)性極大地增加了對CPS建模與驗證的難度。現(xiàn)有的技術(shù)還不能夠直接對CPS進(jìn)行建模來檢查系統(tǒng)的一致性和連續(xù)動態(tài)性。

因此，需要一種新的建模方法——能夠同時刻畫系統(tǒng)的離散性和連續(xù)性。現(xiàn)有的建模語言中，AADL[2-3]作為嵌入式系統(tǒng)的建模語言，不僅能夠?qū)ο到y(tǒng)的體系結(jié)構(gòu)進(jìn)行詳細(xì)刻畫，還能夠支持屬性集和行為附件的擴(kuò)展。文獻(xiàn)[4]擴(kuò)展了不確定附件對系統(tǒng)中的不確定性進(jìn)行建模，文獻(xiàn)[5]提出了混成附件對混成系統(tǒng)的連續(xù)行為進(jìn)行建模。而Modelica[6-8]作為面向?qū)ο蟮奈锢硐到y(tǒng)的建模語言，能夠利用微分(代數(shù))方程對物理系統(tǒng)的連續(xù)性進(jìn)行詳細(xì)刻畫。采用AADL對信息系統(tǒng)建模，采用Modelica對物理系統(tǒng)進(jìn)行建模，然后再將所建立的模型通過連接機(jī)制連接起來，能夠充分刻畫CPS的連續(xù)性和離散性。該方法是一種基于模型的體系系統(tǒng)[9-10]的建模方法，體系系統(tǒng)中每個子系統(tǒng)都可以獨(dú)立運(yùn)行，子系統(tǒng)需要與別的子系統(tǒng)進(jìn)行相應(yīng)的交互，來滿足指定的系統(tǒng)需求[11]。文獻(xiàn)[12]通過定義Modelica-AADL的接口將兩者結(jié)合起來，使得物理系統(tǒng)和計算過程相融合。文獻(xiàn)[13]根據(jù)Modelica與AADL的映射關(guān)系，將AADL模型轉(zhuǎn)換為Modelica模型。Z規(guī)范為軟件系統(tǒng)的規(guī)格說明提供了一套嚴(yán)密的數(shù)學(xué)描述方法，主要用來對軟件系統(tǒng)的需求、功能、規(guī)格等進(jìn)行正確的描述和驗證。文獻(xiàn)[14-15]采用Z規(guī)范對系統(tǒng)中產(chǎn)生的數(shù)據(jù)及狀態(tài)變遷進(jìn)行數(shù)據(jù)約束。

文中使用AADL、Modelica分別對CPS中的信息系統(tǒng)和物理系統(tǒng)進(jìn)行建模。針對AADL無法描述狀態(tài)間的概率行為事件，提出了帶有通信機(jī)制的概率行為附件。Modelica語言利用微分方程對物理系統(tǒng)的連續(xù)動態(tài)性進(jìn)行建模。根據(jù)AADL與Modelica的對應(yīng)關(guān)系，對AADL的屬性集進(jìn)行相應(yīng)的擴(kuò)展，將Modelica建立的模型轉(zhuǎn)換為AADL組件，使得信息系統(tǒng)模型可以和物理系統(tǒng)模型進(jìn)行組合，并使用Osate對CPS中的延遲時間進(jìn)行分析。在AADL-Modelica建模的基礎(chǔ)上，采用Z規(guī)范對系統(tǒng)交互過程中產(chǎn)生的數(shù)據(jù)進(jìn)行形式化的約束。

1 AADL擴(kuò)展的概率行為附件

CPS與人們的日常生活緊密聯(lián)系，然而在現(xiàn)實(shí)中很多系統(tǒng)都不是精確無誤的，或多或少地存在一些不確定的影響因素。針對現(xiàn)有AADL還不能夠?qū)π畔⑾到y(tǒng)中的概率行為進(jìn)行建模的問題，本節(jié)通過定義附件子語言的方式提出了一個輕量級的拓展語言——概率行為附件。

為了明確概率行為附件的使用方法，采用EBNF(Extended Backus Naur Form)范式來定義概率行為附件的語法。在EBNF中，關(guān)鍵字通過粗體字表現(xiàn)出來，可替換元素通過“|”進(jìn)行分隔，同一組元素用“()”包圍，可選擇的部分通過“[]”進(jìn)行覆蓋，“{}+”和“{}*”分別表示所包含集合中的一個或多個元素和零個或多個元素。概率行為附件語言主要由variables、states和transition三大模塊組成。

Probability Annex::={**variables {variables_declaration}+states {states_declaration}+transition {transition_declaration}+**}

1.1 variables模塊

概率行為附件內(nèi)的變量及其數(shù)據(jù)類型在variables模塊內(nèi)進(jìn)行聲明，用來刻畫該組件在某一時刻的性質(zhì)。變量的語法定義如下所示：

Variables_declaration::=variable_identifier {,variable_iden-tifier }* : data_componet_classifier_reference

數(shù)據(jù)類型由分類器進(jìn)行引用并指派給適當(dāng)?shù)腁ADL數(shù)據(jù)組件。引用的外部數(shù)據(jù)組件必須與當(dāng)前組件處在同一個包下，或者使用關(guān)鍵字with，將另一個包的數(shù)據(jù)組件導(dǎo)入到當(dāng)前的組件范圍內(nèi)。

1.2 states模塊

states模塊用來定義系統(tǒng)中出現(xiàn)的狀態(tài)集合和系統(tǒng)的初始狀態(tài)。狀態(tài)的聲明包括初始狀態(tài)聲明和狀態(tài)集合聲明。狀態(tài)的語法定義如下所示：

States_declaration::=initial_state_declaration,states_declara-tioninitial_state_declaration::=Initial_state_identifier: initial state;states_declaration::={state_ identifier}+:states;

1.3 transition模塊

transition模塊定義狀態(tài)間的變遷關(guān)系，一個狀態(tài)如果滿足相應(yīng)的條件將會跳轉(zhuǎn)到相應(yīng)的后繼狀態(tài)，但跳轉(zhuǎn)到的后繼狀態(tài)具有不確定性。狀態(tài)變遷的語法定義如下所示:

transition_declaration:: state-[guard]->prob:state[ac-tion] { + prob:state[action]} *

其中g(shù)uard表示狀態(tài)發(fā)生變遷所要滿足的條件，prob表示當(dāng)前狀態(tài)跳轉(zhuǎn)到下一個狀態(tài)的概率約束，prob的取值范圍在[0,1]之間，所有可能跳轉(zhuǎn)到的后繼狀態(tài)的prob值相加為1。狀態(tài)變遷表示如果當(dāng)前狀態(tài)滿足相應(yīng)的條件，將在所有的后續(xù)狀態(tài)中以一定的概率挑選一個狀態(tài)進(jìn)行跳轉(zhuǎn)，同時執(zhí)行相應(yīng)的動作[action]。

guard條件可以是當(dāng)前狀態(tài)內(nèi)變量的布爾表達(dá)式，也可以是當(dāng)前狀態(tài)執(zhí)行的輸入或輸出動作。guard的語法定義如下：

guard::=data_expression | control_communicationdata_expression::=data_communication and bool_expression

guard可以描述兩種不同的狀態(tài)變遷場景，第一種是因為狀態(tài)內(nèi)變量的值滿足謂詞條件約束，從而引發(fā)狀態(tài)上的變遷。信息系統(tǒng)中連續(xù)變量的值都是通過數(shù)據(jù)傳輸端口從物理系統(tǒng)中獲得，所以guard中的data_expression由data_communication和bool_expression作與運(yùn)算(and)得到，data_communication表示從相應(yīng)的數(shù)據(jù)端口接收數(shù)據(jù)，當(dāng)接收到的數(shù)據(jù)值使得變量的謂詞條件約束Bool_expression為真時，狀態(tài)發(fā)生遷移。這種情況下發(fā)生的狀態(tài)遷移是一種概率選擇事件，即狀態(tài)變遷時可能會有多個后繼狀態(tài)的選擇，跳轉(zhuǎn)到相應(yīng)狀態(tài)的可能性大小即為對應(yīng)的概率值。

第二種發(fā)生狀態(tài)變遷的場景是因為當(dāng)前狀態(tài)執(zhí)行了發(fā)送或接收動作，從而引發(fā)了狀態(tài)上的變遷。執(zhí)行動作帶來的變遷同樣是一種概率選擇事件，從當(dāng)前狀態(tài)跳轉(zhuǎn)到的后繼狀態(tài)可能有多個，且跳轉(zhuǎn)到相應(yīng)狀態(tài)的可能性大小即為對應(yīng)的概率值。

布爾表達(dá)式(Boolean_expression)由布爾表達(dá)式通過二元運(yùn)算符與(and)、或(or)和一元運(yùn)算符非(not)組合而成。比較關(guān)系由數(shù)學(xué)表達(dá)式結(jié)合了標(biāo)準(zhǔn)的比較運(yùn)算符(= ,<,>,<=,>=,!=)組合而成。布爾表達(dá)式主要用來描述信息系統(tǒng)中發(fā)生狀態(tài)遷移時的變量謂詞約束。布爾表達(dá)式的語法定義如下：

Boolean_expression::=ture | false | Boolean_expression | Boolean_expression { and Boolean_expression} + | Boolean_expression { or Boolean_expression} + | not Boolean_expres-sion | comparisonComparsion ::= [numberic_expression comparison_symobol numberic_expression]Comparsion_symbol ::= = | < | > | <= | >= | !=Numberic_expression ::= numberic_term | numberic_term - numberic_term | numberic_term / numberic_term | numberic_term mod numberic_term | numberic_term + numberic_term | numberic_term * numberic_termNumberic_term ::= [-] (numberic_literal | variable_identi-fier)numeric_literal ::= integer_literal | real_literal

狀態(tài)變遷時可以給跳轉(zhuǎn)到的后繼狀態(tài)指定相應(yīng)的執(zhí)行動作action，action動作主要用于對狀態(tài)中的變量進(jìn)行重賦值。action的語法定義如下：

Action::=action {,action} *Action::=assignmentAssignment::=variable_identifier= (integer_number | real_number| boolean)

1.4 信息系統(tǒng)中的交互建模

信息系統(tǒng)不僅與物理系統(tǒng)有著廣泛的交互，還與其余的信息系統(tǒng)有著密切的聯(lián)系。因此對信息系統(tǒng)與其余系統(tǒng)之間的通信行為進(jìn)行準(zhǔn)確建模是對信息系統(tǒng)進(jìn)行建模的重要組成部分。AADL組件的通信依賴于組件類型聲明中的端口。對于數(shù)據(jù)信號的傳輸，使用數(shù)據(jù)端口(data port)進(jìn)行建模；對于控制信號的傳輸，采用數(shù)據(jù)事件端口(event data port)進(jìn)行建模。相互通信的端口在互補(bǔ)方向上是成對出現(xiàn)的。端口和端口通信的語法定義如下：

Event_port::=event_port_identifier {, event_port_identi-fier}* : data_componet_classifier_referenceData_port::=data_port_identifier {, data_port_identifi-er}* : data_componet_classifier_referenceData_communication::=data_port_identifier? ( [variable_identifier] )Control_communication::=event_port_identifier(?|!)([variable_identifier] )

(? | !)分別表示從端口輸入/輸出信號，信息系統(tǒng)的數(shù)據(jù)端口主要用來接收物理系統(tǒng)中的變量值，所以信息系統(tǒng)中的數(shù)據(jù)端口只有接收動作。而信息系統(tǒng)不僅可以發(fā)送控制信號給物理系統(tǒng)，還可以與別的信息系統(tǒng)進(jìn)行控制信號上的交互，所以信息系統(tǒng)中的控制端口可以執(zhí)行輸入/輸出動作。

2 Modelica向AADL的轉(zhuǎn)化

CPS中的物理系統(tǒng)具有連續(xù)變化的行為特性，使用Modelica可以很方便地利用數(shù)學(xué)方程對物理系統(tǒng)中的連續(xù)變化進(jìn)行建模，通過將所建立的模型編譯成方程組，對方程組進(jìn)行求解可以得到系統(tǒng)的仿真結(jié)果。

2.1 Modelica與AADL的對應(yīng)關(guān)系

Modelica是一種面向?qū)ο蟮慕ＵZ言，主要構(gòu)成元素是類和對象。AADL中的組件可以分為類型聲明和實(shí)現(xiàn)兩個部分，一個組件類型聲明可以擁有多個組件實(shí)現(xiàn)。AADL中的組件類型和組件實(shí)現(xiàn)與Modelica中的類和對象一一對應(yīng)。同時AADL與Modelica都支持繼承機(jī)制，這為兩種建模語言的相互轉(zhuǎn)換奠定了基礎(chǔ)。

Modelica主要用來對物理系統(tǒng)進(jìn)行建模，而物理系統(tǒng)相當(dāng)于計算機(jī)系統(tǒng)中的硬件設(shè)備，因此將Modelica中的類轉(zhuǎn)換為AADL中的設(shè)備(device)類型聲明，實(shí)例化后的對象轉(zhuǎn)化為設(shè)備對應(yīng)的實(shí)現(xiàn)；在Modelica中數(shù)據(jù)信息的交互主要是通過connector來實(shí)現(xiàn)，而AADL中的feature可以用來描述組件之間的數(shù)據(jù)和事件的交互端口，同時能夠刻畫數(shù)據(jù)/事件的傳輸方向，這兩者可以進(jìn)行相互轉(zhuǎn)換；Modelica中的變量可以通過AADL中的參數(shù)(parameter)表示；Modelica中的函數(shù)(function)可以用AADL中的子程序(subprogram)來實(shí)現(xiàn)，同時函數(shù)中的參數(shù)可以用AADL中的參數(shù)進(jìn)行標(biāo)識；Modelica自身支持的多種不同的數(shù)據(jù)類型，在AADL中可以使用datatype對各種不同的數(shù)據(jù)類型進(jìn)行定義，能夠滿足相互轉(zhuǎn)化的需求。而Modelica中常用的建模元素常量和方程在AADL中沒有相對應(yīng)的對象，因此通過對AADL的屬性集進(jìn)行擴(kuò)展引入新的屬性和屬性類型，使得AADL和Modelica能夠相互轉(zhuǎn)換。Modelica模型與AADL模型的對應(yīng)關(guān)系如表1所示。

表1 Modelica模型與AADL模型的對應(yīng)關(guān)系

2.2 AADL擴(kuò)展的屬性集

對于AADL中沒有的對應(yīng)轉(zhuǎn)換元素，采用AADL的內(nèi)置數(shù)據(jù)類型aadlstring對屬性集進(jìn)行擴(kuò)展。擴(kuò)展的屬性集再通過applies to子句添加到硬件組件上。擴(kuò)展的AADL屬性集合如下所示：

property set Modelica_property isVariables:aadlstring applies to (device);InitialVariable:aadlstring applies to (device);ConstantVariables:aadlstring applies to (device);ConstantValues:aadlstring applies to (device);Equation:aadlstring applies to (device);end Modelica_property;

3 水箱進(jìn)出水系統(tǒng)的實(shí)例

3.1 使用AADL對水箱控制系統(tǒng)建模

本節(jié)選擇水箱系統(tǒng)進(jìn)行研究，如圖1所示，該系統(tǒng)由控制器、水箱和進(jìn)出水管道組成。其中，控制器相當(dāng)于信息系統(tǒng)，而水箱及進(jìn)出水管道相當(dāng)于物理系統(tǒng)，兩者通過端口緊密聯(lián)系。

圖1 水箱進(jìn)出水系統(tǒng)

控制器通過數(shù)據(jù)接收端口wl接收物理系統(tǒng)發(fā)送的水位值h，控制器對h進(jìn)行判斷：當(dāng)h下降到100時，控制系統(tǒng)將會通過事件數(shù)據(jù)端口cc給水箱發(fā)送開閘放水的控制信號on，水箱系統(tǒng)接收到控制信號后，立即打開閥門注水；當(dāng)h上升到150時，控制系統(tǒng)將會發(fā)送關(guān)閉進(jìn)水的控制信號off，整個系統(tǒng)將會把h控制在[100,150]的區(qū)間范圍內(nèi)。但因為控制系統(tǒng)存在接觸不良或者線路老化等問題，控制系統(tǒng)有20%的可能不能夠順利地對水箱進(jìn)行控制，出現(xiàn)故障時，控制系統(tǒng)將會跳轉(zhuǎn)至錯誤模式。

使用AADL對水箱系統(tǒng)中的控制系統(tǒng)進(jìn)行建模，如下所示：

process controller features cc:out event data port; wl:in data port;end controller;process implementation controller.impl annex Probability_behavior {** variables v:WLCS::ValveStatus h:WLCS::WaterLevel states: inactive:initial state; low,high,inflow,error: states; transitions: inactive - [wl?(h) & h=100] -> 0.8:low{v = on} + 0.2:error; low - [cc!(v)] -> inflow; inflow-[[wl?(h) & h= 150]] -> 0.8:high{v = off} + 0.2:error; high - [cc!(v)] -> inactive; **};end controller.impl;

3.2 使用Modelica對水箱物理部分建模

使用Modelica對水箱系統(tǒng)中的物理部分進(jìn)行建模，如下所示：

model watertank import Modelica.Blocks.Interfaces.BooleanInput; import Modelica.Blocks.Interfaces.RealOutput; BooleanInput cc=true; RealOutput wl; Real h=150; parameter Real Qin=0.07; parameter Real g=9.8; parameter Real pi=3.14; parameter Real r=0.025 4; equation when cc==true then h=Qin-pi*r*r*1.414*g; end when; when cc==false then h=-pi*r*r*1.414*g; end when;end watertank;

3.3 Modelica模型向AADL模型的轉(zhuǎn)化

根據(jù)對應(yīng)關(guān)系，可以將Modelica模型轉(zhuǎn)化為擴(kuò)展了屬性集的AADL組件。轉(zhuǎn)化后的模型如下所示：

package watertankpublicwith Modelica_property;device watertankfeatures cc :in event data port; wl :out data port;properties modelica_property::Variables =>"h"; modelica_property::InitialVariables =>"150"; modelica_property::ConstantVariables =>"Qin,g,pi,r"; modelica_property::ConstantValues =>"0.07,9.8,3.14,0.025 4"; modelica_property::Equation => "whencc == true then h = Qin - pi * r * r * 1.414 * g; end when; whencc == false then h = -pi * r * r * 1.414 * g; end when;";end watertank;end watertank;

3.4 系統(tǒng)的組合

將物理系統(tǒng)轉(zhuǎn)化后的AADL組件與控制系統(tǒng)的AADL模型進(jìn)行組合，系統(tǒng)內(nèi)的AADL組件連接如圖2所示。

圖2 系統(tǒng)內(nèi)部的組件連接圖

水箱系統(tǒng)對應(yīng)的體系結(jié)構(gòu)模型如下所示：

system wholeSystemend wholeSystem;system implementation wholeSystem.Impl subcomponents waterTank:device watertank::watertank.impl; Controller:process controller::controller.impl;connections conn1:port waterTank.wl -> Controller.wl; conn2:port controller.cc -> waterTank.cc; flows on_end_to_end:end to end flow waterTank.on_flow_src -> conn1 ->Controller.on_flow_path ->conn2 ->waterTank.on_flow_sink {latency => 12 ms.. 12 ms;};end wholeSystem.Impl;

3.5 系統(tǒng)的流延遲分析

3.5.1 添加系統(tǒng)的流規(guī)范

在系統(tǒng)的AADL體系結(jié)構(gòu)模型上，可以通過給每個AADL組件添加屬性，利用現(xiàn)有的AADL模型分析工具Osate對系統(tǒng)的體系結(jié)構(gòu)進(jìn)行流延遲分析、資源分配分析、實(shí)時調(diào)度分析和安全性分析。

本節(jié)對系統(tǒng)的流延遲進(jìn)行了分析：檢測從水箱的水位值達(dá)到閾值后到接收到控制系統(tǒng)的控制信號并改變運(yùn)行狀態(tài)所要花費(fèi)的時間。為了驗證系統(tǒng)的流延遲，需要為控制系統(tǒng)和物理系統(tǒng)的AADL模型分別添加流規(guī)范，每個流規(guī)范都被賦予了一個延遲值。

物理系統(tǒng)的流規(guī)范如下所示，表示物理系統(tǒng)發(fā)送數(shù)據(jù)信號的流延遲為2 ms～3 ms，物理系統(tǒng)接收控制信號的流延遲為2 ms～3 ms。

on_flow_src:flow source wl{latency => 2 ms .. 3 ms;};on_flow_sink:flow sink cc{latency => 2 ms .. 3 ms;};

信息系統(tǒng)的流規(guī)范如下所示，表示信息系統(tǒng)對接收到的數(shù)據(jù)信號進(jìn)行判斷并將控制信號發(fā)送給物理系統(tǒng)的流延遲為3 ms～4 ms。

on_flow_path: flow path wl -> cc {latency => 3 ms .. 4 ms;};

水箱控制系統(tǒng)對進(jìn)水閘進(jìn)行操作的完整路徑，是從源組件watertank再到watertank的數(shù)據(jù)信號的流動，在上一小節(jié)wholeSystem系統(tǒng)中說明了這種流動。此外，模型wholeSystem還為該過程定義了一個12 ms的延遲。該數(shù)據(jù)可以從系統(tǒng)的要求中獲取。

3.5.2 系統(tǒng)的流分析

利用流延遲分析工具Osate，檢測水箱內(nèi)水位值達(dá)到閾值后能否在規(guī)定時間內(nèi)操作水閘。圖3說明了此次流分析的運(yùn)行結(jié)果。水位值到達(dá)閾值之后打開注水開關(guān)的操作總延遲時間區(qū)間為7 ms～10 ms，小于系統(tǒng)要求的12 ms。

圖3 頂層的端對端流分析結(jié)果

4 Modelica、AADL上的數(shù)據(jù)約束

CPS中的信息系統(tǒng)與物理系統(tǒng)在交互的過程中將會產(chǎn)生大量的數(shù)據(jù)，為了能夠更好地對交互過程及狀態(tài)變遷中的變量進(jìn)行形式化的約束，在AADL-Modelica建模的基礎(chǔ)上，采用Z語言對模型中的狀態(tài)及狀態(tài)變遷進(jìn)行形式化的描述。

Z語言中主要有兩種模式：狀態(tài)模式和操作模式，分別表示狀態(tài)空間和在狀態(tài)空間上進(jìn)行的操作。使用Z語言描述狀態(tài)空間如下所示：

水平線上是對變量的聲明，x1,…,xn表示狀態(tài)中所包含的所有變量，變量的取值表示當(dāng)前所處的狀態(tài)；S1,…,Sn表示變量x1,…,xn的取值范圍；水平線下是對變量的謂詞聲明，相當(dāng)于變量的限制條件且這些限制條件必須為真，同時這些限制條件在相應(yīng)的操作模式下也必須為真。

Z語言描述的操作模式如下所示：

CPS是由物理系統(tǒng)和信息系統(tǒng)組合而成的系統(tǒng)，其本身是一個狀態(tài)變遷系統(tǒng)。本節(jié)將對上述的水箱系統(tǒng)進(jìn)行形式化的說明。水箱信息系統(tǒng)中的狀態(tài)inactive、狀態(tài)low以及從狀態(tài)inactive跳轉(zhuǎn)到狀態(tài)low的Z語言描述如下：

狀態(tài)inactive：

狀態(tài)low：

狀態(tài)inactive到狀態(tài)low的狀態(tài)遷移：

5 結(jié)束語

對CPS的建模與驗證是一個復(fù)雜的問題，文中基于模型的體系結(jié)構(gòu)建模方法，將CPS中的信息系統(tǒng)和物理系統(tǒng)分開建模。使用AADL對信息系統(tǒng)進(jìn)行建模，使用Modelica對物理系統(tǒng)進(jìn)行建模。針對信息系統(tǒng)中的概率行為事件，提出了輕量級的拓展語言——概率行為附件；根據(jù)Modelica與AADL的對應(yīng)關(guān)系，對AADL拓展相應(yīng)的屬性集，使得Modelica模型轉(zhuǎn)化為相應(yīng)的AADL組件成為可能。將Modelica模型轉(zhuǎn)換后的AADL組件與信息系統(tǒng)的AADL模型組合形成一個完整的系統(tǒng)模型。利用模型分析工具Osate，可以對系統(tǒng)的整體架構(gòu)、流延遲以及可調(diào)用性進(jìn)行分析。最后再在AADL-Modelica建模的基礎(chǔ)上，使用Z規(guī)范對CPS中產(chǎn)生的大量數(shù)據(jù)進(jìn)行形式化的數(shù)據(jù)約束。采用AADL與Modelica相結(jié)合的方法對CPS進(jìn)行建模是一個可取的方法，該研究也為系統(tǒng)后續(xù)的形式化分析與驗證打下了基礎(chǔ)。