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

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

of timed automata. Then, a plug-in is implemented in the Ptolemy environment that automatically translated the discrete event model into
a network of timed automata, and verifies the network of timed automata by calling the Uppaal validation kernel. Finally, a case of traffic
light control system is successfully translated and verified, and the experimental results confirm that the proposed approach is reliable and
effective for the verification of Ptolemy discrete event model.
Key words: formal verification; Ptolemy DE model; automatic model translation; timed automata

近些年来,随着计算机技术的发展,物理信息融合系统(cyber-physical system,简称 CPS)已经广泛应用到社
会中的各个领域,发挥着举足轻重的作用.航空、军事、医疗等高可靠领域对系统正确性的要求尤为突出.然而,
在传统的系统开发过程中,通常采用测试的方法验证系统正确性.测试一般是在系统开发结束才执行,发现问题
晚,修改的代价是巨大的.因此,一个有效的设计开发过程必须在早期包含对系统正确性的分析,以确保实现的
系统满足正确性需求.
模型驱动开发的核心思想是分离业务分析与业务实现,将开发人员的关注点转移到业务领域建模上,模型
在开发过程中起到主线的作用.当模型构建完成后,可以对模型进行验证,这样就可以在整个开发过程的早期发
[1]
现问题.Ptolemy 是由加州大学伯克利分校的团队设计、开发的一个研究并发、实时嵌入式系统建模、仿真的
集成环境,其依靠其开源、面向角色以及支持异构等方面的优点,在模型驱动开发过程中,越来越受到业内人员
的广泛关注.Ptolemy 在建模、仿真方面拥有强大的功能,但是缺乏形式化验证,只能通过仿真来检测模型正确性.
然而,这种方法是不完备的,因为对模型进行仿真,仅仅是检测模型中的某条路径,无法对模型进行穷尽搜索,形
[2]
式化验证则可以高效全面地检测模型的正确性 .
[3]
模型检测是一种重要的形式化方法 ,其基本思想是:用状态迁移系统表示系统的行为,用时序逻辑公式描
述系统的性质.这样,“系统是否具有所期望的性质”就转化为数学问题“状态迁移系统是否是公式的一个模型?”.
对有穷状态系统,这个问题是可判定的,即可以用计算机程序在有限时间内自动确定.时间自动机是一种可以指
定时间的模型,并拥有相应的分析与验证工具 Uppaal,而且作为模型检测基础的时序逻辑可以方便地表示离散
事件或状态是否发生以及发生的先后顺序,所以,本文提出了将 Ptolemy 离散事件模型转换为时间自动机模型
进行形式化验证的方法.我们首先定义了 Ptolemy 离散事件模型的语义;其次,设计了一组将离散事件模型转换
为时间自动机的映射规则;然后,在 Ptolemy 环境中实现了一个插件,可以自动将离散事件模型转换为时间自动
机模型,进而通过调用 Uppaal 验证内核进行形式化验证,验证系统的正确性需求.
本文中,我们的主要贡献在于:(1) 定义了更为完整的 Ptolemy 组件映射规则,可以支持更多的组件;(2) 将
Ptolemy 模型中的各个组件转换为时间自动机,在上层组件转换生成的时间自动机和下层组件转换生成的时间
自动机之间设置一个同步通道,用于上下层之间传递信息,保留了模型层次化的特点,有效避免了摊平层次化组
件时可能造成的状态空间爆炸;(3) 避免使用 tick 计时,降低验证的复杂度;(4) 在 Ptolemy 环境中设计实现了一
个自动转换验证的插件,完善了使用 Ptolemy 进行模型驱动开发的工具链.
本文第 1 节介绍 Ptolemy 离散事件模型.第 2 节介绍时间自动机模型.第 3 节是将 Ptolemy 离散事件模型转
换为时间自动机模型的映射规则.第 4 节介绍 Ptolemy 离散事件模型验证框架及其实现.第 5 节是一个具体的案
例分析.第 6 节介绍相关工作.第 7 节是本文的总结与展望.

1 Ptolemy 离散事件模型

Ptolemy 是一个开源的建模和仿真工具,与其他建模工具不同,Ptolemy 支持层次化异构建模.Ptolemy 的一
个关键目标就是将不同领域之间的语法、语义和语用之间的差异最小化,并将不同领域设计之间的互操作性最
大化.

1.1 Ptolemy模型语法
Ptolemy 支持面向组件的层次化建模,如图 1 是一个 Ptolemy 层次化异构模型的示意图.D 1 和 D 2 是指示器
(director),指明 Ptolemy 模型的语义域(semantic domain),不同语义域下,组件之间的交互是不同的,体现了