消息传递的MSVL通信机制及其实现

• 作者: 段振华 王小兵 郭文轩
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 通道 消息传递 通信机制 PTL 时序逻辑程序设计
• 年，卷（期）: 2018,（6）
• 所属期刊栏目: 形式化方法的理论基础专题
• 页码范围: 1607-1621
• 页数: 15页
• 分类号: TP311
• 字数: 11120字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005471

摘要

建模、仿真和验证语言(MSVL)是一种时序逻辑编程语言,它是投影时序逻辑(PTL)的可执行子集.MSVL和PTL可用于并发系统的建模和性质验证.然而,MSVL缺少一种消息传递的通信机制,这种机制对于并发分布式系统的建模和验证至关重要.说明了如何在MSVL中开发和实现合适的机制来对分布式系统进行建模和验证.该机制首先定义了通道结构,对通信语句和进程结构进行形式化描述;接着介绍了这些通信语句的实现机制;最后提供了一个关于电子合同签名协议的建模和验证实例,说明消息传递在MSVL中的工作原理.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王小兵	西安电子科技大学计算机学院	60	484	12.0	18.0
2	段振华	西安电子科技大学计算机学院	47	363	10.0	16.0
3	郭文轩	西安电子科技大学计算机学院	1	1	1.0	1.0