主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2019年第10期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
蒋屹新,林闯,曲扬,尹浩.基于Petri网的模型检测研究.软件学报,2004,15(9):1265-1276
基于Petri网的模型检测研究
Research on Model-Checking Based on Petri Nets
投稿时间:2003-08-27  修订日期:2003-08-27
DOI:
中文关键词:  时序逻辑  Petri网  状态空间  模型检测
英文关键词:peer-to-peer  information retrieval
基金项目:Supported by the National Natural Science Foundation of China under Grant No.90104002(国家自然科学基金);the National High-Tech Research and Development Plan of China under Grant No.2001AA112080(国家高技术研究发展计划(863));the National Grand Fundamental Research 973 Program of China under Grant No.2003CB314804(国家重点基础研究发展规划(973))
作者单位
蒋屹新 清华大学,计算机科学与技术系,北京,100084 
林闯 清华大学,计算机科学与技术系,北京,100084 
曲扬 清华大学,计算机科学与技术系,北京,100084 
尹浩 清华大学,计算机科学与技术系,北京,100084 
摘要点击次数: 3873
全文下载次数: 4256
中文摘要:
      模型检测是关于系统属性验证的算法和方法.它通常采用状态空间搜索的方法来检测一个给定的计算模型是否满足某个用时序逻辑公式表示的特定属性.系统模型的状态空间的爆炸问题是模型检测所面临的主要问题,其主要原因是系统自身的并发特性和状态变迁的语义交织对基于Petri网的模型检测理论和验证技术进行了较为详细的研究,着重探讨了基于Petri网状态可达图的偏序简化和偏序语义技术、基于自动机的模型检测算法、基于Petri网的状态聚合法以及基于系统对称性的参数化和符号模型检测技术,并给出了研究思路以及未来所要进行的重点研究工作.模型检测技术已在通信协议和硬件系统的验证等领域得到成功应用,并且随着各种状态空间简化技术和模型检测算法的不断优化,其在其他应用领域也展示出广泛的应用前景.
英文摘要:
      In this paper, the emerging P2P computing is first briefly introduced, including its distinct features, potential merits and applications, and the problems from which the existing P2P-based data sharing systems are suffering are further point out. To address these problems, the concept of P2P-based information retrieval is proposed, which can not only exploit the potential merits of P2P to overcome the problems of traditional information retrieval systems (e.g., lacking of scalability), but also achieve fully semantic retrieval and sharing in the context of P2P systems. Based on the ideology, PeerIS, a P2P-based information retrieval system is developed. Then, the architecture of PeerIS and its peers’ components are presented. The key issues of implementation are described, including communication, semantics-based self-reconfiguration, query processing and self-adaptive routing mechanisms, are also described. Finally, an experimental study is used to verify the advantages of PeerIS.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

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