Algorithmic Verification of Component-based Systems

This dissertation discusses algorithmic verification techniques for concurrent component-based systems modeled in the Behavior-Interaction-Priority (BIP) framework with both bounded and unbounded concurrency. BIP is a component framework for mixed software/hardware system design in a rigorous and correct-by-construction manner. System design is defined as a formal, accountable and coherent process for deriving trustworthy and optimised implementations from high-level system models and the corresponding execution platform descriptions. The essential properties of a system model are guaranteed at the earliest possible design phase, and a correct implementation is then automatically generated from the validated high-level system model through a sequence of property preserving model transformations, which progressively refines the model with details specific to the target execution platform. The first major contribution of this dissertation is an efficient safety verification technique for BIP system models, where the number of participating components is fixed and the data variables can have infinite domains, but their manipulation is limited to linear arithmetic. The key insight of our technique is to take advantage of the structure features of the BIP system and handle the computation in the components and coordination between the components in the verification separately. On the computation level, we apply the state-of-the-art counterexample abstraction techniques to reason about the behavior of components and explore all the possible reachable states ; while on the coordination level, we exploit both partial order techniques and symmetry reduction techniques to handle the state space explosion problem due to concurrency, and reduce the redundant interleavings of concurrent interactions. We have implemented the proposed techniques in a prototype tool and carried out a comprehensive performance evaluation on a set of BIP system models. The second major contribution of this dissertation is a uniform design and verification framework for parameterized systems based on BIP. Parameterized systems are systems consisting of homogeneous processes, and the parameter indicates the number of such processes in the system. A parameterized system, therefore, describes an infinite family of systems, where instances of the family can be obtained by fixing the value of the parameter. Verification of correctness of such systems amounts to verifying the correctness of every member of the infinite family described by the system. First of all, we propose the first order interaction logic (FOIL) as a formal language for parameterized system architectures and communication primitives. This logic is powerful enough to express architectures found in distributed systems, including the classical architectures : token-passing rings, rendezvous cliques, broadcast cliques, rendezvous stars. We also identify a fragment of FOIL that is well-suited for the specification of parameterized BIP systems and prove its decidability. Second, we provide a framework for the integration of mathematical models from the parameterized model checking literature in an automated way. With our new framework, we close the gap between the mathematical formalisms and algorithms from the parameterized verification research and the practice of parameterized verification, which is usually done by engineers who are not familiar with the details of the literature.