Doctor of Philosophy / Department of Computing and Information Sciences / Matthew Dwyer / John M. Hatcliff / To analyze an open system, one needs to close it with a definition of
its environment, i.e., its execution context. Environment modeling is a significant challenge: environment
models should be general enough to permit analysis of large portions of a
system's possible behaviors, yet sufficiently precise to enable cost-effective
reasoning. This thesis presents the Bandera Environment
Generator (BEG), a toolset that automates generation of environment
models to provide a restricted form of modular model checking of Java
programs, where the module's source code is the subject of analysis along
with an abstract model of the environment's behavior.
Since the most general environments do not allow for tractable model checking, BEG has
support for restricting the environment behavior based on domain-specific knowledge and
assumptions about the environment behavior, which can be
acquired from a variety of sources. When the environment code is not
available, developers can encode their assumptions as an explicit formal
specification. When the environment code is available,
BEG employs static analyses to extract environment assumptions.
Both specifications and static analyses can be tuned to reflect domain-specific knowledge, i.e., to
describe domain-specific aspects of the environment behavior.
Initially, BEG was implemented to handle general Java applications; later, it was extended to handle
two specific domains: Graphical User Interfaces (GUI)
implemented using the Swing/AWT libraries and web applications implemented using the J2EE framework.
BEG was evaluated on several non-trivial case studies, including industrial applications from NASA, SUN, and Fujitsu. This thesis presents the domain-specific environment generation for GUI and web applications and describes BEG, its extensible architecture, usage, and how it can be extended to handle new domains.
| Identifer | oai:union.ndltd.org:KSU/oai:krex.k-state.edu:2097/1122 |
| Date | January 1900 |
| Creators | Tkachuk, Oksana |
| Publisher | Kansas State University |
| Source Sets | K-State Research Exchange |
| Language | en_US |
| Detected Language | English |
| Type | Dissertation |
Page generated in 0.0018 seconds