Proving refinement transformations for deriving high-assurance software

Victor L. Winter, James M. Boyle

Research output: Contribution to conferencePaper

4 Citations (Scopus)

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 languageEnglish (US)
Pages68-77
Number of pages10
StatePublished - Jan 1 1997
EventProceedings of the 1996 High-Assurance Systems Engineering Workshop - Niagara, Can
Duration: Oct 21 1996Oct 22 1996

Other

OtherProceedings of the 1996 High-Assurance Systems Engineering Workshop
CityNiagara, Can
Period10/21/9610/22/96

Fingerprint

Software engineering
Automation
Semantics
Specifications

ASJC Scopus subject areas

  • Engineering(all)

Cite this

Winter, V. L., & Boyle, J. M. (1997). 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.

1997. 68-77 Paper presented at Proceedings of the 1996 High-Assurance Systems Engineering Workshop, Niagara, Can, .

Research output: Contribution to conferencePaper

Winter, VL & Boyle, JM 1997, 'Proving refinement transformations for deriving high-assurance software', Paper presented at Proceedings of the 1996 High-Assurance Systems Engineering Workshop, Niagara, Can, 10/21/96 - 10/22/96 pp. 68-77.
Winter VL, Boyle JM. Proving refinement transformations for deriving high-assurance software. 1997. Paper presented at Proceedings of the 1996 High-Assurance Systems Engineering Workshop, Niagara, Can, .
Winter, Victor L. ; Boyle, James M. / Proving refinement transformations for deriving high-assurance software. Paper presented at Proceedings of the 1996 High-Assurance Systems Engineering Workshop, Niagara, Can, .10 p.
@conference{9e9fbfaa9e33450bbc1280d895dbc44d,
title = "Proving refinement transformations for deriving high-assurance software",
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.",
author = "Winter, {Victor L.} and Boyle, {James M.}",
year = "1997",
month = "1",
day = "1",
language = "English (US)",
pages = "68--77",
note = "Proceedings of the 1996 High-Assurance Systems Engineering Workshop ; Conference date: 21-10-1996 Through 22-10-1996",

}

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 -