Abstract
This paper describes algorithms to compute a counterexample when compositional nonblocking verification determines that a discrete event system is blocking. Counterexamples are an important feature of model checking that explains the cause of a detected problem, greatly helping users to understand and fix faults. In compositional verification, counterexamples are difficult to compute due to the large state space and the loss of information after abstraction. The paper explains the difficulties and proposes solutions, and experimental results show that counterexamples can be computed successfully for several industrial-scale systems.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Åkesson K, Fabian M, Flordal H, Malik R (2006) Supremica—an integrated environment for verification, synthesis and simulation of discrete event systems. In: 8th Int. workshop on discrete event systems, WODES,’06. IEEE, pp 384–385, DOI https://doi.org/10.1109/WODES.2006.382401
Bérard B, Bidoit M, Finkel A, Laroussinie F, Petit A, Petrucci L, Schnoebelen P (2001) Systems and software verification. Springer
Cassandras CG, Lafortune S (2008) Introduction to discrete event systems, 2nd edn. Springer Science & Business Media, New York
Clarke EM, Long DE, McMillan KL (1989) Compositional model checking. In: 4th Annual symp. logic in computer science, pp 353–362, DOI https://doi.org/10.1109/LICS.1989.39190
Dams D, Grumberg O, Gerth R (1994) Abstract interpretation of reactive systems: abstractions preserving ∀CTL∗, ∃CTL∗ and CTL∗. In: Olderog ER (ed) IFIP WG2.1/WG2.2/WG2.3 working conf. programming concepts, methods and calculi (PROCOMET), IFIP transactions. Elsevier, pp 573–592
De Nicola R, Hennessy MCB (1984) Testing equivalences for processes. Theoret Comput Sci 34(1–2):83–133. https://doi.org/10.1016/0304-3975(84)90113-0
Flordal H, Malik R (2009) Compositional verification in supervisory control. SIAM J Control Optim 48(3):1914–1938. https://doi.org/10.1137/070695526
Graf S, Steffen B (1990) Compositional minimization of finite state systems. In: 1990 workshop on computer- aided verification, LNCS, vol 531. Springer, pp 186–196, DOI https://doi.org/10.1007/BFb0023732
Hart PE, Nilsson NJ, Raphael B (1968) A formal basis for the heuristic determination of minimum cost paths. IEEE Trans Syst Sci Cybern 4(2):100–107. https://doi.org/10.1109/TSSC.1968.300136
Hoare CAR (1985) Communicating sequential processes. Prentice-Hall
Hopcroft JE, Motwani R, Ullman JD (2001) Introduction to automata theory, languages, and computation. Addison-Wesley, Boston
Huth M, Ryan M (2004) Logic in computer science. Cambridge University Press, Cambridge
Lindsey J (2012) The set of certain conflicts. Honours project report. University of Waikato, Dept. of Computer Science
Malik R (2010) The language of certain conflicts of a nondeterministic process. Working Paper 05/2010, Dept. of Computer Science, University of Waikato, Hamilton, New Zealand. http://hdl.handle.net/10289/4108
Malik R (2016) Programming a fast explicit conflict checker. In: 13th Int. workshop on discrete event systems, WODES,’16. IEEE, pp 464–469, DOI https://doi.org/10.1109/WODES.2016.7497885
Malik R, Leduc R (2013) Compositional nonblocking verification using generalised nonblocking abstractions. IEEE Trans Autom Control 58(8):1–13. https://doi.org/10.1109/TAC.2013.2248255
Malik R, Ware S (2018) Counterexample computation in compositional nonblocking verification. IFAC PapersOnLine 51(7):230–235. https://doi.org/10.1016/j.ifacol.2018.06.334
Malik R, Streader D, Reeves S (2006) Conflicts and fair testing. Int J Found Comput Sci 17(4):797–813. https://doi.org/10.1142/S012905410600411X
Milner R (1989) Communication and concurrency. Series in computer science. Prentice-Hall
Pena PN, Cury JER, Lafortune S (2009) Verification of nonconflict of supervisors using abstractions. IEEE Trans Autom Control 54(12):2803–2815. https://doi.org/10.1109/TAC.2009.2031730
Pilbrow C, Malik R (2015) An algorithm for compositional nonblocking verification using special events. Sci Comput Programming 113(2):119–148. https://doi.org/10.1016/j.scico.2015.05.010
Ramadge PJG, Wonham WM (1989) The control of discrete event systems. Proc IEEE 77(1):81–98. https://doi.org/10.1109/5.21072
Su R, van Schuppen JH, Rooda JE, Hofkamp AT (2010) Nonconflict check by using sequential automaton abstractions based on weak observation equivalence. Automatica 46(6):968–978. https://doi.org/10.1016/j.automatica.2010.02.025
Valmari A (1996) Compositionality in state space verification methods. In: 18th Int. conf. application and theory of Petri nets, LNCS, vol 1091. Springer, pp 29–56, DOI https://doi.org/10.1007/3-540-61363-3_3
Ware S, Malik R (2008) The use of language projection for compositional verification of discrete event systems. In: 9th Int. workshop on discrete event systems, WODES,’08. IEEE, pp 322–327, DOI https://doi.org/10.1109/WODES.2008.4605966
Ware S, Malik R (2012) Conflict-preserving abstraction of discrete event systems using annotated automata. Discrete Event Dyn Syst 22(4):451–477. https://doi.org/10.1007/s10626-012-0133-3
Ware S, Malik R (2013) Compositional verification of the generalized nonblocking property using abstraction and canonical automata. Int J Found Comput Sci 24(8):1183–1208. https://doi.org/10.1142/S0129054113500287
Ware S, Malik R (2014) An algorithm to test the conflict preorder. Sci Comput Programming 89(A):23–40. https://doi.org/10.1016/j.scico.2013.09.006
Wirth N (1986) Algorithms and data structures. Prentice-Hall
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher’s note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
This article belongs to the Topical Collection: Applications-2020
Guest Editors: Francesco Basile, Jan Komenda, and Christoforos Hadjicostis
Rights and permissions
About this article
Cite this article
Malik, R., Ware, S. On the computation of counterexamples in compositional nonblocking verification. Discrete Event Dyn Syst 30, 301–334 (2020). https://doi.org/10.1007/s10626-019-00305-w
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10626-019-00305-w