Browse Prior Art Database

Verification of Ada Tasking Programs Using Symbolic Execution Part II: General Safety Properties

IP.com Disclosure Number: IPCOM000128372D
Original Publication Date: 1987-Dec-31
Included in the Prior Art Database: 2005-Sep-15
Document File: 20 page(s) / 58K

Publishing Venue

Software Patent Institute

Related People

Laura K. Dillon: AUTHOR [+3]

Abstract

General safety properties provide a more appropriate notion of correctness for con-current programs than partial correctness. This paper shows how a symbolic execution-based approach for verifying partial correctness of Ada tasking programs is used for verifying more general safety properties as well. Specific safety properties that are considered include mutual exclusion, freedom from deadlock and absence of communi-cation failure. The techniques are illustrated on a pedagogical solution to the readers and writers problem. The symbolic execution approach described below will serve as a basis for automating the verification of general safety properties of Ada tasking programs.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 7% of the total text.

Page 1 of 20

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

Verification of Ada Tasking Programs Using Symbolic Execution Part II: General Safety Properties

Laura K. Dillon Department of Computer Science

i April 1988

Abstract

General safety properties provide a more appropriate notion of correctness for con-current programs than partial correctness. This paper shows how a symbolic execution-based approach for verifying partial correctness of Ada tasking programs is used for verifying more general safety properties as well. Specific safety properties that are considered include mutual exclusion, freedom from deadlock and absence of communi-cation failure. The techniques are illustrated on a pedagogical solution to the readers and writers problem. The symbolic execution approach described below will serve as a basis for automating the verification of general safety properties of Ada tasking programs.

1 Introduction

Partial correctness [101 is a natural criterion for sequential programs. A sequential program is typically intended to perform some computation and then terminate. It's "behavior" can be characterized by the relation it computes between a set of initial states and a set of final states. It is natural, therefore, to consider a sequential program correct if assertions about

*This work supported in part by the National Science Foundation grant CCR a (desired) relation between initial and final states can be proved valid for the relation the program computes.1

For a concurrent program, however, intermediate program states, such as when several processes are contending for access to a shaxed resource, may also be of interest. In fact, concurrent programs that provide a continuing service to the environment may be designed to never terminate.

The concept of safety was introduced to provide a more useful notion of correctness for concurrent programs. Informally, a safety property asserts that the program never enters an unacceptable state [141. Examples of safety properties include mutual exclusion (the program never enters a state in which two processes are within critical sections simulta-neously), absence of deadlock (the program never enters a state in which all processes are either blocked or terminated and at least one process is blocked), and partial correct-ness (the program never enters a state in which all processes are terminated and the exit assertion is not satisfied)-

A symbolic execution-based approach for verifying partial correctness of Ada tasking programs is presented in (6]. The strength of this approach is that tasks are symbolically executed and verified independently, and then checked for cooperation where interference can occur. This reduces the combinatorial problems inherent in techniques that rely on executing a tasking

University of California at Santa Barbara Page 1 Dec 31, 1987

Page 2 of 20

Verification of Ada Tasking Programs Using Symbolic Execution Part II: General Safety Properties

program...