Formalizing Probabilistic Safety Claims

8 years 1 months ago
Formalizing Probabilistic Safety Claims
A safety claim for a system is a statement that the system, which is subject to hazardous conditions, satisfies a given set of properties. Following work by John Rushby and Bev Littlewood, this paper presents a mathematical framework that can be used to state and formally prove probabilistic safety claims. It also enables hazardous conditions, their uncertainties, and their interactions to be integrated into the safety claim. This framework provides a formal description of the probabilistic composition of an arbitrary number of hazardous conditions and their effects on system behavior. An example is given of a probabilistic safety claim for a conflict detection algorithm for aircraft in a 2D airspace. The motivation for developing this mathematical framework is that it can be used in an automated theorem prover to formally verify safety claims.
Heber Herencia-Zapana, George Hagen, Anthony Narka
Added 14 May 2011
Updated 14 May 2011
Type Journal
Year 2011
Where NFM
Authors Heber Herencia-Zapana, George Hagen, Anthony Narkawicz
Comments (0)