微信服务号

微信订阅号

2025年4月4日 23:54 星期五
首页 > 过刊浏览>2004年第15卷第9期 >1265-1276
PDF HTML阅读 XML下载 导出引用 引用提醒
基于Petri网的模型检测研究
作者:
基金项目:

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))

  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [46]
    • |
  • 相似文献
    • |
  • 引证文献
    • | |
  • 文章评论
    摘要:

    模型检测是关于系统属性验证的算法和方法.它通常采用状态空间搜索的方法来检测一个给定的计算模型是否满足某个用时序逻辑公式表示的特定属性.系统模型的状态空间的爆炸问题是模型检测所面临的主要问题,其主要原因是系统自身的并发特性和状态变迁的语义交织对基于Petri网的模型检测理论和验证技术进行了较为详细的研究,着重探讨了基于Petri网状态可达图的偏序简化和偏序语义技术、基于自动机的模型检测算法、基于Petri网的状态聚合法以及基于系统对称性的参数化和符号模型检测技术，并给出了研究思路以及未来所要进行的重点研究工作.模型检测技术已在通信协议和硬件系统的验证等领域得到成功应用，并且随着各种状态空间简化技术和模型检测算法的不断优化，其在其他应用领域也展示出广泛的应用前景.

    Abstract:

    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.

    参考文献
    [1]Clarke EM, Grumberg O, Peled D. Model Checking. Cambridge: MIT Press, 2001.35～49.
    [2]Sistla AP, Clarke EM. The complexity of propositional linear temporal logics. Journal of the ACM, 1985,32(3):733～749.
    [3]Clarke EM, Emerson EA, Sistla AP. Automatic verification of finite state concurrent system using temporal logical specification.ACM Trans. on Programming Language and Systems, 1986,8(2):244～263.
    [4]Lin C. Computer Network and Computer System Performance Eyaluation. Beijing: Tsinghua University Press, 2001 (in Chinese).
    [5]Emerson EA, Halpern JY. Sometimes and Not Never revisited: On branching versus linear time. Journal of the ACM, 1986,33(1):151～178.
    [6]Girault C, Valk R. Petri Nets for System Engineering: A Guide to Modeling, Verification and Application. Springer-Verlag, 2003.
    [7]Vardi MY. Linear vs. Banching tme-A complexity-theoretic perspective. In: Proc. of the 13th Annual IEEE Symp. on Logic in Computer Science. IEEE Computer Society Press, 1998.94～405.
    [8]Bhat G, Cleaveland R, Grumberg O. Efficient on-the-fly model checking for CTL. In: Proc. of the 10th Annual IEEE Symp. on Logic in Computer Science. IEEE Computer Society Press, 1995. 388～397.
    [9]Bryant RE. Graph-Based algorithms for boolean function manipulation. IEEE Trans. on Computers, 1986,35(8):667～691.
    [10]Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ. Symbolic model checking: 1020 states and beyond. Information and Computation, 1998,2:141～170.
    [11]Burch JR, Clarke EM, Long DE, McMillan KI, Dill DL. Symbolic model checking for sequential circuit verification. IEEE Trans.on Computer-aided Design of Integrated Circuits, 1994,13(4):401～424.
    [12]Burch JR, Clarke EM, Long DE. Symbolic model checking with partitioned transition relations. In: Proc. of the Int'l Conf. on Very Large Scale Integration. 1991.49～58.
    [13]Abdulla PA, Bjesse P, Een N. Symbolic reachability analysis based on SAT-solver. In: Proc. of the 6th Int'l Conf. on Tools and Algorithm for Construction and Analysis of Systems (TACAS 2000). LNCS 1785, Springer-Verlag, 2000. 411～425.
    [14]Biere A, Cimatti A, Clarke E. Symbolic model checking without BDDs. In: Proc. of the 5th Int'l Conf. on Tools and Algorithm for Construction and Analysis of Systems (TACAS'99). LNCS 1579, Springer-Verlag, 1999. 193～207.
    [15]Gerth R, Peled D, Vardi M, Wolper P. Simple on-the-fly automatic verification of linear temporal logic. In: Proc. of the 15th Int'l Conf. on Protocol Specification, Testing and Verification. Warsaw, 1993.
    [16]Courcoubets C, Vardi M, Wolper P, Yannakakis M. Memory-Efficient algorithms for the verification of temporal properties.Formal Methods in System Design, 1992,1:275～288.
    [17]Holzmann GJ, Peled D, Yannakakis M. On nested depth first search. In: Proc. of the 2nd SPIN Workshop. AMS, 1996. 23～32.
    [18]Holzmann GJ. The spin model checker. IEEE Trans. on Software Engineering, 1997,23(5):279～295.
    [19]Varpaaniemi K, Hiekkanen K, Lilius J. PROD 3.2-An advanced tool for efficient reachability analysis. In: Proc. of the 9th Int'l Conf. on Computer Aided Verification (CAV'97). LNCS 1254, Springer-Verlag, 1997. 472～475.
    [20]Best B, Grahlmann B. PEP-more than a Petri nets. In: Proc. of the 2nd Int'1 Workshop, TACAS'96. LNCS 1055, Passau:Springre-Verlag, 1996. 397～401.
    [21]Bollig B, Leucker M. Deciding LTL over Mazurkiewicz traces. In: Proc. of the IEEE 8th Symp. on Temporal Representation and Reasoning. 2001. 189～198.
    [22]Alur R, Brayton RK, Henzinger TA, Qadeer S, Rajamani SK. Partial-Order reduction in symbolic state space exploration. In: Proc.of the 9th Int'l Conf. on Computer Aided Verification. LNCS 1254, Grumberg: Springer-Verlag, 1997. 340～351.
    [23]Varpaanieme K. On the stubborn set method in reduced state space generation [Ph.D. Thesis]. Helsinki University of Technology,1998.
    [24]Godefroid P. Partial-Order methods for the verification of concurrent systems, an approach to the state-explosion problem. LNCS1032, Springer-Verlag, 1996.
    [25]Varpaaniemi K. Stable models for stubborn sets. In: Proc. of the CS&P'99 Workshop. Warsaw, 1999. 263～274.
    [26]Vernadat F, Azema P, Michel F. Covering step graph. In: Proc. of the 17th Int'l Conf. on Application and Theory of Petri Nets 96.LNCS 1091, Osaka: Springer-Verlag, 1996. 516～535.
    [27]Ribet PO, Vernadat F, Berthomieu B. On combining the persistent sets method with the covering steps graph method. In: Proc. of the FORTE 02. LAAS Report 02388, 2002.
    [28]Esparza J, Schroter C. Net reductions for LTL model-checking. In: Proc. of the 11th CHARME. LNCS 2144, Springer-Verlag, 2001.310～324.
    [29]Esparza J, Heljanko K. Implementing LTL model checking with net unfoldings. In: Proc. of the 8th Int'l SPIN Workshop on Model Checking of Software (SPIN 2001). LNCS 2057, Springer-Verlag, 2001.37～56.
    [30]Korver H, Springintveld J. A computer-checked verification of Milner's scheduler. In: Proc. of the Int'l Symp. on the Theoritical Aspect of Computer Software (TACS'94). LNCS 789, Springer-Verlag, 1994. 161～178.
    [31]Jensen K. An introduction to the theoretical aspects of coloured Petri nets. In: de Bakker JW, de Roever WP, Rozenberg G, eds. A Decade of Concurrency. LNCS 803, Springer-Verlag, 1994. 230～272.
    [32]Corbert JC. Evaluating deadlock detection methods for concurrent software. IEEE Trans. on Software Engineering, 1996,22(3):161～180.
    [33]Heljanko K. Combining symbolic and partial order methods for model checking 1-safe Petri nets [Ph.D. Thesis]. Helsinki University of Technology, 2002.
    [34]Chiola G, Dutheillet C, Franceschinis G, Haddad S. Stochastic well-formed colored nets and symmetric modeling applications.IEEE Trans. on Computers, 1993,42(11 ): 1343～1360.
    [35]Kurshan RP, McMillan K. A structural induction theorem for processes. In: Proc. of the 8th Annual ACM Symp. on Principles of Distributed Computing. Alberta, 1989. 239～247.
    [36]Haddad S, I1ie JM, Taghelit M, Zouari B. Symbolic reachability graph and partial symmetries. In: Proc. of the 16th Int'l Conf. on Application and Theory of Petri Nets. LNCS 935, Springer-Verlag, 1995. 238～251.
    [37]Haddad S, Ilie JM, Ajami K. A model checking method for partially symmetric systems. In: FORTE 2000. 2000. 121～136.
    [38]Miller A, Calder M. An application of abstraction and induction techniques to degenerating systems of processes. In: Proc. of the Int'l Workshop on Model-Checking for Dependable Software Intensive Systems (MCDSIS 2003). IEEE Computer Society Press,2003.
    [39]Li J, Suzuki I, Yamashita M. A new structural induction theorem for rings of temporal Petri nets. IEEE Trans. on Software Engineering, 1994,20(2):115～126.
    [40]Clarke EM, Grumberg O, Jha S. Verifying parameterized networks using abstraction and regular languages. In: Proc. of the 6th Int'l Conf. on Concurrency Theory. LNCS 962, Springer-Verlag, 1995. 365～407.
    [41]German S, Sistla AP. Reasoning about systems with many processes. Journal of the ACM, 1992,39(3):675～735.
    [42]Vernier I. Symbolic executions of symmetrical parallel programs. In: Proc. of the 4th Euromicro Workshop on Parallel and Distributed Processing. Portugal, 1996. 327～334.
    [43]Cousot P, Cousot R. Refining model checking by abstract interpretation. Journal of Automated Software Engineering, 1999,6(1):69～95.
    [44]Ritchey RW, Ammann P. Using model checking to analyze network vulnerabilities. In: Proc. of the 2000 IEEE Symp. on Security and Privacy. Oakland, 2000. 156～165.
    [45]Ramakrishnan CR, Sekar R. Model-Based analysis of configuration vulnerabilities. Journal of Computer Security (JCS), 2002,10(1):189～209.
    [4]林闯.计算机网络和系统性能评价.北京:清华大学出版社,2001.
    相似文献
    引证文献
引用本文

蒋屹新,林闯,曲扬,尹浩.基于Petri网的模型检测研究.软件学报,2004,15(9):1265-1276

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2003-08-27
  • 最后修改日期:2003-08-27
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19788084位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号