MA建模的概率混成自动机转换方法研究
2019-02-25张福高曹雪岳
张福高，曹雪岳
(南京航空航天大学 计算机科学与技术学院，江苏 南京 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是变迁的边集合。其中具体的集合元素形如
(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模型转换成了概率混成自动机模型，为后续的形式化分析与验证工作奠定了基础。
