UNSPECIFIED (1999) Specification and verification of fault-tolerance, timing, and scheduling. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 21 (1). pp. 46-89. ISSN 0164-0925

Full text not available from this repository.

Abstract

Fault-tolerance and timing have often been considered to be implementation issues of a program, quite distinct from the functional safety and liveness properties. Recent work has shown how these non-functional and functional properties can be verified in a similar way. However, the more practical question of determining whether a real-time program will meet its deadlines, i.e., showing that there is a feasible schedule, is usually done using scheduling theory, quite separately from the verification of other properties of the program. This makes it hard to use the results of scheduling analysis in the design, or redesign, of fault-tolerant and real-time programs. This article shows how fault-tolerance, timing, and schedulability can be specified and verified using a single notation and model. This allows a unified view to be taken of the functional and nonfunctional properties of programs and a simple transformational method to be used to combine these properties. It also permits results from scheduling theory to be interpreted and used within a formal proof framework. The notation and model are illustrated using a simple example.

Item Type:	Journal Article
Subjects:	Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software
Journal or Publication Title:	ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS
Publisher:	ASSOC COMPUTING MACHINERY
ISSN:	0164-0925
Date:	January 1999
Volume:	21
Number:	1
Number of Pages:	44
Page Range:	pp. 46-89
Publication Status:	Published
URI:	http://wrap.warwick.ac.uk/id/eprint/14366

Data sourced from Thomson Reuters' Web of Knowledge

Request changes to a record

Actions (login required)

View Item