A Formal Method to Analyze Framework-Based Software

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.

Name thesis:degree_name

PhD

Grantor dc:publisher

Brigham Young University - Provo

Author dc:creator

• Larson, Trent N.

• formal verification
• software frameworks
• software verification
• framework-based software systems
• Computer Sciences

Language dc:language

English

Repository record dc:identifier

https://scholarsarchive.byu.edu/etd/104

OAI identifier oai:identifier

oai:scholarsarchive.byu.edu:etd-1103