This research aims to develop a formal, integrated analysis framework based on a synergistic combination of various analysis techniques such as symbolic execution, model checking, static analysis, constraint solving, and theorem proving for reasoning about behaviors of open systems (whose computational structures are incomplete). The framework enables a holistic approach to quality-assurance of modern software systems for strong behavioral properties including contract checking, assisting code inspection and understanding, and automatic test case generation. Key technical challenges in providing such framework are scalability of the analysis and support for modular reasoning about deep semantic properties of software components that heavily use dynamically created heap objects, high-level programming constructs and abstractions (e.g., design patterns), libraries, and software frameworks. This project lays the foundation for a long-term investigation of an automatic formal analysis for open object-oriented systems that draws its strengths from significant advancements of various analysis techniques over the past several years. In addition to reasoning about strong functional properties, the approach can support a spectrum of software quality-assurance techniques for future investigations such as analyzing concurrency aspects, secure information-flow, and system event orderings (e.g., useful for checking protocol conformance of application programming interfaces).
Best practices in software development techniques heavily emphasize the development of reusable and modular software, which allow software components to be developed and maintained independently. On the other hand, the most commonly used technique to assure software quality today is testing. Testing fails to adequately address a wide-range of quality-assurance issues when following these best practices such as assuring individual component behaviors and component integration. Testing does not provide high-assurance and it is expensive (i.e., it usually accounts for more than 50% of the total software development cost). Despite significant advances in software analysis techniques to assure software quality (e.g., symbolic execution, model checking, theorem proving, and static analyses), each of these techniques does not address emerging issues in modern open systems. Some key technical challenges are scalability of the analysis and support for modular reasoning about deep semantic properties of software components that heavily use dynamically created heap objects, high-level programming constructs and abstractions (e.g., design patterns), libraries, and software frameworks. For example, reasoning frameworks like ESC/Java offer contract-based reasoning of open systems; while they have been successful to some extent, they do not provide analysis of strong heap properties. In addition, their analysis is not directly leveraged for automating some of the developers' daily tasks such as code understanding and testing. Thus, developers are less likely to adopt the approach because the burden of writing contracts is not perceived to be cost-effective. To provide a research foundation for addressing these challenges, in this NSF CAREER project, we investigated novel software quality assurance techniques that could reason about strong properties of open systems, as well as providing a well-thought out application methodology that developers are likely willing to adopt. We developed a holistic approach to quality-assurance of modern software systems for strong behavioral properties including contract checking, assisting code inspection and understanding, and automatic test case generation. We applied our techniques to two domains: (1) dynamic Java software with contracts specified using the widely used Java Modeling Language (JML) research contract language for Java, and (2) safety/security-critical embedded systems written in Spark Ada -- a subset of Ada; the Spark language and toolset developed by Altran Praxis and AdaCore is one of the premier commercial development systems for developing high-assurance software. We developed prototypes for these application domains and demonstrated that our approach gives at least two-order magnitudes of reduction in terms analysis time and space (i.e., computer memory and storage) cost than previously known techniques on various realistic systems including secure embedded systems supplied as challenge problems by our industrial partner -- Rockwell Collins. In addition, we demonstrated that our approach could automatically generate test cases with a very high-degree coverage. We also integrated our research prototypes in a popular Eclipse Integrated Development Environment (IDE) to illustrate how our prototypes could be deployed in a regular software development workflow to aid code inspection, understanding, and debugging. We are currently collaborating with AdaCore and Altran-Praxis to transition our techniques/research prototypes as back-end tools for the next generation of Spark toolset to be released in 2014. Regarding broader impacts of the work, the research investigations and collaborations with industry led to: (a) several academic papers on how to verify contracts efficiently while producing evidences (e.g., test cases) that justify the conclusions reached by the analysis, and (b) a software infrastructure suitable as research and teaching vehicles for prototyping software analysis techniques and teaching software specification and verification.
