Abstract
Formal verification of a hierarchical component application involves (i) checking of behavior compliance among sub-components of each composite component, and (ii) checking of implementation of each primitive component against its behavior specification and other properties like absence of concurrency errors. In this thesis, we focus on verification of primitive components implemented in Java against the properties of obeying a behavior specification defined in behavior protocols (frame protocol) and absence of concurrency errors.
We use the Java PathFinder model checker as a core verification tool. We propose a set of techniques that address the key issues of formal verification of real-life components in Java via model checking: support for high-level property of obeying a behavior specification, environment modeling and construction, and state explosion.
The techniques include (1) an extension to Java PathFinder that allows checking of Java code against a frame protocol, (2) automated generation of