主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
王小兵,郭文轩,段振华.消息传递的MSVL通信机制及其实现.软件学报,2018,29(6):1607-1621
消息传递的MSVL通信机制及其实现
Communication Mechanism and Its Implementation for MSVL Based on Message Passing
投稿时间:2017-07-02  修订日期:2017-09-01
DOI:10.13328/j.cnki.jos.005471
中文关键词:  通道  消息传递  通信机制  PTL  时序逻辑程序设计
英文关键词:channel  message passing  communication mechanisms  projection temporal logic  temporal logic programming
基金项目:国家自然科学基金(61672430,61420106004,61732013,61402347);中央高校基本科研业务费专项基金(JBG160306)
作者单位E-mail
王小兵 西安电子科技大学 计算机学院, 陕西 西安 710071  
郭文轩 西安电子科技大学 计算机学院, 陕西 西安 710071  
段振华 西安电子科技大学 计算机学院, 陕西 西安 710071 zhhduan@mail.xidian.edu.cn 
摘要点击次数: 760
全文下载次数: 451
中文摘要:
      建模、仿真和验证语言(MSVL)是一种时序逻辑编程语言,它是投影时序逻辑(PTL)的可执行子集.MSVL和PTL可用于并发系统的建模和性质验证.然而,MSVL缺少一种消息传递的通信机制,这种机制对于并发分布式系统的建模和验证至关重要.说明了如何在MSVL中开发和实现合适的机制来对分布式系统进行建模和验证.该机制首先定义了通道结构,对通信语句和进程结构进行形式化描述;接着介绍了这些通信语句的实现机制;最后提供了一个关于电子合同签名协议的建模和验证实例,说明消息传递在MSVL中的工作原理.
英文摘要:
      The modeling, simulation and verification language (MSVL) is a temporal logic programming language as well as an executable subset of projection temporal logic (PTL). MSVL and PTL are used for modeling and verifying properties of concurrent systems. However, MSVL lacks a mechanism of communication based on message passing which is essential for modeling and verifying concurrent distributed systems. This paper shows how to develop and implement a suitable mechanism in MSVL to model and verify concurrent distributed systems. First, channel structure is defined while communication statements and process structures are formalized. Then, the implementation mechanisms for those communication statements are presented. Finally, a modeling and verification example involving an electronic contract signing protocol is provided to illustrate how the message passing works in MSVL.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利