MA建模的概率混成自动机转换方法研究

张福高，曹雪岳

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

0 引 言

AADL是一种支持组件系统建模的语言[1]，用来对系统的软、硬件体系结构进行建模，并对系统的功能与非功能性质进行描述，采用单一模型支持多种分析的方式，从系统的需求分析、设计，到系统模型建立、模型验证以及自动代码生成等融合在统一的框架之下[2]。Modelica是一种面向对象语言，可以应用于多领域建模[3-5]。

信息物理系统(CPS)整合了计算进程和物理进程[6]，是将计算(computation)、通信(communication)与控制(control)技术进行有机和深度融合的下一代智能系统。CPS充分调度计算资源与物理资源，合理安排信息物理的融合。CPS追求的是物理世界与计算过程的深度融合，要实现二者间的互相通信与控制，要对CPS进行抽象建模比较困难，文献[7-8]提出了一些集成方法。AADL对于物理细节的建模不如Modelica精确[9]，而在软件部分建模方面，AADL具有丰富的组件来完成建模工作。为了实现信息物理系统的建模，完成软件与硬件的结合，可以使用Modelica为物理系统模块进行建模，信息系统部分交由AADL组件和行为附件来实现。

Modelica与AADL不是完全形式化的建模方式，那么很难对Modelica-AADL模型进行形式化验证与分析工作。依据转换算法进行模型转换，再进行后续的形式化验证与分析是一种很好的策略。文献[10]基于构件交互自动机的AADL模型转换方法，之后依据模型检测算法[11]进行了验证分析工作。

因此，将Modelica-AADL模型转换成适合的形式化模型很有必要，根据信息物理融合系统的特性，转换成概率混成自动机[12]，为后续的验证分析工作奠定基础。

1 概率扩展的Modelica与AADL模型的状态

1.1 Modelica中的状态

由于Modelica中没有直接的状态转换说明，所以需要进行进一步的抽象转换。Modelica建模系统中的运行与转换关系主要根据方程Equation[13]中的定义得出。假设系统的状态集合为Q，系统的当前状态为s0，那么下面给出Modelica中几个重要的Equation下的状态划分规则。

规则1：Equation if pred then alt1 else alt2 Equation 存在某一状态到两个状态之间的迁移。

在当前状态s0下进行条件判断，若满足条件，则执行操作alt1，将之后的状态作为新的状态s1，若不满足条件pred，则执行操作alt2，将之后的状态作为新的状态s2。那么s0与状态s1,s2就存在着一定的迁移关系。

规则2：Equation when pred then op 存在某一状态到另外一个状态间的迁移。

在当前状态s0下进行条件判断，若满足条件pred，则执行操作集合op，这里操作集合op中的操作顺序无关紧要，将之后的状态作为新的状态s1，那么s0与状态s1就存在着一定的迁移关系。

规则3：Equation for _indices loop 存在某一状态间的循环。

在当前状态s0下进行循环，根据_indices的迭代次数确定系统在该状态下的运行，在loop中可以有循环操作。那么状态s0与s0就存在循环的迁移关系。

规则4：Equation connect (component_reference1, component_reference2) 存在某一状态到另外一个状态间的迁移。

在component_reference1下的状态s0可以迁移到component_reference1下的状态s1。在Modelica中connect方程的目的是通过两个连接器将两个对象相连。根据连接关系，找出连接集合中的内连接器与外连接器的对应连接，进行连接融合，建立对应连接器内对应元素变量的方程关系。

1.2 Modelica的概率扩展

物理组件要根据物理事件进行响应，而现实中的物理事件常常伴有随机性。建立随机物理系统的模型就变得很有必要。

对于Modelica的扩展有很多实现[14]，Modelica中的特性有助于将概率因子引入其中。Modelica中的条件集合可以触发系统中的离散改变或者事件的发生。

2 Modelica-AADL建模

2.1 AADL中的状态

AADL行为附件是AADL标准核心库的扩展，提供了描述组件局部功能行为的说明方式。它支持精确描述行为，例如端口通信，计算，时间等等。行为附件中具有系统迁移状态的描述。

2.2 Modelica与AADL接口设计

对于接口的定义，AADL与Modelica模块之间具有一定的对应关系。根据对应关系，可以在Modelica中创建一个AADL工具库AADLUnit，也可以在AADL中定义一个ModelicaPackage，实现部分，可以利用如xml等形式完成相关参数值的注入。

在需要利用接口的时候，为了在具体的AADL模型中可以描述Modelica中的方程、常量等一些组件变量、参数的关系与值传递，需要对AADL引入附加的属性。

同样Modelica支持多领域统一建模[15]，利用Modelica中的扩展connector组件连接操作，完成参数变量的传递，将AADL与Modelica接口之间的变量关系以Modelica的形式描述出来。

2.3 Modelica-AADL模型中的状态

以AADL状态作为基础，对Modelica-AADL模型做出如下规定。

(1)Modelica模型与AADL行为模型中的状态可以转化为Modelica-AADL模型中的一般状态；

(2)Modelica模型中状态的概率迁移可以转换为Modelica-AADL模型中状态的概率迁移；

(3)Modelica模型中的传输就绪状态与AADL行为附件中的状态通过接口进行关键参数传递时，可以转换成Modelica-AADL实例状态；

