National Taiwan Ocean University Institutional Repository:Item 987654321/52045
English  |  正體中文  |  简体中文  |  全文筆數/總筆數 : 27287/39131
造訪人次 : 2442760      線上人數 : 33
RC Version 4.0 © Powered By DSPACE, MIT. Enhanced by NTU Library IR team.
搜尋範圍 進階搜尋


題名: Compositional Verification of Concurrent Systems Using Petri-Nets-Based Condensation Rules
作者: Eric Y. T. Juan
Jeffrey J. P. Tsai
Tadao Murata
貢獻者: 國立臺灣海洋大學:資訊工程學系
關鍵詞: Boundedness
compositional verification
deadlock states
Petri nets
reachability analysis
reachability graphs
reachable markings
日期: 1998
上傳時間: 2019-01-23T06:08:25Z
出版者: ACM Transactions on Programming Languages and Systems
摘要: 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.
關聯: 20(5) pp.917-979
顯示於類別:[資訊工程學系] 期刊論文


檔案 描述 大小格式瀏覽次數



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