Page 264 - 《软件学报》2021年第6期

1838 Journal of Software 软件学报 Vol.32, No.6, June 2021

( [1]) ≅
Trans _ NActor E Edge l φ 1 ( ,,rev ?, , )φ lc ∩ Edge lc g φ ( , ,,,) l′ ∩ φ
2
( [1]) ∩
( ,! , g sen φ
Trans Actor E Edge lc !, , ) l
_
3
Trans _ NActor E x ≅ ([ ]) Trans Actor E x ∩ _ ( [ ]) Edge lc φ ( , ,sen φ !, , ) li
Trans_RFSM(R[i])表示模态模型形式的细化模型中迁移的转换规则,lc 是 committed 状态,linit 是细化模型
的初始状态.Edge 1 用于接收前一个细化模型发送的同步,若该细化模型是状态下的第 1 个细化模型,则此迁移用
于接收 down?;Edge 2 表示当满足约束条件时,对输出接口赋值并更新参数,同时发送同步信号,若该细化模型是
状态下的最后一个细化模型,则此迁移用于发送 up!;Edge 3 表示当约束条件不满足时,只发送同步信号;Edge 4 表
示接收到初始化细化模型的广播,时间自动机回归到初始状态.
Trans_RCOM(E)表示组件形式的细化模型中迁移的转换规则,细化模型中 depth 最小和最大的组件,需要添
加接收或发送同步信号的迁移,其他组件按组件映射规则转换即可.Trans_NActor(E[1])用于转换 depth 最小的
组件.Edge 1 用于接收前一个细化模型发送的同步,然后立即判断组件需要的模态模型输入接口信息是否满足:
若满足 Edge 2 ,更新到 E[1]对应时间自动机结构的迁移状态,并发送同步信号;若不满足 Edge 3 ,则回到接收同步信
号的状态,并发送同步信号.Trans_NActor(E[x])用于转换细化模型中 depth 最大的组件,当组件对应时间自动机
执行完,最后加一条 Edge 用于发送同步信号.
3.4 一致性保证
基于模型转换的形式化验证方法,保证转换前后模型的一致性是至关重要的.一般情况下,如果两个模型的
[9]
语义保证下列行为是一致的,则说明两个模型是等价的 .(1) 当输入相同时,两个模型有相同的执行路径;(2)
当输入相同时,两个模型对应的参数是相同的.
在 Ptolemy DE 模型中,组件的触发顺序是严格按照事件的时间戳进行的,当两个事件的时间戳一样时,则继
续判断两个组件的优先级:若优先级也一样,则按照加入模型的顺序进行触发.Ptolemy DE 模型中组件的触发总
是满足该原则:向组件 B 提供输入的组件 A 会先执行.
根据第 3.1 节数据类型的映射规则,因为时间自动机中支持 int 和 bool 类型,所以可以直接将 Ptolemy 中 int
和 bool 类型的数据转换为时间自动机中 int 和 bool 类型的数据;为了保证时间自动机必然可以在某一时刻发生
迁移,为其设置了一个时钟变量,并添加位置上的 invariant 和迁移上的 guard 约束;在 Ptolemy 模型中,事件是从
一个组件发送给另一个组件的瞬时消息,即从前一个组件产生输出消息,到后一个组件接收到该消息,并触发组
件是瞬时完成的,逻辑时间没有推进.
根据第 3.2 节关系的映射规则,保证了时间自动机为输出接口参数赋值和后继组件转换生成的时间自动机
为输入接口参数赋值是同时发生的,并且转换而来的时间自动机与组件功能一致,保证了当输入相同时,时间自
动机对参数的更新操作与组件对参数的更新操作是相同的.
根据第 3.3.1 节特定组件的映射规则,将每个组件转换成功能相同的时间自动机,同时,每个时间自动机都
有一个 depth 属性,各个时间自动机的 depth 值不同,时间自动机网络按照 depth 从小到大,判断时间自动机是否
可以执行,保证了时间自动机始终遵循着 Ptolemy 中“向组件 B 提供输入的组件 A 会被先执行”这一原则,从而保
证了当输入相同时,时间自动机的执行顺序和 Ptolemy 中组件的执行顺序是严格一致的.
根据第 3.3.2 节有限状态机的映射规则,将组件接收和发送事件,转换为时间自动机中的接收同步信号和发
送同步信号,有限状态机中的一次状态迁移转换为时间自动机中的一组位置迁移.
第 3.3.3 节指出了层次化模型中,上层组件和下层组件转换生成的时间自动机之间通过交互通道通信,保证
了各层之间信息的传递.
4 Ptolemy DE 模型验证框架及实现

4.1 Ptolemy DE模型验证框架
本文提出将 Ptolemy DE 模型转换为可以在 Uppaal 中进行形式化验证的时间自动机模型,从而进行验证,