Software systems are frequently designed using abstractions that make software verification tractable. Specifically, by choosing meaningful, formal abstractions for interfaces and then designing according to those interfaces, one can verify entire systems according to behavioral predicates. While impractical for systems in general, framework-based software architectures are a type of system for which formal analysis can be beneficial and practical over the life of the system. We present a method to formally analyze behavioral properties of framework-based software with higher-order logic and then demonstrate its utility for a significant, modern system.
College and Department
Physical and Mathematical Sciences; Computer Science
BYU ScholarsArchive Citation
Larson, Trent N., "A Formal Method to Analyze Framework-Based Software" (2002). Theses and Dissertations. 104.
formal verification, software frameworks, software verification, framework-based software systems