This thesis presents a fully automated technique for procedure-modular verification of control flow temporal safety properties. Procedure-modular verification is a natural instantiation of modular verification where modularity is achieved at the level of procedures. Here it is used for the verification of software systems in the presence of code evolution, multiple method implementations (as arising from software product lines), or even unknown method implementations (as in mobile code for open platforms). The technique is built on top of a previously developed modular verification framework based on maximal model construction. In the framework, program data is abstracted away completely to achieve algorithmic verification. This restricts the class of properties that can be verified. The technique is supported by a fully automated tool called ProMoVer which is described and evaluated on a number of real-life case studies. ProMoVer is quipped with a number of features, such as automatic specification extraction, to facilitate easy usage. Moreover, it provides a proof storage and reuse mechanism for efficiency. An application area which can significantly benefit from modular verification is software product line (SPL) design. In SPL engineering, products are generated from a set of well-defined commonalities and variabilities. The products of an SPL can be described by means of a hierarchical variability model specifying the commonalities and variabilities between the individual products. The number of products generated from a hierarchical model is exponential in the size of the hierarchical model. Therefore, scalable and efficient verification for SPL is only possible by exploiting modular verification techniques. In this thesis, we propose a hierarchical variability model for modeling product families. Then the modular verification technique and ProMoVer are adapted for the SPLs described with this hierarchical model. A natural extension of the modular verification technique is to include program data in a conservative fashion, by encoding data from a finite domain through control. By this, a wider class of properties can be supported. As a first step towards including program data, Boolean values are added to the program model, specification languages, maximal model construction and modular verification principles. / QC 20120507

Feature-oriented software architecture is a way of organizing code around the features that the program provides instead of the program's objects and components. In the development of a feature-oriented software system, the developers, supplied with a set of features, select and organize features to construct the desired system. This approach, by better aligning the implementation of a system with the external view of users, is believed to have many potential benefits such as feature reuse and easy maintenance. However, there are challenges in the formal verification of feature-oriented systems: first, the product may grow very large and complicated. As a result, it's intractable to apply the traditional formal verification techniques such as model checking on such systems directly; second, since the number of feature-oriented products the developers can build is exponential in the number of features available, there may be redundant verification work if doing verification on each product. For example, developers may have shared specifications on different products built from the same set of features and hence doing verification on these features many times is really unnecessary. All these drive the need for modular verifications for feature-oriented architectures. Assume-guarantee reasoning as a modular verification technique is believed to be an effective solution. In this thesis, I compare two verification methods of this category on feature-oriented systems and analyze the results. Based on their pros and cons, I propose a new modular model checking method to accomplish verification for sequential feature compositions with cyclic connections between the features. This method first builds an abstract finite state machine, which summarizes the information related to checking the property/specification from the concrete feature design, and then applies a revised CTL model checker to decide whether the system design can preserve the property or not. Proofs of the soundness of my method are also given in this thesis.

"Feature-oriented programming is a way of designing a program around the features it performs, rather than the objects or files it manipulates. This should lead to an extensible and flexible "product-line" architecture that allows custom systems to be assembled with particular features included or excluded as needed. Composing these features together modularly, while leading to flexibility in the feature-set of the finished product, can also lead to unexpected interactions that occur between features. Robert Hall presented a manual methodology for locating these interactions and has used it to search for feature interactions in email. Li et al. performed automatic verification of Hall's system using model-checking verifications tools. Model-checking verification is state-based, and is not well-suited for verifying recursive data structures, an area where theorem-proving verification tools excel. In this thesis, we propose a methodology for using formal theorem-proving tools for modularly verifying feature-oriented systems. The methodology presented captures the essential steps for using modular techniques for modeling and verifying a system. This enables verification of individual modules, without examining the source code of the other modules in the system. We have used Hall's email system as a test case for validating the methodology."