English  |  正體中文  |  简体中文  |  Items with full text/Total items : 28607/40644
Visitors : 4760076      Online Users : 298
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: http://ntour.ntou.edu.tw:8080/ir/handle/987654321/52045

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
URI: http://ntour.ntou.edu.tw:8080/ir/handle/987654321/52045
Appears in Collections:[資訊工程學系] 期刊論文

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