Browse Prior Art Database

Verification of Ada Tasking Programs Using Symbolic Execution Part I: Partial Correctness

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

Publishing Venue

Software Patent Institute

Related People

Laura K. Dillon: AUTHOR [+3]

Abstract

In previous work on symbolic execution of concurrent programs, concurrency is modeled by interleaving the execution of sequential processes. This approach suffers from well-known combinatorial problems, making it unsuitable for formal verifica-tion. This paper describes an alternate approach. Symbolic execution is based on an axiomatic proof system for concurrent programs, in which processes are verified separately and then checked for cooperation. Two Hoare-style proof systems for Ada tasking programs, which differ in their formulation of cooperation, were considered. Using these proof systems, a computationally tractable approach to symbolic execution for a tasking subset of Ada is obtained. This isolation approach allows the verification of general safety properties. The partial correctness proof is described in this paper. A companion paper describes the proof of more general safety properties [5]. We intend to use the isolation approach for automating the verification 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 18

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

Verification of Ada Tasking Programs Using Symbolic Execution Part I: Partial Correctness

Laura K. Dillon

Department of Computer Science

April 1988

Abstract

In previous work on symbolic execution of concurrent programs, concurrency is modeled by interleaving the execution of sequential processes. This approach suffers from well-known combinatorial problems, making it unsuitable for formal verifica-tion. This paper describes an alternate approach. Symbolic execution is based on an axiomatic proof system for concurrent programs, in which processes are verified separately and then checked for cooperation. Two Hoare-style proof systems for Ada tasking programs, which differ in their formulation of cooperation, were considered. Using these proof systems, a computationally tractable approach to symbolic execution for a tasking subset of Ada is obtained. This isolation approach allows the verification of general safety properties. The partial correctness proof is described in this paper. A companion paper describes the proof of more general safety properties [5]. We intend to use the isolation approach for automating the verification of Ada tasking programs.

I Introduction

The research on symbolic execution of Ada tasking programs described in this paper is motivated by the need to provide automated support for the verification of concurrent programs. Hantler and King [91 show how to use symbolic execution for automating the verification of sequential programs. The question addressed below is how to adapt this approach for use with concurrent programs.

*This work supported in part by the National Science Foundation grant CCR n earlier work on symbolic execution of concurrent programs [3,13,171, concurrency is modeled by interleaving the execution of sequential processes (i.e., tasks). Theoretically, all possible interleavings of "atomic" actions should be considered. In practice, processes are usually partitioned into sequential segments, which are interleaved to simulate all possible execution sequences. This approach helps reduce the combinatorial problems inherent in the interleaving approach. The number of symbolic execution paths grows exponentially with the number of processes in the system, and the finer the interleaving, the worse the combinatorial explosion. Preliminary experience indicates, however, that it may not be possible to reduce the combinatorial growth of "program paths" to the point where the interleaving approach will be of much practical value. Symbolic execution models based on the interleaving approach appear to be better suited for symbolic testing, for which it is not necessary to explore all program paths, than verification 16].

The isolation approach described in this paper is based on an axiomatic proof system for Ada tasking programs. Assertions specify the intended behavior of each task. The proof system

Yale University Page 1 Dec 31, 1987

Pag...