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