卜星晨，曹子寧，胡名光

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

0 引 言

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

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

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

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

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

為了明確概率行為附件的使用方法，采用EBNF(Extended Backus Naur Form)范式來(lái)定義概率行為附件的語(yǔ)法。在EBNF中，關(guān)鍵字通過粗體字表現(xiàn)出來(lái)，可替換元素通過“|”進(jìn)行分隔，同一組元素用“()”包圍，可選擇的部分通過“[]”進(jìn)行覆蓋，“{}+”和“{}*”分別表示所包含集合中的一個(gè)或多個(gè)元素和零個(gè)或多個(gè)元素。概率行為附件語(yǔ)言主要由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)行聲明，用來(lái)刻畫該組件在某一時(shí)刻的性質(zhì)。變量的語(yǔ)法定義如下所示：

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)前組件處在同一個(gè)包下，或者使用關(guān)鍵字with，將另一個(gè)包的數(shù)據(jù)組件導(dǎo)入到當(dāng)前的組件范圍內(nèi)。

1.2 states模塊

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

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)系，一個(gè)狀態(tài)如果滿足相應(yīng)的條件將會(huì)跳轉(zhuǎn)到相應(yīng)的后繼狀態(tài)，但跳轉(zhuǎn)到的后繼狀態(tài)具有不確定性。狀態(tài)變遷的語(yǔ)法定義如下所示:

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

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

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

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

guard可以描述兩種不同的狀態(tài)變遷場(chǎng)景，第一種是因?yàn)闋顟B(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為真時(shí)，狀態(tài)發(fā)生遷移。這種情況下發(fā)生的狀態(tài)遷移是一種概率選擇事件，即狀態(tài)變遷時(shí)可能會(huì)有多個(gè)后繼狀態(tài)的選擇，跳轉(zhuǎn)到相應(yīng)狀態(tài)的可能性大小即為對(duì)應(yīng)的概率值。

第二種發(fā)生狀態(tài)變遷的場(chǎng)景是因?yàn)楫?dāng)前狀態(tài)執(zhí)行了發(fā)送或接收動(dòng)作，從而引發(fā)了狀態(tài)上的變遷。執(zhí)行動(dòng)作帶來(lái)的變遷同樣是一種概率選擇事件，從當(dāng)前狀態(tài)跳轉(zhuǎn)到的后繼狀態(tài)可能有多個(gè)，且跳轉(zhuǎn)到相應(yīng)狀態(tài)的可能性大小即為對(duì)應(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á)式主要用來(lái)描述信息系統(tǒng)中發(fā)生狀態(tài)遷移時(shí)的變量謂詞約束。布爾表達(dá)式的語(yǔ)法定義如下：

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

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

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

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

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] )

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

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

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

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

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

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

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

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

對(duì)于AADL中沒有的對(duì)應(yīng)轉(zhuǎn)換元素，采用AADL的內(nèi)置數(shù)據(jù)類型aadlstring對(duì)屬性集進(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對(duì)水箱控制系統(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，控制器對(duì)h進(jìn)行判斷：當(dāng)h下降到100時(shí)，控制系統(tǒng)將會(huì)通過事件數(shù)據(jù)端口cc給水箱發(fā)送開閘放水的控制信號(hào)on，水箱系統(tǒng)接收到控制信號(hào)后，立即打開閥門注水；當(dāng)h上升到150時(shí)，控制系統(tǒng)將會(huì)發(fā)送關(guān)閉進(jìn)水的控制信號(hào)off，整個(gè)系統(tǒng)將會(huì)把h控制在[100,150]的區(qū)間范圍內(nèi)。但因?yàn)榭刂葡到y(tǒng)存在接觸不良或者線路老化等問題，控制系統(tǒng)有20%的可能不能夠順利地對(duì)水箱進(jìn)行控制，出現(xiàn)故障時(shí)，控制系統(tǒng)將會(huì)跳轉(zhuǎn)至錯(cuò)誤模式。

使用AADL對(duì)水箱系統(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對(duì)水箱物理部分建模

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

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

物理系統(tǒng)的流規(guī)范如下所示，表示物理系統(tǒng)發(fā)送數(shù)據(jù)信號(hào)的流延遲為2 ms～3 ms，物理系統(tǒng)接收控制信號(hào)的流延遲為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)對(duì)接收到的數(shù)據(jù)信號(hào)進(jìn)行判斷并將控制信號(hào)發(fā)送給物理系統(tǒng)的流延遲為3 ms～4 ms。

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

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

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

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

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

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

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

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

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

Z語(yǔ)言描述的操作模式如下所示：

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

狀態(tài)inactive：

狀態(tài)low：

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

5 結(jié)束語(yǔ)

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