带有数据约束的信息物理融合系统的建模方法

卜星晨，曹子宁，胡名光

(南京航空航天大学 计算机科学与技术学院，江苏 南京 211106)

0 引 言

信息物理融合系统(cyber-physical system，CPS)[1]是一种集成的动态系统，系统同时具有离散动态性的计算单元和连续动态性的物理系统。CPS将物理系统的连续变化引入到计算单元的离散状态变迁中，物理系统中变量的演变可以触发计算单元中的离散事件，而计算单元中的离散事件也可以改变物理系统中变量的变化模式，这种系统间的相互关联性极大地增加了对CPS建模与验证的难度。现有的技术还不能够直接对CPS进行建模来检查系统的一致性和连续动态性。

因此，需要一种新的建模方法——能够同时刻画系统的离散性和连续性。现有的建模语言中，AADL[2-3]作为嵌入式系统的建模语言，不仅能够对系统的体系结构进行详细刻画，还能够支持属性集和行为附件的扩展。文献[4]扩展了不确定附件对系统中的不确定性进行建模，文献[5]提出了混成附件对混成系统的连续行为进行建模。而Modelica[6-8]作为面向对象的物理系统的建模语言，能够利用微分(代数)方程对物理系统的连续性进行详细刻画。采用AADL对信息系统建模，采用Modelica对物理系统进行建模，然后再将所建立的模型通过连接机制连接起来，能够充分刻画CPS的连续性和离散性。该方法是一种基于模型的体系系统[9-10]的建模方法，体系系统中每个子系统都可以独立运行，子系统需要与别的子系统进行相应的交互，来满足指定的系统需求[11]。文献[12]通过定义Modelica-AADL的接口将两者结合起来，使得物理系统和计算过程相融合。文献[13]根据Modelica与AADL的映射关系，将AADL模型转换为Modelica模型。Z规范为软件系统的规格说明提供了一套严密的数学描述方法，主要用来对软件系统的需求、功能、规格等进行正确的描述和验证。文献[14-15]采用Z规范对系统中产生的数据及状态变迁进行数据约束。

文中使用AADL、Modelica分别对CPS中的信息系统和物理系统进行建模。针对AADL无法描述状态间的概率行为事件，提出了带有通信机制的概率行为附件。Modelica语言利用微分方程对物理系统的连续动态性进行建模。根据AADL与Modelica的对应关系，对AADL的属性集进行相应的扩展，将Modelica建立的模型转换为AADL组件，使得信息系统模型可以和物理系统模型进行组合，并使用Osate对CPS中的延迟时间进行分析。在AADL-Modelica建模的基础上，采用Z规范对系统交互过程中产生的数据进行形式化的约束。

1 AADL扩展的概率行为附件

CPS与人们的日常生活紧密联系，然而在现实中很多系统都不是精确无误的，或多或少地存在一些不确定的影响因素。针对现有AADL还不能够对信息系统中的概率行为进行建模的问题，本节通过定义附件子语言的方式提出了一个轻量级的拓展语言——概率行为附件。

为了明确概率行为附件的使用方法，采用EBNF(Extended Backus Naur Form)范式来定义概率行为附件的语法。在EBNF中，关键字通过粗体字表现出来，可替换元素通过“|”进行分隔，同一组元素用“()”包围，可选择的部分通过“[]”进行覆盖，“{}+”和“{}*”分别表示所包含集合中的一个或多个元素和零个或多个元素。概率行为附件语言主要由variables、states和transition三大模块组成。

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

1.1 variables模块

概率行为附件内的变量及其数据类型在variables模块内进行声明，用来刻画该组件在某一时刻的性质。变量的语法定义如下所示：

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

数据类型由分类器进行引用并指派给适当的AADL数据组件。引用的外部数据组件必须与当前组件处在同一个包下，或者使用关键字with，将另一个包的数据组件导入到当前的组件范围内。

1.2 states模块

states模块用来定义系统中出现的状态集合和系统的初始状态。状态的声明包括初始状态声明和状态集合声明。状态的语法定义如下所示：

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

1.3 transition模块

transition模块定义状态间的变迁关系，一个状态如果满足相应的条件将会跳转到相应的后继状态，但跳转到的后继状态具有不确定性。状态变迁的语法定义如下所示:

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

其中guard表示状态发生变迁所要满足的条件，prob表示当前状态跳转到下一个状态的概率约束，prob的取值范围在[0,1]之间，所有可能跳转到的后继状态的prob值相加为1。状态变迁表示如果当前状态满足相应的条件，将在所有的后续状态中以一定的概率挑选一个状态进行跳转，同时执行相应的动作[action]。

