Pragmatic Approaches to Composition and Verification of Assured Software
Abstract
Mature engineering fields have methods of construction that have high likelihoods of success, and that guarantee the proper functioning of systems, even within hostile environments. These methods relate behavior to structure and have underlying notions of composition related to the implementation domain. Unfortunately, the construction of computer systems has not yet reached the same level of maturity. While many mathematical theories have been developed, they have in yet been brought into standard engineering practice. Bridging the gap between theory and engineering practice requires sound and pragmatic principles of construction and composition for software systems. One potentially promising and practical approach employs a combination of higher-order logic, category theory, and algebraic specifications, as incorporated into the HOL theorem prover and the Specware system for specification composition, refinement, and code synthesis. This report presents a HOL formulation of the primary mathematical concepts underlying Specware, fully explicating the underlying principles of construction and composition. Furthermore, the purpose of computer-assisted reasoning is to allow nonexperts in a given domain to nonetheless have confidence in their analysis. The HOL formulation describes the relevant concepts in an executable form that nonexperts can use in the future to construct assured specifications and ultimately assured code.
Document Details
- Document Type
- Technical Report
- Publication Date
- Mar 01, 2000
- Accession Number
- ADA376282
Entities
People
- Dan Zhou
- Shiu-kai Chin
- Susan Older
Organizations
- Syracuse University