(4)Modelica-AADL实例状态与AADL中的状态依然具有迁移关系，因Modelica-AADL实例状态的一部分属于AADL状态，原先的迁移关系可以得到保留。

3 Modelica-AADL模型向概率混成自动机的转换

3.1 概率混成自动机

信息物理融合系统(CPS)是物理连续变化与离散计算系统相融合的系统架构，对于它的建模，混成自动机是一种比较理想的模型，状态上发生连续的变换，而离散的变化发生在状态转换之间。为了进一步描述CPS中的随机成分，将混成自动机扩展，引入概率因子，概率混成自动机(PHA)的定义如下：

定义：概率混成自动机可以描述为元组H=(L,X,Σ,E,P,F,I)，其中

(1)L表示有限状态集合；

(2)X为变量有限集，可以划分连续变量CV与一般变量GV，即变量X=CV∪GV；

(3)∑=∑t∪∑i∪∑o表示传输动作，输入动作，输出动作的集合；

(4)E⊆L×Σ×L是变迁的边集合。其中具体的集合元素形如，包含了保卫条件g，同步动作a，变量的更新关系u∈X×X，u包含了必须更新的变量，以及变迁前后保持不变的变量；

(5)P是概率函数，L×Σ×L→[0,1]，满足对于任意l∈L,有∑P(l,α,l')=1,(l,α,l')∈E；

(6)F函数为状态l∈L赋予一个流条件，F函数限制了变量的变化率，通常用变量对时间的一阶导数方程表示；

(7)I函数为状态l∈L赋予一个不变式条件，变量需要满足不变式条件。

3.2 Modelica-AADL模型转换

下面具体描述Modelica-AADL模型(MA模型)向PHA的转换规则。

(1)Modelica-AADL模型中的状态是系统的执行状态，把它转换到PHA中的状态集合L;对于Modelica-AADL模型中三种类型的状态sM|-，sM|sA，-|sA，统一转换成为PHA中的状态，构成状态集合L。

(2)Modelica-AADL模型中的变量，传输与端口转换成PHA中的量集合X与动作集合Σ。

(3)根据Modelica-AADL模型中的sM|sA状态传输的关键变量的物理连续变换率转换成为PHA中连续变量变化率F。

(4)概率混成自动机中的不变条件I根据具体的系统状态限制进行转换。

假设根据之前的描述，已经构建了Modelica-AADL模型的概率状态迁移ST={S,→,s0},从-|sA类型的初始状态s0开始，下面给出模型转换算法的伪代码。

Function G_PHA(PHA,ST={S,→,s0})

s, v, a，s=s0

While next(s)!=null do

after_s=next(s)

If prob(s,after_s)<1 then

s=BFS(S,→,s) continue

End

v=getData(after_s)

a=getEvent(s,after_s)

L=L∪(after_s),X=X∪v,∑=∑∪a

E=E∪{(s,a,after_s)},P(s,after_s)=1

End

Return PHA(L,X,Σ,E,P,F)

Function BFS(S,→,root)

Q, Visited, s, tail, v, a

Visited=Visited∪root Enque(Q,root)

Whileempty(Q)==false do

s=Deque(Q) after_s=next(s)

Ifafter_s=null then continue

End

While after_s!=null do

v=getData(after_s)

a=getEvent(s,after_s)

Ifafter_s∉Visitedthen

L=L∪(after_s),E=E∪{(s,a,after_s)},P(s,after_s)=prob(s,after_s)

Visited=Visited∪after_s

Enque(Q,after_s)

after_s=next(s)

Else

E=E∪{(s,a,after_s)},P(s,after_s)=prob(s,after_s)

F(v,after_s)=getEquation(v,after_s)

tail=after_s

End

X=X∪v,∑=∑∪a,

End

End

Return tail

next(s)函数返回s的下一个状态的状态列表的第一个状态(因为概率转移的存在，s的下一个状态可能会有多个)。next函数内置一个指针再次调用next将返回状态列表的后一个状态，直到状态列表遍历完毕，指针重置指向第一个位置。

prob(s1,s2)函数返回状态之间的迁移概率，不涉及概率的状态迁移，将概率看作1。

getEquation(s)函数返回sM|sA类型状态s中传递的关键连续物理变量的变化函数。

getData(s)函数返回状态中的变量并将其归类到CV与GV，包括CV包含modelica物理连续变量，GV包含AADL行为状态的数据端口以及状态变量。

getEvent(s1,s2)返回状态间的动作并将其归类到∑i，∑o和∑t，∑i,∑o包括了AADL行为状态的事件端口，∑t包括了Modelica_AADL接口的传输动作。

4 结束语

信息物理融合系统的建模与验证是一项复杂且十分困难的工作。Modelica与AADL是两种优秀的建模语言，对于CPS的建模工作交由这两种建模方式组合处理是一个可取的策略。将物理系统的建模工作交给Modelica处理，将信息计算系统的建模工作交给AADL处理，这种混合建模方式可以充分利用二者的优势。Modelica与AADL相结合的重点就是如何建立它们的联系，文中完成了Modelica-AADL接口的设计，向Modelica中添加了概率扩展用以描述物理系统中的随机性，抽象出了Modelica模型中原来并不存在的状态，进而结合AADL行为附件的系统状态，定义了Modelica-AADL模型中的系统状态。之后制定了相关规则，将Modelica-AADL模型转换成了概率混成自动机模型，为后续的形式化分析与验证工作奠定了基础。