guard条件可以是当前状态内变量的布尔表达式，也可以是当前状态执行的输入或输出动作。guard的语法定义如下：

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

guard可以描述两种不同的状态变迁场景，第一种是因为状态内变量的值满足谓词条件约束，从而引发状态上的变迁。信息系统中连续变量的值都是通过数据传输端口从物理系统中获得，所以guard中的data_expression由data_communication和bool_expression作与运算(and)得到，data_communication表示从相应的数据端口接收数据，当接收到的数据值使得变量的谓词条件约束Bool_expression为真时，状态发生迁移。这种情况下发生的状态迁移是一种概率选择事件，即状态变迁时可能会有多个后继状态的选择，跳转到相应状态的可能性大小即为对应的概率值。

第二种发生状态变迁的场景是因为当前状态执行了发送或接收动作，从而引发了状态上的变迁。执行动作带来的变迁同样是一种概率选择事件，从当前状态跳转到的后继状态可能有多个，且跳转到相应状态的可能性大小即为对应的概率值。

布尔表达式(Boolean_expression)由布尔表达式通过二元运算符与(and)、或(or)和一元运算符非(not)组合而成。比较关系由数学表达式结合了标准的比较运算符(= ,<,>,<=,>=,!=)组合而成。布尔表达式主要用来描述信息系统中发生状态迁移时的变量谓词约束。布尔表达式的语法定义如下：

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

状态变迁时可以给跳转到的后继状态指定相应的执行动作action，action动作主要用于对状态中的变量进行重赋值。action的语法定义如下：

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

1.4 信息系统中的交互建模

信息系统不仅与物理系统有着广泛的交互，还与其余的信息系统有着密切的联系。因此对信息系统与其余系统之间的通信行为进行准确建模是对信息系统进行建模的重要组成部分。AADL组件的通信依赖于组件类型声明中的端口。对于数据信号的传输，使用数据端口(data port)进行建模；对于控制信号的传输，采用数据事件端口(event data port)进行建模。相互通信的端口在互补方向上是成对出现的。端口和端口通信的语法定义如下：

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

(? | !)分别表示从端口输入/输出信号，信息系统的数据端口主要用来接收物理系统中的变量值，所以信息系统中的数据端口只有接收动作。而信息系统不仅可以发送控制信号给物理系统，还可以与别的信息系统进行控制信号上的交互，所以信息系统中的控制端口可以执行输入/输出动作。

2 Modelica向AADL的转化

CPS中的物理系统具有连续变化的行为特性，使用Modelica可以很方便地利用数学方程对物理系统中的连续变化进行建模，通过将所建立的模型编译成方程组，对方程组进行求解可以得到系统的仿真结果。

2.1 Modelica与AADL的对应关系

Modelica是一种面向对象的建模语言，主要构成元素是类和对象。AADL中的组件可以分为类型声明和实现两个部分，一个组件类型声明可以拥有多个组件实现。AADL中的组件类型和组件实现与Modelica中的类和对象一一对应。同时AADL与Modelica都支持继承机制，这为两种建模语言的相互转换奠定了基础。

Modelica主要用来对物理系统进行建模，而物理系统相当于计算机系统中的硬件设备，因此将Modelica中的类转换为AADL中的设备(device)类型声明，实例化后的对象转化为设备对应的实现；在Modelica中数据信息的交互主要是通过connector来实现，而AADL中的feature可以用来描述组件之间的数据和事件的交互端口，同时能够刻画数据/事件的传输方向，这两者可以进行相互转换；Modelica中的变量可以通过AADL中的参数(parameter)表示；Modelica中的函数(function)可以用AADL中的子程序(subprogram)来实现，同时函数中的参数可以用AADL中的参数进行标识；Modelica自身支持的多种不同的数据类型，在AADL中可以使用datatype对各种不同的数据类型进行定义，能够满足相互转化的需求。而Modelica中常用的建模元素常量和方程在AADL中没有相对应的对象，因此通过对AADL的属性集进行扩展引入新的属性和属性类型，使得AADL和Modelica能够相互转换。Modelica模型与AADL模型的对应关系如表1所示。

表1 Modelica模型与AADL模型的对应关系

2.2 AADL扩展的属性集

对于AADL中没有的对应转换元素，采用AADL的内置数据类型aadlstring对属性集进行扩展。扩展的属性集再通过applies to子句添加到硬件组件上。扩展的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 水箱进出水系统的实例

3.1 使用AADL对水箱控制系统建模

本节选择水箱系统进行研究，如图1所示，该系统由控制器、水箱和进出水管道组成。其中，控制器相当于信息系统，而水箱及进出水管道相当于物理系统，两者通过端口紧密联系。

