This thesis presents a framework for understanding first-order theories by investigating their models. A common application is to help users, who are not necessarily experts in formal methods, analyze software artifacts, such as access-control policies, system configurations, protocol specifications, and software designs. The framework suggests a strategy for exploring the space of finite models of a theory via augmentation. Also, it introduces a notion of provenance information for understanding the elements and facts in models with respect to the statements of the theory. The primary mathematical tool is an information-preserving preorder, induced by the homomorphism on models, defining paths along which models are explored. The central algorithmic ideas consists of a controlled construction of the Herbrand base of the input theory followed by utilizing SMT-solving for generating models that are minimal under the homomorphism preorder. Our framework for model-exploration is realized in Razor, a model-finding assistant that provides the user with a read-eval-print loop for investigating models.
| Identifer | oai:union.ndltd.org:wpi.edu/oai:digitalcommons.wpi.edu:etd-dissertations-1457 |
| Date | 30 April 2015 |
| Creators | Saghafi, Salman |
| Contributors | Daniel J. Dougherty, Advisor, Joshua D. Guttman, Committee Member, George T. Heineman, Committee Member, John D. Ramsdell, Committee Member, Craig E. Wills, Department Head |
| Publisher | Digital WPI |
| Source Sets | Worcester Polytechnic Institute |
| Detected Language | English |
| Type | text |
| Format | application/pdf |
| Source | Doctoral Dissertations (All Dissertations, All Years) |
Page generated in 0.0015 seconds