Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Butler, R.: Formalization of the integral calculus in the PVS theorem prover. Journal of Formalized Reasoning 2(1) (2009)
Chung, W.W., Staab, R.: A 1090 extended squitter automatic dependent surveillance broadcast (ADS-B) reception model for air-traffic-management simulations. In: AIAA Modeling and Simulation Technologies Conference and Exhibit (2006)
Herencia-Zapana, H., Jeannin, J.B., Muñoz, C.: Formal verification of safety buffers for state-based conflict detection and resolution. In: Proceedings of 27th International Congress of the Aeronautical Sciences, ICAS 2010, Nice, France (2010)
Holloway, C.M.: Safety case notations: alternatives for the non-graphically inclined? In: 3rd IET International Conference on System Safety (2008)
Littlewood, B., Rushby, J.: Reasoning about the realiability of diverse two channel systems in which one channel is possibly perfect. In: Tech report SRI-CSL-09-02 (2010)
NASA Langley Formal Methods Team: Airborne coordinated conflict resolution and detection (2010), http://shemesh.larc.nasa.gov/people/cam/ACCoRD/
Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992), http://www.csl.sri.com/papers/cade92-pvs/
Minimum aviation system performance standards for automatic dependent surveillance broadcast (ADS-B). DO-242A, RTCA (June 2002), section 2.1.2.12–2.1.2.15
Rushby, J.: Formalism in safety cases. In: Proceedings of the Eighteenth Safety-critical Systems Symposium (2010)
Shiryaev, A.N.: Probability. Springer, Heidelberg (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Herencia-Zapana, H., Hagen, G., Narkawicz, A. (2011). Formalizing Probabilistic Safety Claims. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds) NASA Formal Methods. NFM 2011. Lecture Notes in Computer Science, vol 6617. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20398-5_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-20398-5_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-20397-8
Online ISBN: 978-3-642-20398-5
eBook Packages: Computer ScienceComputer Science (R0)