Model Checking Implicit-Invocation Systems: An Approach to the Automatic Analysis of Architectural Style

by Jeremy S. Bradbury

Supervisor

Abstract

MSc thesis cover (2002)In general, model checking and other finite-state analysis techniques have been very successful when used with hardware systems and less successful with software systems. It is especially difficult to analyze software systems developed with the implicit-invocation architectural style because the loose coupling of their components increases the size of the finite state model. It is the goal of this research to gain insight into the larger problem of how to make model checking a better analysis and verification tool for software systems. Specifically, we will extend an existing approach to model checking implicit-invocation systems. We will then proceed to evaluate our technique on several non-trivial examples.

Bibliographic Information [Bibtex format]

@mastersthesis{Bra03,
Author = {Jeremy S. Bradbury},
Month = {May},
School = {Queen's University},
Title = {Model Checking Implicit-Invocation Systems: An Approach to the Automatic Analysis of Architectural Styles},
Year = {2002}}

Thesis: [PDF]   Presentation: [PDF]