ASE2 CARD CATALOG ENTRY

Instructions:

• Scroll forward and backward through this Card Catalog Entry to view it.
• Strike the PRINT button on your browser to print this Card Catalog Entry.
• Go to the FILE SPECS section of this Card Catalog Entry to find out where the associated directories and files are. If they are on this Website, you can transfer to them by clicking on the indicated hyperlinks. Note: the FILE SPECS hyperlink in this bullet will take you directly to the FILE SPECS section.
• Use the FIND command of your browser to search this Card Catalog Entry.
• Click here to go to the Card Catalog Taxonomy.
• Click here to go to the Card Catalog Index. Warning: the index file is large, so this may take a while on slower systems.
• Click here to go to the Title Page.

---

ASSET OVERVIEW

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

---

CLASSIFICATION

KEYWORDS

Penelope
Software Measurement
Measurement, Software
Tasking

INDEX

Hoover, Douglas
Unisys

DEPENDENCIES

None

SEE ALSO

SHORT DESCRIPTION

A method for Penelope to support verification of Ada tasks

TAXONOMY

Documents

Software Verification

Penelope

Verifying Ada Tasking

---

FILE LISTING

FILE SPECS

Click here to enter Asset Directory/transfer Asset File(s): ../../ase02_01/docs/penelope/penverfy

DIRECTORY DISPLAY

Follow path to see directory

---

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:

• 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.
• Program annotations should contribute to the understanding of the program by stating properties that must hold at that point of the computation.
• 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.
• The compositionality should be syntax directed, that is, the verification must break up along the lines of Ada tasks, subprograms, and packages.
• 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.
• 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.
• 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:

• local vs. inter-task properties; and
• 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.

---

ASE CARD CATALOG ENTRY NAVIGATION

• Go to Title Page
• Go to Taxonomy
• Go to Index (warning: the index file is large, so this may take a while on slower systems)
• Go to Top of this Page

Powered by the Generic Web-Based Reuse Library (GWRL)