Date of Award
December 2019
Document Type
Dissertation
Degree Name
Doctor of Philosophy (PhD)
Department
School of Computing
Committee Member
Murali Sitaraman
Committee Member
Wayne D Goddard
Committee Member
John D McGregor
Committee Member
Nigamanth Sridhar
Abstract
Component-based software verification is a difficult challenge because developers must specify components formally and annotate implementations with suitable assertions that are amenable to automation. This research investigates the intrinsic complexity in this challenge using a component-based case study. Simultaneously, this work also seeks to minimize the extrinsic complexities of this challenge through the development and usage of a formalization integrated development environment (F-IDE) built for specifying, developing, and using verified reusable software components.
The first contribution is an F-IDE built to support formal specification and automated verification of object-based software for the integrated specification and programming language RESOLVE. The F-IDE is novel, as it integrates a verifying compiler with a user-friendly interface that provides a number of amenities including responsive editing for model-based mathematical contracts and code, assistance for design by contract, verification, responsive error handling, and generation of property-preserving Java code that can be run within the F-IDE.
The second contribution is a case study built using the F-IDE that involves an interplay of multiple artifacts encompassing mathematical units, component interfaces, and realizations. The object-based interfaces involved are specified in terms of new mathematical models and non-trivial theories designed to encapsulate data structures and algorithms. The components are designed to be amenable to modular verification and analysis.
Recommended Citation
Welch, Daniel Thomas, "Scaling Up Automated Verification: A Case Study and a Formalization IDE for Building High Integrity Software" (2019). All Dissertations. 2517.
https://tigerprints.clemson.edu/all_dissertations/2517