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

来源：软件学报杂志2018年第6期北京时间：

作者：王小兵,郭文轩,段振华

单位：王小兵，西安电子科技大学 计算机学院, 陕西 西安 71007111,郭文轩，西安电子科技大学 计算机学院, 陕西 西安 71007102,段振华，西安电子科技大学 计算机学院, 陕西 西安 71007103

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

关键词：通道;消息传递;通信机制;PTL;时序逻辑程序设计

基金资助：国家自然科学基金（61672430，61420106004，61732013，61402347）；中央高校基本科研业务费专项基金（JBG160306）