PAL CARD CATALOG ENTRY

SHORT DESCRIPTION

A method for Penelope to support verification of Ada tasks


MOVEMENT WITHIN THE PAL CARD CATALOG
Move to top-level taxonomy
Move to keyword list

ASSET PROFILE

UNIT NAME
PENVERFY
VERSION
STARS-AC-A023/003/00, 26-FEB-94
ORIGIN
ASSET
REVIEW CODE
OK
INET ADDRESS
librarian@source.asset.com
AUTHOR
Douglas Hoover
UNISYS
RIGHTS
Approved for public release; distribution unlimited
COPYRIGHT
1994 UNISYS
LOCATION
ASSET
PAL

FILE LISTING

Directory Display


languages/ada/docs/penelope/penverfy:
  File Name                 Size
  ---------                 ----
  README                   2,851
  penverfy.zip            89,276


Totals
  ==============  ==============
    2 Files               92,127

ABSTRACT

Methodology for Verifying Ada Tasking with Penelope

     This paper sketches a method for Penelope to support verification
of Ada programs that use tasking.  In developing this method, our aims
have been the following:

   1.  The method must be compatible with Penelope.  That is, program
       annotations should be written in classical logic, and Penelope
       should generate verification conditions whose proof verifies
       the program.

   2.  Program annotations should contribute to the understanding of the
       program by stating properties that must hold at that point of the
       computation.

   3.  The verification process must be compositional; we must be
       able to verify parts of the program separately and then put them
       together to obtain a verification of the whole without repeating
       the verification of the parts.

   4.  The compositionality should be syntax directed, that is, the
       verification must break up along the lines of Ada tasks,
       subprograms, and packages.

   5.  The method should support separation of concerns in the verification
       process.  For example, it should be possible to separately verify
       partial correctness, freedom from deadlock and liveness without
       much duplication of labor.

   6.  The method should support both data refinement and program
       refinement.  Whenever possible, verification of properties
       expressible at more abstract levels should be inherited by
       the implementation.

   7.  If no tasks or global variables shared by tasks are visible from
       a given subprogram or package, then verification in that
       subprogram or package should be carried on in the sequential
       style, even if there are tasks contained inside visible
       subprograms or packages.

     Properties of concurrent programs can be partitioned in two ways:

   o  local vs. inter-task properties; and
   o  safety vs. liveness properties.

     Local properties are those that can be regarded as properties of an
individual subprogram or task.  Inter-task properties are those that
describe the interactions of a group of tasks.  Safety properties state
that the program will always be in an acceptable state.  Liveness
properties state that some desired action will eventually be performed.
     Local safety properties are just partial correctness properties: 
we must show that each annotation in a task or subprogram holds whenever
it is reached. Local liveness properties are similar to proving
termination of a sequential program.  For example, one may want to prove
that the execution of an individual task or subprogram will reach
completion provided all the task entry or subprogram calls it makes
terminate, in case the task as a whole is not meant ever to reach
completion on its own.


REVISION HISTORY

STARS-AC-A023/003/00  1 June 94  Initial release to the PAL


RELEASE NOTICE

Approved for public release; Distribution unlimited


DISCLAIMER

This documentation is provided "AS IS" and without any expressed or
implied warranties whatsoever.  No warranties as to performance,
merchantability, or fitness for a particular purpose exist.

The user must assume the entire risk and liability of using this
document.  In no event shall any person or organization of people be
held responsible for any direct, indirect, consequential or
inconsequential damages or lost profits.