A foundation for system safety using predicate logic

This paper presents a formal method based on standard concepts from mathematical logic, for the analysis of system properties, particularly safety. Informally, a safety proposition is a statement, ldquoThis system is saferdquo, and a safety predicate is a statement, ldquoThis system is safe under such-and-such conditionsrdquo. The standard syntactic rules for predicate logic apply with safety predicates, though their semantics now derive from the context of systems theory and systems engineering. The main insight is that the description of a safety predicate by its quantifier, variable, range, and term can be used as a safety specification for a system on a large scale as well, and that substitutions of expressions for variables in a safety predicate can be used as a tool of refinement.