The Library
A COMPOSITIONAL FRAMEWORK FOR FAULT-TOLERANCE BY SPECIFICATION TRANSFORMATION
Tools
UNSPECIFIED (1994) A COMPOSITIONAL FRAMEWORK FOR FAULT-TOLERANCE BY SPECIFICATION TRANSFORMATION. THEORETICAL COMPUTER SCIENCE, 128 (1-2). pp. 99-125. ISSN 0304-3975.
Research output not available from this repository.
Request-a-Copy directly from author or use local Library Get it For Me service.
Abstract
The incorporation of a recovery algorithm into a program can be viewed as a program transformation, converting the basic program into a fault-tolerant version. We present a framework in which such program transformations are accompanied by a corresponding specification transformation which obtains properties of the fault tolerant versions of the programs from properties of the basic programs. Compositionality is achieved when every property of the fault tolerant version can be obtained from a transformed property of the basic program.
A verification method for proving the correctness of specification transformations is presented. This makes it possible to prove just once that a specification transformation corresponds to a program transformation, removing the need to prove separately the correctness of each transformed program.
Item Type: | Journal Article | ||||
---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||
Journal or Publication Title: | THEORETICAL COMPUTER SCIENCE | ||||
Publisher: | ELSEVIER SCIENCE BV | ||||
ISSN: | 0304-3975 | ||||
Official Date: | 6 June 1994 | ||||
Dates: |
|
||||
Volume: | 128 | ||||
Number: | 1-2 | ||||
Number of Pages: | 27 | ||||
Page Range: | pp. 99-125 | ||||
Publication Status: | Published |
Data sourced from Thomson Reuters' Web of Knowledge
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |