×

zbMATH — the first resource for mathematics

Shield synthesis. (English) Zbl 1386.68101
Summary: Shield synthesis is an approach to enforce safety properties at runtime. A shield monitors the system and corrects any erroneous output values instantaneously. The shield deviates from the given outputs as little as it can and recovers to hand back control to the system as soon as possible. In the first part of this paper, we consider shield synthesis for reactive hardware systems. First, we define a general framework for solving the shield synthesis problem. Second, we discuss two concrete shield synthesis methods that automatically construct shields from a set of safety properties: (1) k-stabilizing shields, which guarantee recovery in a finite time. (2) Admissible shields, which attempt to work with the system to recover as soon as possible. Next, we discuss an extension of \(k\)-stabilizing and admissible shields, where erroneous output values of the reactive system are corrected while liveness properties of the system are preserved. Finally, we give experimental results for both synthesis methods. In the second part of the paper, we consider shielding a human operator instead of shielding a reactive system: the outputs to be corrected are not initiated by a system but by a human operator who works with an autonomous system. The challenge here lies in giving simple and intuitive explanations to the human for any interferences of the shield. We present results involving mission planning for unmanned aerial vehicles.
Reviewer: Reviewer (Berlin)
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
ABC
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] LTL Specification Patterns. http://patterns.projects.cis.ksu.edu/documentation/patterns/ltl.shtml · Zbl 0575.68030
[2] Alpern, B; Schneider, FB, Defining liveness, Inf Process Lett, 21, 181-185, (1985) · Zbl 0575.68030
[3] Bernet, J; Janin, D; Walukiewicz, I, Permissive strategies: from parity games to safety games, ITA, 36, 261-275, (2002) · Zbl 1090.91514
[4] Bloem, R; Chatterjee, K; Greimel, K; Henzinger, TA; Hofferek, G; Jobstmann, B; Könighofer, B; Könighofer, R, Synthesizing robust systems, Acta Inf, 51, 193-220, (2014) · Zbl 1302.93079
[5] Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B (2010) Robustness in the presence of liveness. In: Proceedings of computer aided verification, 22nd international conference, CAV 2010, Edinburgh, 5-19 July 2010, pp 410-424
[6] Bloem R, Ehlers E, Könighofer R (2015) Cooperative reactive synthesis. In: ATVA, LNCS, vol. 9364. Springer, pp 394-410. doi:10.1007/978-3-319-24953-7 · Zbl 06527565
[7] Bloem, R; Jobstmann, B; Piterman, N; Pnueli, A; Sa’ar, Y, Synthesis of reactive(1) designs, J Comput Syst Sci, 78, 911-938, (2012) · Zbl 1247.68050
[8] Bloem R, Könighofer B, Könighofer R, Wang C (2015) Shield synthesis: runtime enforcement for reactive systems. In: Tools and algorithms for the construction and analysis of systems—21st international conference, TACAS 2015, London, 11-18 Apr 2015, LNCS, vol. 9035. Springer, pp 533-548
[9] Brayton RK, Mishchenko A (2010) ABC: an academic industrial-strength verification tool. In: CAV, LNCS, vol 6174, Springer, pp 24-40
[10] Bryant, RE, Graph-based algorithms for Boolean function manipulation, IEEE Trans Comput, 35, 677-691, (1986) · Zbl 0593.94022
[11] Chao, H; Cao, Y; Chen, Y, Autopilots for small unmanned aerial vehicles: a survey, Int J Control Autom Syst, 8, 36-44, (2010)
[12] Cimatti A, Roveri M, Schuppan V, Tchaltsev A (2008) Diagnostic information for realizability. In: Proceedings of verification, model checking, and abstract interpretation, 9th international conference, VMCAI 2008, San Francisco, 7-9 Jan 2008, pp 52-67 · Zbl 1138.68442
[13] Dalamagkidis K, Valavanis KP, Piegl LA (2011) On integrating unmanned aircraft systems into the national airspace system: issues, challenges, operational restrictions, certification, and recommendations, vol 54. Springer, Berlin
[14] Donmez, B; Nehme, C; Cummings, ML, Modeling workload impact in multiple unmanned vehicle supervisory control, IEEE Trans Syst Man Cybern A Syst Hum, 40, 1180-1190, (2010)
[15] Duquette M (2009) Effects-level models for UAV simulation. In: AIAA modeling and simulation technologies conference
[16] Dwyer MB, Avrunin GS, Corbett JC (1999) Patterns in property specifications for finite-state verification. In: ICSE, ACM, pp 411-420
[17] Ehlers R, Könighofer R, Bloem R (2015) Synthesizing cooperative reactive mission plans. In: 2015 IEEE/RSJ international conference on intelligent robots and systems, IROS 2015, Hamburg, 2015, IEEE, pp 3478-3485 · Zbl 1247.68050
[18] Ehlers R, Topcu U (2014) Resilience to intermittent assumption violations in reactive synthesis. In: 17th international conference on hybrid systems: computation and control, HSCC’14, Berlin, 15-17 Apr 2014, ACM, pp 203-212. doi:10.1145/2562059.2562128 · Zbl 1361.68146
[19] Faella M (2009) Admissible strategies in infinite games over graphs. In: Mathematical foundations of computer science 2009, 34th international symposium, MFCS 2009, Novy Smokovec, 2009, LNCS, vol. 5734. Springer, pp 307-318 · Zbl 1250.68187
[20] Falcone, Y; Fernandez, J; Mounier, L, What can you verify and enforce at runtime?, STTT, 14, 349-382, (2012)
[21] Feng L, Wiltsche C, Humphrey L, Topcu U (2016) Synthesis of human-in-the-loop control protocols for autonomous systems. In: IEEE/RSJ international conference on intelligent robots and systems (IROS) · Zbl 1302.93079
[22] Humphrey L, Könighofer B, Könighofer R, Topcu U (2016) Synthesis of admissible shields. In: Proceedings of hardware and software: verification and testing—12th international haifa verification conference, HVC 2016, Haifa, 14-17 Nov 2016, pp 134-151 · Zbl 0904.90057
[23] Könighofer, R; Hofferek, G; Bloem, R, Debugging formal specifications: a practical approach using model-based diagnosis and counterstrategies, STTT, 15, 563-583, (2013)
[24] Leucker, M; Schallhart, S, A brief account of runtime verification, J Log Algebr Program, 78, 293-303, (2009) · Zbl 1192.68433
[25] Li W, Sadigh D, Sastry S, Seshia S (2014) Synthesis for human-in-the-loop control systems. In: Proceedings of tools and algorithms for the construction and analysis of systems—20th international conference, TACAS 2014, Grenoble, 5-13 Apr 2014, LNCS, vol. 8413. Springer, pp 470-484 · Zbl 1154.68510
[26] Liffiton, MH; Sakallah, KA, Algorithms for computing minimal unsatisfiable subsets of constraints, J Autom Reason, 40, 1-33, (2008) · Zbl 1154.68510
[27] Loh, R; Bian, Y; Roe, T, UAVs in civil airspace: safety requirements, IEEE Aerosp Electr Syst Mag, 24, 5-17, (2009)
[28] Lygeros, J; Godbole, DN; Sastry, S, Verified hybrid controllers for automated vehicles, IEEE Trans Autom Control, 43, 522-539, (1996) · Zbl 0904.90057
[29] Mancini T, Mari F, Massini A, Melatti I, Tronci E (2014) Anytime system level verification via random exhaustive hardware in the loop simulation. In: 17th Euromicro conference on digital system design (DSD), 2014, pp 236-245
[30] Mazala R (2001) Infinite games. In: Grädel E, Thomas W, Wilke T (eds) Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001]. Lecture Notes in Computer Science, vol 2500, pp 23-42. Springer. doi:10.1007/3-540-36387-4_2 · Zbl 0575.68030
[31] Piterman N, Pnueli A (2006) Faster solutions of Rabin and Streett games. In: 21st symposium on logic in computer science, IEEE press, pp 275-284
[32] Pnueli A (1977) The temporal logic of programs. In: 18th annual symposium on foundations of computer science, Providence, 31 Oct-1 Nov 1977, pp 46-57
[33] Pnueli A, Rosner R (1989) Automata, languages and programming. In: Proceedings of 16th international colloquium Stresa, 11-15 July 1989, chap. On the synthesis of an asynchronous reactive module, Springer, Berlin, Heidelberg, pp 652-671
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.