The proposed renement method may seem to potentially result in a large FSA due to the involved state splitting. However, the current version of our renement algorithm [10] bounds the number of possible renements by allowing a single state with incoming transitions labeled with I per predicate value combination. For larger objects, we may utilize a smaller number of state predicates to more efficiently obtain an invariant-based FSA; in such cases increasing this renement bound could benefit the quality of the obtained automata. Additionally, we plan to assess the utility of statistics-based reasoning about state renements (similar to [2,16]).
For example, trace statistics, annotated on FSA transitions, may uncover some invocation casualties that can be effected in additional state renements.
Another benet of rening the invariant-based FSA in the described manner is identication of transitions that are legal according to the inferred invariants, but are not executed in the system executions. Hence, such behavior is a strong
candidate for further testing and renement of the object specication. For example, the renement process identies that the looping transition labeled makeEmpty on state S02 is not traversed with the dynamic traces since it is a maybe transition. A detailed inspection of the implementation reveals this particular transition to be impossible and a result of overgeneralized program invariants.
Defines standard
Replaced/Superseded by document(s)
Cancelled by
Amended by
| File | MIME type | Size (KB) | Language | Download | |
|---|---|---|---|---|---|
| usc-csse-2010-513.pdf | application/pdf | 227.93 KB | English | DOWNLOAD! |
Provides definitions
Abstract
Software behavioral models have proven useful for design,
validation, verication, and maintenance. However, existing
approaches for deriving such models sometimes overgeneralize what behavior is legal. We outline a novel approach that utilizes inferred likely program invariants and method invocation sequences to obtain an object-level model that describes legal execution sequences. The key insight is using program invariants to identify similar states in the sequences.
We exemplify how our approach improves upon certain aspects of the state-of-the-art FSA-inference techniques.