Exceptions for Dependability

Exceptions for Dependability

Emil Sekerinski (McMaster University, Canada)
DOI: 10.4018/978-1-60960-747-0.ch002
OnDemand PDF Download:
$30.00
List Price: $37.50

Abstract

Exception handling allows (1) a program to be structured such that the original design is preserved in presence of possibly failing components; (2) rare or undesired cases to be treated in an unobtrusive manner; and (3) imperfections to be handled systematically. This chapter develops a theory of exception handling with try-catch statements, and demonstrates its use in the design of dependable systems by giving a formal account of the patterns of masking, propagating, flagging, rollback, degraded service, recovery block, repeated attempts, and conditional retry. The theory is based on weakest exceptional preconditions, which are used for both defining statements and proofs. Proof outlines are introduced and used to establish the correctness of the patterns.
Chapter Preview
Top

Introduction

A program may fail to perform its intended task for three reasons:

  • The specification may be in error. It may not capture the user's requirements, or the requirements are inconsistent or incomplete.

  • There may be errors in the design. There errors arise from incorrect arguments that the program meets its specification (e.g. overlooking a case), or from idealized or incorrect assumptions about the programming language, libraries, and the hardware (e.g. a sufficiently large integer range and sufficiently available memory).

  • The underlying software or hardware may fail, (e.g. operating system, disk, memory, or network).

Some failures are always detected at run-time by the underlying (virtual) machine (e.g. indexing an array out of bounds, allocating memory when none is available, or reading a file beyond its end). Other failures may be detected by programmer-added checks (e.g. checking the range of parameters of a procedure). Finally, some failures are too difficult to detect by any means.

The possibility of a failure is present even when the best effort is put forth to design error-free programs. The question then arises how programs should respond to detected failures. Suppose that a problem calls for the sequential composition of four statements,S1 ; S2 ; S3 ; S4and statements S1 and S3 may fail in a detectable way. In case they do fail, the sequence should be abandoned and statement T should be executed instead. In the a priory scheme, we add a test before running S1 and S3. In the a posteriori scheme, we run S1 and S3 and test if they were successful (see Box 1).

Box 1.
if S1possible thenS1 ;
S1 ;if S1successful then
S2 ;S2 ;
if S3possible thenS3 ;
S3 ;if S3successful then
S4S4
elseelse
TT
elseelse
TT

Complete Chapter List

Search this Book:
Reset