Distributed symbolic reachability analysis.

详细信息   

• 作者：Chung ; Ming-Ying.
• 学历：Doctor
• 年：2007
• 导师：Ciardo, Gianfranco
• 毕业院校：University of California
• 专业：Artificial Intelligence.;Computer Science.
• ISBN：9780549419228
• CBH：3298209
• Country：USA
• 语种：English
• FileSize：7738347
• Pages：187

文摘

Formal verification techniques such as model checking have become widely used in industry for quality assurance, as they can be used to detect design errors early in the product lifecycle. State-space generation, also called reachability analysis, is an essential but very memory-intensive step in model checking. Yet, the increasing complexity of real world systems stresses the most severe limitation of model checking, the state-space explosion problem: the search space can grow exponentially in the size of the targeted systems. Even though the introduction of symbolic state-space encoding techniques, based on Binary Decision Diagrams (BDDs) or Multiway Decision Diagrams (MDDs), helps to cope with this problem, the analysis of many industrial designs still relies on the use of virtual memory.;To deal with the large memory requirement of symbolic reachability analysis, in [28], we partitioned MDDs horizontally onto a Network Of Workstations (NOW), and developed a distributed state-space generation algorithm based on the Saturation algorithm introduced in [37], so that the memory required for the state-space encoding is spread onto workstations: each workstation exclusively owns a contiguous range of MDD levels while performing Saturation-style fix-point computation over a NOW. However, this horizontal image slicing scheme comes with a serious tradeoff: it introduces a succinct MDDs partition but makes parallelism more difficult. Since, with Saturation NOW, only one workstation is active at any time, the distributed computation is virtually sequentialized. To overcome this limitation, in [29, 30], we introduced a series of approaches to accelerate Saturation NOW by using workstations' idle time and perform image computation speculatively.;In addition, to let our distributed approaches utilize the overall NOW memory while the algorithm performs its highly irregular exploration, in [31], we developed a garbage collection scheme and several operation-cache policies dedicated to symbolic reachability analysis for examining extremely complex systems. Also, in [32], we introduced a two-step chaining scheme that is fine-grained and dynamically applied to the decision-diagram nodes for improving the convergence of fix-point computation during reachability analysis. We stress that all mechanisms described in this dissertation can facilitate not only Saturation-based but also breath-first-based reachability analysis.