A Theoretical Framework for Specification Refinement Via Transformations
Abstract
The idea of successively refining an abstract specification until it contains enough detail to suggest an implementation has been investigated by numerous researchers. The emphasis to date has been on techniques that, unfortunately, lead to a large amount of manual labor for each refinement step. With such techniques, both the cost and the possibility of errors arising in the formal manipulation are high. Using a theorem prover can reduce the number of manipulation errors, but the amount of labor involved is daunting. This research explores an alternative solution to the refinement problem, namely the use of syntactic transformations to realize each refinement step. We reduce formal labor by employing automatic transformations that guarantee the preservation of desirable properties such as deadlock freedom, safety, and liveness of process-algebraic specifications. This report presents three syntactic transformations that can be used to replace an atomic action in a concurrent program by a program fragment. We include applicability conditions for these transformations, and show that deadlock freedom and certain liveness properties are preserved when the transformations are applied in a context where the applicability conditions are satisfied.
Document Details
- Document Type
- Technical Report
- Publication Date
- May 01, 1998
- Accession Number
- ADA348660
Entities
People
- Paul Attie
Organizations
- Florida International University