Doctor of Philosophy / Department of Computing and Information Sciences / John M. Hatcliff / 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.
| Identifer | oai:union.ndltd.org:KSU/oai:krex.k-state.edu:2097/345 |
| Date | January 1900 |
| Creators | Deng, Xianghua |
| Publisher | Kansas State University |
| Source Sets | K-State Research Exchange |
| Language | en_US |
| Detected Language | English |
| Type | Dissertation |
Page generated in 0.0017 seconds