Automated compositional analysis for checking component substitutability

Model checking is an automated technique to verify hardware and software systems formally. Most of the model checking research has focused on developing scalable techniques for verifying large systems. A number of techniques, e.g., symbolic methods, abstractions, compositional reasoning, etc. have been proposed towards this goal. While methods based on symbolic reasoning (using binary decision diagrams or satisfiability solving) and methods based on computing abstractions automatically in a counterexample-driven manner have proved to be useful in verifying hardware and software systems, they do not directly scale to systems with large number of modules or components. The reason is that they try to verify the complete system in a monolithic manner, which inevitably leads to the state-space explosion problem, i.e., there are too many states in the system to explore exhaustively. Compositional reasoning techniques try to address this problem by following a divide-and-conquer approach: the task of system verification is divided into several sub-tasks, each involving a small subset of system components. Assume-Guarantee Reasoning (AGR) is a particular form of compositional verification, where one first generates environment assumptions for a component and then discharges them on its environment (i.e., the other components) separately. Assume-Guarantee Reasoning methods have been mainly studied in a theoretical context traditionally. The central bottleneck in making them practical is the lack of algorithms to automatically compute appropriate environment assumptions for components.; A recent approach for computing these assumptions relies on combining machine learning algorithms together with model checking techniques to achieve its goal. The technique uses machine learning algorithms for finite state machines in an iterative counterexample-driven manner, assisted by a model checker. In this thesis, we build an abstract framework for automated AGR based on machine learning algorithms and propose new algorithms for instantiating this framework for several different notions of composition and conformances. In particular, we propose compositional techniques for checking simulation conformance, based on learning regular tree languages, and for checking deadlock based on learning failure languages. Moreover; we present an approach to scale this framework to real-life systems communicating via shared memory by using new algorithms for learning machines with large alphabets together with symbolic model checking.; Most industrial hardware and software systems are designed using previously available off-the-shelf components. Such component technologies are gaining acceptance in both hardware and software engineering as effective tools for quickly assembling complex systems from pre-developed components. During their life-cycle, these components may undergo several bug-fixes and upgrades and therefore need to be verified after every such component substitution step. In this thesis, we refer to this problem as checking component substitutability. This problem is pervasive across both software and hardware engineering communities, where a large amount of effort is spent on re-validating systems from scratch after each update. In the thesis, we first formalize the problem for software systems taking into account that evolution of components may involve both addition of new features and removal of old behaviors. Then, we propose a solution based on an incremental automated AGR technique, together with counterexample-driven automated abstraction techniques.; The new techniques proposed in this thesis have been implemented and evaluated on both software and hardware benchmarks and are shown to be useful in practice.