English  |  正體中文  |  简体中文  |  Items with full text/Total items : 93288/109022 (86%)
Visitors : 20954644      Online Users : 336
RC Version 6.0 © Powered By DSPACE, MIT. Enhanced by NTU Library IR team.
Scope Tips:
  • please add "double quotation mark" for query phrases to get precise results
  • please goto advance search for comprehansive author search
  • Adv. Search
    HomeLoginUploadHelpAboutAdminister Goto mobile version

    Please use this identifier to cite or link to this item: http://asiair.asia.edu.tw/ir/handle/310904400/4778

    Title: Compositional Verification of Concurrent Systems Using Petri-Nets-Based Condensation Rules
    Authors: Jeffrey J. P. Tsai;E. Juan;T. Murata
    Date: 1998
    Issue Date: 2009-12-02 09:04:10 (UTC+8)
    Publisher: Asia University
    Abstract: The state-explosion problem of formal verification has obstructed its application to large-scale software systems. In this article, we introduce a set of new condensation theories: IOT-failure equivalence, IOT-state equivalence, and firing-dependence theory to cope with this problem. Our condensation theories are much weaker than current theories used for the compositional verification of Petri nets. More significantly, our new condensation theories can eliminate the interleaved behaviors caused by asynchronously sending actions. Therefore, our technique provides a much more powerful means for the compositional verification of asynchronous processes. Our technique can efficiently analyze several state-based properties: boundedness, reachable markings, reachable submarkings, and deadlock states. Based on the notion of our new theories, we develop a set of condensation rules for efficient verification of large-scale software systems. The experimental results show a significant improvement in the analysis large-scale concurrent systems.
    Relation: ACM Transactions on Programming Languages and Systems 20(5):917-979
    Appears in Collections:[生物資訊與醫學工程學系 ] 期刊論文

    Files in This Item:

    File Description SizeFormat
    310904400-4778.doc30KbMicrosoft Word331View/Open

    All items in ASIAIR are protected by copyright, with all rights reserved.

    DSpace Software Copyright © 2002-2004  MIT &  Hewlett-Packard  /   Enhanced by   NTU Library IR team Copyright ©   - Feedback