Abstract
Autonomous systems operating in the vicinity of humans are critical in that they potentially harm humans. As the complexity of autonomous system software makes the zero-fault objective hardly attainable, we adopt a fault-tolerance approach. We consider a separate safety channel, called a monitor, that is able to partially observe the system and to trigger safety-ensuring actuations. A systematic process for specifying a safety monitor is presented. Hazards are formally modeled, based on a risk analysis of the monitored system. A model-checker is used to synthesize monitor behavior rules that ensure the safety of the monitored system. Potentially excessive limitation of system functionality due to presence of the safety monitor is addressed through the notion of permissiveness. Tools have been developed to assist the process.
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
Mekki-Mokhtar, A., Blanquart, J.P., Guiochet, J., Powell, D., Roy, M.: Safety trigger conditions for critical autonomous systems. In: 18th Pacific Rim Int’l Symp. on Dependable Computing (PRDC), pp. 61–69. IEEE (2012)
ISO/IEC 61508-7: Functional safety of electrical / electronic / programmable electronic safety-related systems - part 7: Overview of techniques and measures (2010)
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: Nusmv 2: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)
Dufossé, F., Machin, M., Guiochet, J., Powell, D., Roy, M., Waeselynck, H.: Safety strategy synthesis: Game theory versus model-checking. LAAS-CNRS, Tech. Rep. 14059 (2014)
Saphari project, http://www.saphari.eu
Rushby, J.: Kernels for safety. Safe and Secure Computing Systems, 210–220 (1989)
Leucker, M., Schallhart, C.: A brief account of runtime verification. Journal of Logic and Algebraic Programming 78(5), 293–303 (2009)
Pike, L., Niller, S., Wegmann, N.: Runtime verification for ultra-critical systems. In: 2nd Int’l Conf. on Runtime Verification, San Francisco, California, USA (2011)
Wonham, W.M.: Supervisory control of discrete event systems (2005)
Fotoohi, L., Gräser, A.: A supervisory control approach for safe behavior of service robot case study: Friend. In: Proceedings of the 2010 ACM Symposium on Applied Computing, pp. 1305–1306. ACM (2010)
Woodman, R., Winfield, A.F., Harper, C., Fraser, M.: Building safer robots: Safety driven control. Int’l J. Robotics Research 31(13), 1603–1626 (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Machin, M., Dufossé, F., Blanquart, JP., Guiochet, J., Powell, D., Waeselynck, H. (2014). Specifying Safety Monitors for Autonomous Systems Using Model-Checking. In: Bondavalli, A., Di Giandomenico, F. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2014. Lecture Notes in Computer Science, vol 8666. Springer, Cham. https://doi.org/10.1007/978-3-319-10506-2_18
Download citation
DOI: https://doi.org/10.1007/978-3-319-10506-2_18
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10505-5
Online ISBN: 978-3-319-10506-2
eBook Packages: Computer ScienceComputer Science (R0)