National Taiwan Ocean University Institutional Repository:Item 987654321/52045
English  |  正體中文  |  简体中文  |  Items with full text/Total items : 28607/40644
Visitors : 5925203      Online Users : 289
RC Version 4.0 © Powered By DSPACE, MIT. Enhanced by NTU Library IR team.
Scope Adv. Search

Please use this identifier to cite or link to this item:

Title: Compositional Verification of Concurrent Systems Using Petri-Nets-Based Condensation Rules
Authors: Eric Y. T. Juan
Jeffrey J. P. Tsai
Tadao Murata
Contributors: 國立臺灣海洋大學:資訊工程學系
Keywords: Boundedness
compositional verification
deadlock states
Petri nets
reachability analysis
reachability graphs
reachable markings
Date: 1998
Issue Date: 2019-01-23T06:08:25Z
Publisher: ACM Transactions on Programming Languages and Systems
Abstract: 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: 20(5) pp.917-979
Appears in Collections:[Department of Computer Science and Engineering] Periodical Articles

Files in This Item:

File Description SizeFormat

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


著作權政策宣告: 本網站之內容為國立臺灣海洋大學所收錄之機構典藏,無償提供學術研究與公眾教育等公益性使用,請合理使用本網站之內容,以尊重著作權人之權益。
網站維護: 海大圖資處 圖書系統組
DSpace Software Copyright © 2002-2004  MIT &  Hewlett-Packard  /   Enhanced by   NTU Library IR team Copyright ©   - Feedback