Specification and verification of fault-tolerance, timing, and scheduling
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-0925Full text not available from this repository.
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|
|Number of Pages:||44|
|Page Range:||pp. 46-89|
Actions (login required)