图1 水箱进出水系统

控制器通过数据接收端口wl接收物理系统发送的水位值h，控制器对h进行判断：当h下降到100时，控制系统将会通过事件数据端口cc给水箱发送开闸放水的控制信号on，水箱系统接收到控制信号后，立即打开阀门注水；当h上升到150时，控制系统将会发送关闭进水的控制信号off，整个系统将会把h控制在[100,150]的区间范围内。但因为控制系统存在接触不良或者线路老化等问题，控制系统有20%的可能不能够顺利地对水箱进行控制，出现故障时，控制系统将会跳转至错误模式。

使用AADL对水箱系统中的控制系统进行建模，如下所示：

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对水箱系统中的物理部分进行建模，如下所示：

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模型的转化

根据对应关系，可以将Modelica模型转化为扩展了属性集的AADL组件。转化后的模型如下所示：

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 系统的组合

将物理系统转化后的AADL组件与控制系统的AADL模型进行组合，系统内的AADL组件连接如图2所示。

图2 系统内部的组件连接图

水箱系统对应的体系结构模型如下所示：

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 系统的流延迟分析

3.5.1 添加系统的流规范

在系统的AADL体系结构模型上，可以通过给每个AADL组件添加属性，利用现有的AADL模型分析工具Osate对系统的体系结构进行流延迟分析、资源分配分析、实时调度分析和安全性分析。

本节对系统的流延迟进行了分析：检测从水箱的水位值达到阈值后到接收到控制系统的控制信号并改变运行状态所要花费的时间。为了验证系统的流延迟，需要为控制系统和物理系统的AADL模型分别添加流规范，每个流规范都被赋予了一个延迟值。

物理系统的流规范如下所示，表示物理系统发送数据信号的流延迟为2 ms～3 ms，物理系统接收控制信号的流延迟为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;};

信息系统的流规范如下所示，表示信息系统对接收到的数据信号进行判断并将控制信号发送给物理系统的流延迟为3 ms～4 ms。

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

水箱控制系统对进水闸进行操作的完整路径，是从源组件watertank再到watertank的数据信号的流动，在上一小节wholeSystem系统中说明了这种流动。此外，模型wholeSystem还为该过程定义了一个12 ms的延迟。该数据可以从系统的要求中获取。

3.5.2 系统的流分析

利用流延迟分析工具Osate，检测水箱内水位值达到阈值后能否在规定时间内操作水闸。图3说明了此次流分析的运行结果。水位值到达阈值之后打开注水开关的操作总延迟时间区间为7 ms～10 ms，小于系统要求的12 ms。

图3 顶层的端对端流分析结果

4 Modelica、AADL上的数据约束

CPS中的信息系统与物理系统在交互的过程中将会产生大量的数据，为了能够更好地对交互过程及状态变迁中的变量进行形式化的约束，在AADL-Modelica建模的基础上，采用Z语言对模型中的状态及状态变迁进行形式化的描述。

Z语言中主要有两种模式：状态模式和操作模式，分别表示状态空间和在状态空间上进行的操作。使用Z语言描述状态空间如下所示：

水平线上是对变量的声明，x1,…,xn表示状态中所包含的所有变量，变量的取值表示当前所处的状态；S1,…,Sn表示变量x1,…,xn的取值范围；水平线下是对变量的谓词声明，相当于变量的限制条件且这些限制条件必须为真，同时这些限制条件在相应的操作模式下也必须为真。

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

CPS是由物理系统和信息系统组合而成的系统，其本身是一个状态变迁系统。本节将对上述的水箱系统进行形式化的说明。水箱信息系统中的状态inactive、状态low以及从状态inactive跳转到状态low的Z语言描述如下：

状态inactive：

状态low：

状态inactive到状态low的状态迁移：

5 结束语

对CPS的建模与验证是一个复杂的问题，文中基于模型的体系结构建模方法，将CPS中的信息系统和物理系统分开建模。使用AADL对信息系统进行建模，使用Modelica对物理系统进行建模。针对信息系统中的概率行为事件，提出了轻量级的拓展语言——概率行为附件；根据Modelica与AADL的对应关系，对AADL拓展相应的属性集，使得Modelica模型转化为相应的AADL组件成为可能。将Modelica模型转换后的AADL组件与信息系统的AADL模型组合形成一个完整的系统模型。利用模型分析工具Osate，可以对系统的整体架构、流延迟以及可调用性进行分析。最后再在AADL-Modelica建模的基础上，使用Z规范对CPS中产生的大量数据进行形式化的数据约束。采用AADL与Modelica相结合的方法对CPS进行建模是一个可取的方法，该研究也为系统后续的形式化分析与验证打下了基础。