Contract-based verification and test case generation for open systems

Abstract

Current practices in software development heavily emphasize the development of reusable and modular software, which allow software components to be developed and maintained independently. While a component-oriented approach offers a number of benefits, it presents several quality assurance challenges including validating the correctness of individual components as well as their integration. Design-by-contract (DBC) offers a promising solution that emphasizes precisely defined and checkable interface specifications for software components. However, existing tools for the DBC paradigm often have some weaknesses: (1) they have difficulty in dealing with dynamically allocated data; (2) specification and checking efforts are disconnected from quality assurance tools; and (3) user feedback is quite poor. We present Kiasan, a framework that synergistically combines a number of automated reasoning techniques including symbolic execution, model checking, theorem proving, and constraint solving to support design-by-contract reasoning of object-oriented programs written in languages such as Java and C#. Compared to existing approaches to Java contract verification, Kiasan can check much stronger behavioral properties of object-oriented software including properties that make extensive use of heap-allocated data and provide stronger coverage guarantees. In addition, Kiasan naturally generates counter examples illustrating contract violations, visualization of code effects, and JUnit test cases that are driven by code and user-supplied specifications. Coverage/- cost trade-offs are controlled by user-specified bounds on the length of heap-reference chains and number of loop iterations. Kiasan’s unit test case generation facilities compare very favorably with similar tools. Finally, in contrast to other approaches based on symbolic execution, Kiasan has a rigorous foundation: we have shown that Kiasan is relatively sound and complete and the test case generation algorithm is sound.