### Abstract

The construction of a high-assurance system requires some evidence, ideally a proof, that the system as implemented will behave as required. Direct proofs of implementations do not scale up well as systems become more complex and therefore are of limited value. In recent years, refinement-based approaches have been investigated as a means to manage the complexity inherent in the verification process. In a refinement-based approach, a high-level specification is converted into an implementation through a number of refinement steps. The hope is that the proofs of the individual refinement steps will be easier than a direct proof of the implementation. However, if stepwise refinement is performed manually, the number of steps is severely limited, implying that the size of each step is large. If refinement steps are large, then proofs of their correctness will not be much easier than a direct proof of the implementation. We describe an approach to refinement-based software development that is based on automatic application of refinements, expressed as program transformations. This automation has the desirable effect that the refinement steps can be extremely small and, thus, easy to prove correct. We give an overview of the TAMPR transformation system that we use for automated refinement. We then focus on some aspects of the semantic framework that we have been developing to enable proofs that TAMPR transformations are correctness preserving. With this framework, proofs of correctness for transformations can be obtained with the assistance of an automated reasoning system.

Original language | English (US) |
---|---|

Pages | 68-77 |

Number of pages | 10 |

State | Published - Jan 1 1997 |

Event | Proceedings of the 1996 High-Assurance Systems Engineering Workshop - Niagara, Can Duration: Oct 21 1996 → Oct 22 1996 |

### Other

Other | Proceedings of the 1996 High-Assurance Systems Engineering Workshop |
---|---|

City | Niagara, Can |

Period | 10/21/96 → 10/22/96 |

### Fingerprint

### ASJC Scopus subject areas

- Engineering(all)

### Cite this

*Proving refinement transformations for deriving high-assurance software*. 68-77. Paper presented at Proceedings of the 1996 High-Assurance Systems Engineering Workshop, Niagara, Can, .

**Proving refinement transformations for deriving high-assurance software.** / Winter, Victor L.; Boyle, James M.

Research output: Contribution to conference › Paper

}

TY - CONF

T1 - Proving refinement transformations for deriving high-assurance software

AU - Winter, Victor L.

AU - Boyle, James M.

PY - 1997/1/1

Y1 - 1997/1/1

N2 - The construction of a high-assurance system requires some evidence, ideally a proof, that the system as implemented will behave as required. Direct proofs of implementations do not scale up well as systems become more complex and therefore are of limited value. In recent years, refinement-based approaches have been investigated as a means to manage the complexity inherent in the verification process. In a refinement-based approach, a high-level specification is converted into an implementation through a number of refinement steps. The hope is that the proofs of the individual refinement steps will be easier than a direct proof of the implementation. However, if stepwise refinement is performed manually, the number of steps is severely limited, implying that the size of each step is large. If refinement steps are large, then proofs of their correctness will not be much easier than a direct proof of the implementation. We describe an approach to refinement-based software development that is based on automatic application of refinements, expressed as program transformations. This automation has the desirable effect that the refinement steps can be extremely small and, thus, easy to prove correct. We give an overview of the TAMPR transformation system that we use for automated refinement. We then focus on some aspects of the semantic framework that we have been developing to enable proofs that TAMPR transformations are correctness preserving. With this framework, proofs of correctness for transformations can be obtained with the assistance of an automated reasoning system.

AB - The construction of a high-assurance system requires some evidence, ideally a proof, that the system as implemented will behave as required. Direct proofs of implementations do not scale up well as systems become more complex and therefore are of limited value. In recent years, refinement-based approaches have been investigated as a means to manage the complexity inherent in the verification process. In a refinement-based approach, a high-level specification is converted into an implementation through a number of refinement steps. The hope is that the proofs of the individual refinement steps will be easier than a direct proof of the implementation. However, if stepwise refinement is performed manually, the number of steps is severely limited, implying that the size of each step is large. If refinement steps are large, then proofs of their correctness will not be much easier than a direct proof of the implementation. We describe an approach to refinement-based software development that is based on automatic application of refinements, expressed as program transformations. This automation has the desirable effect that the refinement steps can be extremely small and, thus, easy to prove correct. We give an overview of the TAMPR transformation system that we use for automated refinement. We then focus on some aspects of the semantic framework that we have been developing to enable proofs that TAMPR transformations are correctness preserving. With this framework, proofs of correctness for transformations can be obtained with the assistance of an automated reasoning system.

UR - http://www.scopus.com/inward/record.url?scp=0030718431&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0030718431&partnerID=8YFLogxK

M3 - Paper

AN - SCOPUS:0030718431

SP - 68

EP - 77

ER -