| Περίληψη: | <p>Parameterised systems are infinite-state systems comprising a parameterised number of components. The problem of verifying parameterised systems is both important practically and challenging theoretically: it is important because a wide range of real-world computer systems are parameterised in nature, and it is challenging because most relevant properties of parameterised systems are undecidable in general.</p>
<p>In this thesis, we study automated verification approaches using automata-based symbolic model checking (a.k.a. regular model checking) as a generic formalism for parameterised systems. Although this formalism is Turing powerful (i.e. it can simulate the computation of Turing machines), the nice closure and algorithmic properties of finite automata still allow us to design effective heuristics for practical applications. Our main proposal for regular model checking is to use first-order theories over regular relations to reason about correctness properties, and use regular language inference as a means of proof generation. We further develop powerful reduction and abstraction techniques to reduce difficult verification problems to simpler tasks for several classes of parameterised systems. These techniques include reductions from liveness properties to safety properties for regular systems, reductions from infinite data domains to finite alphabets for array systems, and reductions from quantitative reasoning to qualitative reasoning for probabilistic systems. All these reductions are performed in a uniform logical way based on decidable first-order theories.</p>
<p>We have implemented and evaluated our automated approaches against a nontrivial collection of examples covering concurrent systems, distributed algorithms, and cryptographic protocols. The promising experimental results confirm our hypothesis that regular languages and relations provide effective heuristics for parameterised systems verification.</p>
|
|---|