Abstract :
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.
Keywords :
formal specification; security of data; systems analysis; formal method; predicate logic; safety specification; standard syntactic rules; such-and-such conditions; system safety; Aerospace safety; Cities and towns; Information analysis; Information technology; Large-scale systems; Logic; Road safety; Software tools; Systems engineering and theory; Technological innovation;
