摘要:建模、仿真和验证语言（MSVL）是一种时序逻辑编程语言，它是投影时序逻辑（PTL）的可执行子集.MSVL和PTL可用于并发系统的建模和性质验证.然而，MSVL缺少一种消息传递的通信机制，这种机制对于并发分布式系统的建模和验证至关重要.说明了如何在MSVL中开发和实现合适的机制来对分布式系统进行建模和验证.该机制首先定义了通道结构，对通信语句和进程结构进行形式化描述；接着介绍了这些通信语句的实现机制；最后提供了一个关于电子合同签名协议的建模和验证实例，说明消息传递在MSVL中的工作原理.
Abstract: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.
PDF全文下载地址:
http://jos.org.cn/jos/article/pdf/5471
删除或更新信息，请邮件至freekaoyan#163.com(#换成@)
消息传递的MSVL通信机制及其实现
本站小编 Free考研考试/2022-01-02
相关话题/通信 系统 结构 逻辑 语言
领限时大额优惠券,享本站正版考研考试资料!
优惠券领取后72小时内有效，10万种最新考研考试考证类电子打印资料任你选。涵盖全国500余所院校考研专业课、200多种职业资格考试、1100多种经典教材，产品类型包含电子书、题库、全套资料以及视频，无论您是考研复习、考证刷题，还是考前冲刺等，不同类型的产品可满足您学习上的不同需求。 ...考试优惠券 本站小编 Free壹佰分学习网 2022-09-19一种嵌套中断系统的建模和分析方法
摘要:在嵌入式系统和各类操作系统中，中断机制是确保实时响应各类异步事件的重要方法.通常在处理一个中断事件的过程中，往往会有更紧迫的中断事件请求响应，因而发生中断嵌套.建模并验证嵌套中断系统是具有挑战性的工作.提出一种建模和验证嵌套中断系统的方法.首先，提出基于投影时序逻辑（projectiontem ...中科院软件研究所 本站小编 Free考研考试 2022-01-02机器人关节通信总线系统的建模与验证
摘要:高速串行现场总线（controllerareanetwork，简称CAN）被广泛部署到机器人通信系统中.而服务机器人任务具有并发性和高实时性的特点，因此，如何根据总线协议规范和应用需求精化设计模型，保证系统设计的正确性和实时性要求，避免设计阶段的漏洞十分必要.针对传统方法的局限性，提出使用形式 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02医学影像计算机辅助检测与诊断系统综述
摘要:计算机辅助检测/诊断（computer-aideddetection/diagnosis，简称CAD）能够提高诊断的准确性，减少假阳性的产生，为医生提供有效的诊断决策支持.旨在分析计算机辅助诊断工具的最新发展.以CAD研究较多的四大致命性癌症的发病医学部位为主线，按照不同的成像技术和病类，对目 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02基于同态加密系统的图像鲁棒可逆水印算法
摘要:同态加密技术可用于保护数据隐私并允许对密文数据进行算术操作，在云计算安全上有着很好的应用前景.针对云计算中的隐私保护和数据安全等问题，提出了一种基于同态加密系统的图像鲁棒可逆水印算法，主要思想为：（1）对原始图像进行分块和利用Paillier加密系统进行加密得到密文图像；（2）在加密域中，通过 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02基于创意序列学习的艺术风格学习与绘制系统
摘要:在众多传统艺术绘画形式中，笔触是被现代计算机绘画工具（GIMP、Photoshop和Painter）普遍采用的形式之一.创新性地提出了服务于非真实感渲染AI辅助艺术创作系统（A4）.系统能够实现自动生成特定艺术家风格的笔触效果.该系统在强化学习框架下，主要进行以下研究工作：（1）提出基于PGP ...中科院软件研究所 本站小编 Free考研考试 2022-01-02基于图结构的大数据分析与管理技术专刊前言
摘要:Abstract:PDF全文下载地址:http://jos.org.cn/jos/article/pdf/5458 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02分布式图处理系统技术综述
摘要:图作为一种基本的数据类型，是对现实世界中对象及其关联关系的一种抽象.现实中，许多科学问题都可以被模型化为图的问题，因此，对图数据进行分析非常重要.图数据分析在语义Web分析、社交网络、生物基因分析以及信息检索等领域有着广泛的应用.随着移动互联、物联网等信息技术的发展，图数据的规模处于持续增长的 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02基于MapReduce的图结构聚类算法
摘要:图结构聚类（SCAN）是一种著名的基于密度的图聚类算法，该算法不仅能够找到图中的聚类结构，而且还能发现图中的Hub节点和离群节点.然而，随着图数据规模越来越大，传统的SCAN算法的复杂度为O（m1.5）（m为图中边的条数），因此很难处理大规模的图数据.为了解决SCAN算法的可扩展性问题，提出一 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02多维图结构聚类的社交关系挖掘算法
摘要:社交关系的数据挖掘一直是大图数据研究领域中的热门问题.图聚类算法如SCAN（structuralclusteringalgorithmfornetwork）虽然可以迅速地从海量图数据中获得关系紧密的社区结构，但这类社区往往只表示了社交对象的聚集，无法反馈对象间的真实社交关系，如家庭成员、同事、 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02经验研究中情景感知需求获取与建模系统文献综述
摘要:情景感知（contextaware）的应用是当前的一个研究热点，但是，由于情景的复杂性和不确定性，如何获取这些应用的需求面临着巨大挑战，需求工程领域出现了大量的研究来解决这一挑战.使用系统文献综述（systematicliteraturereview）的方法首先分析了不同情景维度对需求获取与建 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02
