Accession Number : ADA187556

Title :   Decomposing Properties into Safety and Liveness Using Predicate Logic.

Descriptive Note : Interim rept.,

Corporate Author : CORNELL UNIV ITHACA NY DEPT OF COMPUTER SCIENCE

Personal Author(s) : Schneider, Fred B

PDF Url : ADA187556

Report Date : 05 Oct 1987

Pagination or Media Count : 6

Abstract : Two classes of properties are of particular interest when considering programs: safety properties and liveness properties. Informally, a safety property stipulates that 'bad things' do not happen during execution of a program and a liveness property stipulates that 'good things' do happen (eventually). Distinguishing between safety and liveness properties is useful because knowing whether a property is safety or liveness helps when deciding how to prove that the property holds for a program. A new proof is given that every property can be expressed as a conjunction of safety and liveness properties. The proof is in terms of first-order predicate logic. Keywords: Concurrency; Semantics.

Descriptors :   *COMPUTER LOGIC, SAFETY, SEMANTICS, COMPUTER PROGRAMMING, SPECIFICATIONS

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE