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

陆芝浩 等:Ptolemy 离散事件模型形式化验证方法 1837

( ) Trans Paras V ∩
( )
( )
( )
Trans _ FSM ⋅≅ _ ( ) Trans _ InputPs I ∩ Trans _OutputPs O ∩ Trans _ RFS R
( [1]) ∩
( [ ])
Trans _ RFS R ≅ ( ) Trans RF R ...∩ Trans _ RF R n
_
( [ ])
Trans _ RF R i ≅ ( [ ]) Trans RFT R i ∪ _ ( [ ]) Trans _ RFF R i
( , , , , ) ∩
( [ ])
Trans _ RFT R i ≅ Edge l g φ r lc Edges ( , ,lc g O !,, )r lc ∩ Edge ( , , ,, )lc g φ r l′
1 2 j 3
Trans _ RFF ( [ ])R i ≅ Edges ( , ,l φ I ?, , )r lu ∩ Edges ( , ,lu φ I ?, , )r lu ∩ Edge ( , , , , )lu g φ φ lg ∩
1 j 2 j 3
Edge 4 ( , , , , )lg g φ r lc ∩ Edge 5 (lg,! , , , )g φ r l ∩ Edges 6 ( ,lc ,g O j !, , )r lc ∩ Edge 7 ( , , , , )lc g φ r l′
有限状态机中的参数、输入接口和输出接口转换成一组变量,有限自动机中的迁移转换成时间自动机中的
迁移,有限时间自动机迁移中的输出接口赋值操作和参数更新操作转换为时间自动机迁移中的 r 操作.若迁移
R[i]的约束条件是“true”,则执行 Trans_RFT(R[i]),其中,l 是 urgent 状态,lc 是 committed 状态.迁移 Edge 1 用于当
满足 depth 时,为输出接口赋值和更新参数;Edge 2 是一组为赋值的输出接口产生同步信号的迁移;Edge 3 使时间
自动机更新到目标状态.注意:当组件的输出接口连接的是仅用于展示结果的组件时,其赋值的输出接口不再产
生同步信号.其他迁移则执行 Trans_RFF(R[i]),其中,lu 是 urgent 状态,lg,lc 是 committed 状态.Edges 1 和 Edges 2
是两组接收同步信号的迁移;Edge 3 用于时间自动机满足 depth 时,更新到判断约束条件是否为真的状态.若约束
条件为真,则执行 Edge 4 为输出接口赋值并更新参数;若约束条件为假,则执行 Edge 5 回到迁移的源状态.Edge 6 是
一组为赋值的输出接口产生同步信号的迁移,Edge 7 使时间自动机更新到目标状态.
3.3.3 模态模型组件
模态模型是层次化的组件,其顶层是 FSM,只是状态可以添加细化模型,从而实现分层.在转换模态模型时
保留下层次化的特点,从而防止了摊平组件时可能造成的状态空间的爆炸:
Trans _ RFT ( [ ])R i ≅ Edge 1 ( , ,l g down !, , )r ld ∩ Edge 2 ( , ,ld φ up ?, , )r lc ∩ Edges 3 ( , ,lc g O j !, , )r lc ∩ Edge 4 ( , , , , )lc g φ r l′
Trans _ RFF ( [ ])R i ≅ Edges 1 ( , ,l φ I j ?, , )r lu ∩ Edges 2 ( , ,lu φ I j ?, , )r lu ∩ Edge 3 ( , ,lu g down !, , )r ld ∩
Edge 4 ( , ,ld φ up ?, , )lrφ ∩ Edge 5 ( , , , , )lr g φ r lc ∩ Edge 6 ( ,! , , ,lr g φ r lro ) ∩
Edges 7 ( , ,lc g O j !, , )r lc ∩ Edge 8 ( , , , , )lc g φ r l′ ∩ Edges 9 (lro , ,g O j !, ,r lro ∩ )
Edge (lro ,! , ,, )g φ r l ∩ Edge (lro , , ,, )g φ r lu
10 11
细化模型有两种,分别是组件形式的细化和模态模型形式的细化:组件形式的细化是指细化模型中可以任
意添加组件,而模态模型形式的细化是指其细化模型中是状态之间的迁移.在模态模型的转换过程中,保留了层
次化的特点,只是在相邻两层之间建立两个同步通道:上层发送同步,使得下层时间自动机触发;下层的各个时
间自动机执行完之后,发送同步,使得上层时间自动机继续执行.
Trans_RFT(R[i]),其中,l 是 urgent 状态,ld 和 lc 是 committed 状态.迁移 Edge 1 用于当满足 depth 时,向下层发
送同步信号;Edge 2 则是接收下层发送的同步信号,同时对输出接口赋值和更新参数;Edges 3 是一组为赋值的输
出接口产生同步信号的迁移;Edge 4 使时间自动机更新到目标状态,若目标状态包含细化模型,则更新到目标状
态的迁移会发送初始化细化模型的广播信号 init!.
Trans_RFF(R[i]),其中,lu 是 urgent 状态,ld,lr,lc 和 lro 是 committed 状态.Edges 1 和 Edges 2 是两组接收同步
信号的迁移;Edge 3 用于时间自动机满足 depth 时,向下层发送同步信号;Edge 4 接收下层发送的同步信号,并更新
到判断约束条件是否为真的状态.若约束条件为真,则执行 Edge 5 为输出接口赋值并更新参数;若约束条件为假,
则执行 Edge 6 更新到准备产生同步信号的状态.Edges 7 和 Edges 9 是两组为赋值的输出接口产生同步信号的迁
移;Edge 8 使时间自动机更新到目标状态;Edge 10 表示当细化模型不可以继续执行时,模态模型本次迭代结束,回
到迁移的源状态;Edge 11 表示细化模型可以继续执行时,时间自动机更新到可以向下层发送同步信号的状态:

( , , g sen r l′ ∩
Trans _ RFSM R i ≅ Edge l φ ( , ,rev ?, , )φ lc ∩ Edge lc !, , )
( [ ])
1 2
Edge lc g sen φ 3 ( ,! , !, , ) l ∩ Edge l φ 4 ( , ,init φ ?, ,linit ∩
)
( [1]) ∩
( [2]) ∩
Trans _ RCOM E ≅ ( ) Trans NActor E Trans _ Actor E ...∩
_
Trans Actor ( [E x − 1]) ∩ Trans _ NActor ( [ ])E x
_