Decomposing the DSub Retrenchment

Hall, J. G. and Gurukumba, T. (2001). Decomposing the DSub Retrenchment. Technical Report 2001/04; Department of Computing, The Open University.

DOI: https://doi.org/10.21954/ou.ro.00015ff3

Abstract

The use of software has become prevalent in high integrity systems such as safety critical systems. The correctness of such software, i.e. thedelivery of a proper service that adheres to specified requirements, is a fundamental issue.Formal methods, which is a software development technique based on mathematics, addresses the issue of correctness of software. In theformal development of computer programs, a correctness- preserving transformation such as refinement may be used. Functional correctness is preserved by means of data refinement as well asalgorithmic refinement.One limitation of refinement is that it only works for operations of the same signature. In particular, in the concrete operation, some state variables may become input variables (e.g., when the variables denote values from some prior computations), some output variables may be added to the operations, and some variables may be constrained to a particular type (e.g., due to the finiteness of computer representation). In that case the signature of the concrete operation would be different from that of the abstract operation. The above techniques introduce the difference in signatures between abstract and concrete operations as a side effect but may be necessary in maintaining safe functionality in the concreteoperation.Retrenchment is a liberalized form of refinement that can be used to reason about functional correctness-preservation where operations may have different signatures. The Operation Retrenchment Proof Obligation is a predicate that characterizes the retrenchment of one operation by another. The proof obligation has slots for variouscharacteristics of a particular retrenchment, e.g., invariants, preconditions, operations, of the two machines involved in the retrenchment. Proving this proof obligation may provide structured proofs in terms of the proof steps required to discharge the operation retrenchment proof obligation. In particular, patterns in proofs can be coded into proof tactics enabling proofs to be automated.Automation enables the provision of software tools which may make the application of formal methods tractable, scalable and less prone to human error.