Contract-based verification and test case generation for open systems

K-REx Repository

Show simple item record Deng, Xianghua 2007-07-09T15:49:48Z 2007-07-09T15:49:48Z 2007-07-09T15:49:48Z
dc.description.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. en
dc.description.sponsorship IBM Eclipse; Lockheed Martin ATL; US Army Research Office (ARO); US National Science Foundation; US Air Force Office of Scientific Research (AFOSR) en
dc.language.iso en_US en
dc.publisher Kansas State University en
dc.subject Software quality assurance en
dc.subject Unit testing en
dc.title Contract-based verification and test case generation for open systems en
dc.type Dissertation en Doctor of Philosophy en
dc.description.level Doctoral en
dc.description.department Department of Computing and Information Sciences en
dc.description.advisor John M. Hatcliff en
dc.subject.umi Computer Science (0984) en 2007 en August en

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search K-REx

Advanced Search


My Account


Center for the

Advancement of Digital