ASE2 CARD CATALOG ENTRY
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:
Properties of concurrent programs can be partitioned in two ways:
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.
STARS-AC-A023/003/00 1 June 94 Initial release to the PAL
Approved for public release; Distribution unlimited
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.
Powered by the Generic Web-Based Reuse Library (GWRL)