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

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

现阶段,关于形式化验证 Ptolemy DE 模型的研究工作有两种,都是根据构建好的 Ptolemy DE 模型,生成另
一种可用于形式化验证结构的文件,进而利用相关验证工具实现验证 Ptolemy DE 模型的形式化验证 [23] .
(1) 根据构建的 Ptolemy DE 模型生成可以使用 RED(regional encoding diagram)进行验证的时间自动机结
构.该方法将 Ptolemy DE 模型描述成一个通信时间自动机,通过 RED 工具进行验证.该方法支持的组
件有 Clock,FSMActor,ModalModel,TimedDelay.这种方法支持的组件数量少、功能单一,ModalModel
仅支持状态包含一个 FSM 细化模型,在转换时采用摊平的方式展开,易造成状态空间爆炸;
(2) 使用 Real-Time Maude 语言形式化 Ptolemy DE 模型,同时,借助 Ptolemy 自身的代码生成机制,生成可
供 Real-Time Maude 工具验证的文件.Real-Time Maude 是一种支持对实时系统和混合系统进行验证
的工具,该工具读取的文件需使用 Real-Time Maude 语言、语法编写.Real-Time Maude 基于重写逻辑
进行验证 ,适合于面向对 象实时系统 的验证 .该方法支持的组 件有 CompositeActor,FSMActor,
ModalModel,TimedDelay,Clock,CurrentTime,Pulse,Ramp,TimedPlotter,SetVariable 和 SingleEvent.这种
方式不支持延迟组件处理多个输入事件,并且事件源组件采用 tick 模拟时间的增加,增加了验证的复
杂度;同时,该方法是利用 Maude 语言形式化组件,进而进行转换,不利于组件库的扩展.

7 总结与讨论

在系统开发前期,如何对模型进行形式化验证、保证系统的可靠性,是目前学术界和工业界共同关注的热
点问题.本文提出一种基于模型转换的形式化方法来验证 Ptolemy DE 模型.Ptolemy DE 模型根据不同事件的时
间戳触发组件,时间自动机模型能够表达这个特征,因此,我们选用 Uppaal 作为验证工具.我们首先设:散事件模
型转换为时间自动机模型,进而通过调用 Uppaal 验证内核完成验证.与现有研究工作相比,该方法定义了更为完
整的 Ptolemy 组件转换规则,可以支持更多的组件;保留了模型层次化的特点,有效避免了状态空间爆炸;避免使
用 tick 计时,降低验证的复杂度.现阶段,该方法支持组件见表 2.
Table 2 Actors that can be translated
表 2 本文方法支持的组件
组件名称 组件名称 组件名称 组件名称 组件名称
CompositeActor FSMActor ModalModel TimeDelay DiscreteClock
Const Clock Ramp TimedDelay TimedPlotter
BooleanSwitch SingleEvent Pulse Scale AddSubtract
RecordAssembler RecordDisassembler Expression Limiter Maximum
BooleanSelect Multiplexor Minimum SetVariable Sampler

对于基于模型转换的形式化验证方法,如何验证模型转换的一致性是一个重要问题.在现有的 Ptolemy 模
型转换研究工作中,都是采用手工确认的方式,未来工作:
(1) 设计一种方法自动化证明 Ptolemy DE 模型与目标模型的语义一致性;
(2) Ptolemy 提供了丰富的组件库,需要继续丰富映射规则,从而支持更多的组件;
(3) Ptolemy 模型支持复杂数据类型(double、矩阵等)和复杂计算操作(三角函数、对数函数等),需要继续
设计这些复杂数据类型及复杂计算操作的映射规则.

References:
[1] Joseph B, Soonho H, Edward L, David M. Ptolemy: A framework for simulating and prototyping heterogeneous systems. Int’l
Journal of Computer Simulation, 1995,10.
[2] Wang J, Zhan NJ, Feng XY, Liu ZM. Overview of formal methods. Ruan Jian Xue Bao/Journal of Software, 2019,30(1):33−61 (in
Chinese with English abstract). http://www.jos.org.cn/1000-9825/5652.htm [doi: 10.13328/j.cnki.jos.005652]
[3] Lin HM, Zhang WH. Model checking: Theories, techniques and applications. Acta Electronica Sinica, 2002,30(z1):1907−1912 (in
Chinese with English abstract).
[4] Mudit G, Kienhuis B, Edward L, Liu J. Ptolemy II—Heterogeneous Concurrent Modeling and Design in Java. 1999.