| The prevailing trend in software and system engineering is towards component-based design. In this approach, a number of small design units called components compose a complex design. Components are typically open systems that have inputs provided by other components and provide inputs to other components. Designers face a number of design issues to build a complex design from these components. A designed system, expected to perform a set of tasks following its specification, may not behave properly due to the following reasons. Firstly, one or more components may contain bugs and behave in an undesirable fashion. Secondly, components make assumptions on their environment, and expect that the actual environment will meet these assumptions. A number of bug-free components may not work together if their input assumptions are violated. Hence, verification of a complex design can be reduced to the verification of the components and communication among them.;The interaction between components in a design can be modeled via games, and a large body of literature on design and verification shows how games can be used to analyze component compatibility and system correctness. However, while games provide an appropriate, mathematical model for interaction, solving the games is often impractical with current algorithms, due to the large state-space of games representing realistic components, together with the inherent complexity of game-solving techniques. In this thesis, we propose algorithms for the efficient analysis of games with large state spaces.;We present two novel algorithm families in the thesis: (1) Game-based Three Valued Abstraction (GTVA) for two-player games/transition systems, and (2) Magnifying Lens Abstraction (MLA) for Markov Decision Processes (MDPs). GTVA evaluates the property on the abstract game in three-valued fashion ( yes, no, maybe) and refines the abstraction by adding more details to the maybe abstract states. However, other approaches construct abstract models; thus verification becomes extremely expensive. We explain how to achieve efficient enumerative and symbolic implementations of the algorithm. MLA partitions the state-space of MDP into regions and then computes upper and lower bounds on the regions, rather than on the concrete states. MLA iterates over the regions to evaluate these limits and considers the concrete states of each region in turn, as if one were moving a magnifying lens across the abstraction and viewing the concrete states corresponding to the current region. The algorithm refines the regions in an adaptive fashion, splitting regions where we need more details, until the difference between the bounds is smaller than a user-given accuracy. We also provide a symbolic version of algorithm MLA (SMLA).;We have implemented the proposed algorithms, and we have applied them to real-life applications, including planning, protocol verification, and interface synthesis for software libraries. The symbolic three-valued algorithms for reachability, safety, compatibility, and refinement properties have been implemented in the tool TICC; case-studies illustrate the accuracy and efficiency benefits of the GTVA algorithms over other approaches. We have implemented the symbolic version of MLA in the tool PRISM. The experimental results demonstrate that MLA can provide accurate answers, with savings in the memory requirements. These algorithms promise to make the analysis of realistic component-based designs possible by pushing the limits of the size of games that can be solved. |
