Specifying Safety Monitors for Autonomous Systems Using Model-Checking

详细信息    查看全文

• 作者：Mathilde Machin (17) (18)
  Fanny Dufoss茅 (17) (18)
  Jean-Paul Blanquart (19)
  J茅r茅mie Guiochet (17) (18)
  David Powell (17) (18)
  H茅l猫ne Waeselynck (17) (18)
  
• 关键词：Safety Monitoring ; Safety Rules ; Autonomous Robotics
• 刊名：Lecture Notes in Computer Science
• 出版年：2014
• 出版时间：2014
• 年：2014
• 卷：8666
• 期：1
• 页码：262-277
• 全文大小：657 KB
• 参考文献：1. Mekki-Mokhtar, A., Blanquart, J.P., Guiochet, J., Powell, D., Roy, M.: Safety trigger conditions for critical autonomous systems. In: 18th Pacific Rim Int鈥檒 Symp. on Dependable Computing (PRDC), pp. 61鈥?9. IEEE (2012)
  2. ISO/IEC 61508-7: Functional safety of electrical / electronic / programmable electronic safety-related systems - part 7: Overview of techniques and measures (2010)
  3. 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鈥?64. Springer, Heidelberg (2002) href="http://dx.doi.org/10.1007/3-540-45657-0_29" target="_blank" title="It opens in new window">CrossRef
  4. 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)
  5. Saphari project, href="http://www.saphari.eu" class="a-plus-plus"> hasis fontcategory-non-proportional">http://www.saphari.eu
  6. Rushby, J.: Kernels for safety. Safe and Secure Computing Systems, 210鈥?20 (1989)
  7. Leucker, M., Schallhart, C.: A brief account of runtime verification. Journal of Logic and Algebraic Programming聽78(5), 293鈥?03 (2009) href="http://dx.doi.org/10.1016/j.jlap.2008.08.004" target="_blank" title="It opens in new window">CrossRef
  8. Pike, L., Niller, S., Wegmann, N.: Runtime verification for ultra-critical systems. In: 2nd Int鈥檒 Conf. on Runtime Verification, San Francisco, California, USA (2011)
  9. Wonham, W.M.: Supervisory control of discrete event systems (2005)
  10. 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鈥?306. ACM (2010)
  11. Woodman, R., Winfield, A.F., Harper, C., Fraser, M.: Building safer robots: Safety driven control. Int鈥檒 J. Robotics Research聽31(13), 1603鈥?626 (2012) href="http://dx.doi.org/10.1177/0278364912459665" target="_blank" title="It opens in new window">CrossRef
  
• 作者单位：Mathilde Machin (17) (18)
  Fanny Dufoss茅 (17) (18)
  Jean-Paul Blanquart (19)
  J茅r茅mie Guiochet (17) (18)
  David Powell (17) (18)
  H茅l猫ne Waeselynck (17) (18)
  
  17. CNRS, LAAS, 7 avenue du colonel Roche, F-31400, Toulouse, France
  18. Univ de Toulouse, LAAS, F-31400, Toulouse, France
  19. Airbus Defence and Space, 31 rue des cosmonautes, 31402, Toulouse, France
  
• ISSN：1611-3349

文摘

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.