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

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

其整体框架如图 3 所示.验证 Ptolemy DE 模型分为转换模型和形式化验证两部分.
• 在模型的自动转换阶段,将 Ptolemy DE 模型和根据模型提取的属性验证公式作为输入,首先对 Ptolemy
DE 模型进行解析,获得各个组件的结构信息;然后根据定义的映射规则,将各个组件转换为对应的时
间自动机;最终,将时间自动机与属性验证公式共同构成一个可进行验证的时间自动机网络结构;
• 将内存中的时间自动机网络结构输出文件,即可调用 Uppaal 验证引擎进行验证.

翻译模型
映射规则库

形式化验证
Ptolemy DE 解析离散
模型 事件模型 各个组件的 映射 可用于验证的 调用Uppaal
结构信息 时间自动机 验证引擎
网络结构 进行验证
属性验证 各个组件
公式 属性验证 对应的
公式 自动机结构

Fig.3 Framework of verifying Ptolemy DE model
图 3 验证 Ptolemy DE 模型的整体框架
4.2 Ptolemy DE模型验证实现

算法 2 是 Ptolemy DE 模型自动化转换的伪代码,以 Ptolemy DE 模型和属性验证公式为输入/输出一个时间
自动机网络结构.第 4 行获取 Ptolemy DE 模型中的组件.第 5 行~第 8 行将各个组件转换为时间自动机,并保存
到 beans 中.第 6 行 getAByRule(A)是组件转换的核心函数,其过程是:首先,根据组件类型读取模板库中对应的模
板文件;然后,通过获取组件 A 中的参数、接口,生成对应的声明字符串;进而对获取的模板文件中的字符串进行
替换,从而实现根据模板文件生成一个完整的时间自动机.第 9 行表示将各个时间自动机和属性验证公式一起
构成可用于形式化验证的自动机网络结构.

算法 2. Translation of Ptolemy Discrete Event Model.
1: Input: TP model, Formula;
2: Output: Network of automata.
3: bean←∅
4: actorArr←parse(TP model)
5: for each actor A in actorArr do
6: bean←getAByRule(A)
7: bean.add(bean)
8: end for
9: Network←getCode(beans,Formula)
10: return Network

图 4 是调用插件的界面,在 Output Type 中选择输出
可进行形式化验证的时间自动机文件或者直接进行验
证,在 Temporal Formula 中输入属性验证公式,在 Terminal

中返回验证结果.
Fig.4 Interface of verifying Ptolemy DE model
图 4 调用自动化转换插件及验证引擎的界面