Your browser does not support JavaScript!
http://iet.metastore.ingenta.com
1887

access icon openaccess Verification using counterexample fragment based specification relaxation: case of modular/concurrent linear hybrid automata

This is an open access article published by the IET under the Creative Commons Attribution-NonCommercial-NoDerivs License (http://creativecommons.org/licenses/by-nc-nd/3.0/)
Received 19/12/2016, Accepted 08/06/2017, Revised 22/05/2017, Published 12/06/2017

We present LhaVrf, a symbolic verifier for the safety verification of concurrent LHA (Linear Hybrid Automaton). A concurrent LHA is composed of a set of LHAs that interact through shared variables and/or events. An LHA is first translated to a purely discrete linear transition system that preserves the reachability of discrete states. Its analysis can be conducted in the proposed counterexample fragment based specification relaxation (CEFSR) framework, where an invalid fragment of a counterexample is used to eliminate the entire set of counterexamples sharing the same fragment, by way of specification relaxation (as opposed to the traditional model refinement). For concurrent systems, we propose further enhancement towards scalability as follows. For each spurious counterexample, an unsatisfiable core (unsat-core) that makes the counterexample invalid, is identified and used for specification relaxation, thereby eliminating the entire set of spurious counterexamples sharing the same unsat-core in a single iteration. Our implementation of LhaVrf adopts the above key ideas, with capability of automatically translating the hybrid automata into discrete transition system, composing the concurrent model, and using satisfiability modulo theory solver for validating counterexamples and fast-searching for the unsat-core. The verifier is illustrated via an application to the Fischer mutual exclusion protocol.

Inspec keywords: formal verification; reachability analysis; computability; finite state machines; relaxation

Other keywords: symbolic verifier; purely discrete linear transition system; CEFSR framework; discrete state reachability; LhaVrf; Fischer mutual exclusion protocol; LHA; satisfiability modulo theory solver; counterexample fragment based specification relaxation; modular linear hybrid automata; concurrent linear hybrid automaton; unsatisfiable core; safety verification

Subjects: Formal methods; Automata theory; Combinatorial mathematics

References

    1. 1)
      • 8. Henzinger, T.A., Ho, P.S., Wong-Toi, H.: ‘HYTECH: a model checker for hybrid systems’. CAV, 1997.
    2. 2)
      • 20. Guernic, C.L., Girard, A.: ‘Reachability analysis of hybrid systems using support functions’. CAV, 2009.
    3. 3)
      • 34. Ren, H., Kumar, R.: ‘Step simulation/over approximation-based verification of nonlinear deterministic hybrid system with inputs’. Proc. 5th IFAC Conf. on Analysis and Design of Hybrid Systems (ADHS 12), October 2015.
    4. 4)
      • 17. Duggirala, P.S., Mitra, S., Viswanathan, M., et al: ‘C2E2: a verification tool for stateflow models’. TACAS, 2015.
    5. 5)
      • 12. Asarin, E., Dang, T., Maler, O.: ‘The d/dt tool for verification of hybrid systems’. CAV, 2002.
    6. 6)
      • 39. Frehse, G.: ‘PHAVer: algorithmic verification of hybrid systems past HyTech’. HSCC, 2005.
    7. 7)
      • 11. Cimatti, A., Griggio, A., Mover, S., et al: ‘HyComp: an SMT-based model checker for hybrid systems’. TACAS, 2015.
    8. 8)
      • 37. Jha, S.K., Krogh, B.H., Weimer, J.E., et al: ‘Reachability for linear hybrid automata using iterative relaxation abstraction’. HSCC, 2007.
    9. 9)
      • 24. Althoff, M., Frehse, G.: ‘Combining zonotopes and support functions for efficient reachability analysis of linear systems’. CDC, 2016.
    10. 10)
      • 23. Minopoli, S., Frehse, G.: ‘SL2SX translator: from simulink to SpaceEx models’. HSCC, 2016.
    11. 11)
      • 47. Morbé, G., Pigorsch, F., Scholl, C.: ‘Fully symbolic model checking for timed automata’. CAV, 2011.
    12. 12)
      • 3. Clarke, E.M., Grumberg, O., Jha, S., et al: ‘Counterexample-guided abstraction refinement’. CAV, London, UK, 2000, pp. 154–169.
    13. 13)
      • 7. Ren, H., Huang, J., Jiang, S., et al: ‘A new abstraction-refinement based verifier for modular linear hybrid automata and its implementation’. 2014 IEEE 11th Int. Conf. Networking, Sensing and Control (ICNSC), April 2014, pp. 30–35.
    14. 14)
      • 30. Chen, X., Ábrahám, E., Sankaranarayanan, S.: ‘Taylor model flowpipe construction for non-linear hybrid systems’. RTSS, 2012.
    15. 15)
      • 31. Chen, X., Ábrahám, E., Sankaranarayanan, S.: ‘Flow*: an analyzer for non-linear hybrid systems’. CAV, 2013.
    16. 16)
      • 33. Kapinski, J., Deshmukh, J.V., Sankaranarayanan, S., et al: ‘Simulation-guided Lyapunov analysis for hybrid dynamical systems’. HSCC, 2014.
    17. 17)
      • 26. Bak, S., Bogomolov, S., Johnson, T.T.: ‘HyST: a source transformation and translation tool for hybrid automaton models’. HSCC, Seattle, Washington, April 2015.
    18. 18)
      • 16. Duggirala, P.S., Potok, M., Mitra, S., et al: ‘C2E2: a tool for verifying annotated hybrid systems’. HSCC, 2015.
    19. 19)
      • 10. Frehse, G., Jha, S.K., Krogh, B.H.: ‘A counterexample-guided approach to parameter synthesis for linear hybrid automata’. HSCC, 2008.
    20. 20)
      • 1. Alur, R., Courcoubetis, C., Halbwachs, N., et al: ‘The algorithmic analysis of hybrid systems’, Theor. Comput. Sci., 1995, 138, pp. 3–34.
    21. 21)
      • 18. Fan, C., Mitra, S.: ‘Bounded verification with on-the-fly discrepancy computation’. ATVA, 2015.
    22. 22)
      • 21. Guernic, C.L., Girard, A.: ‘Reachability analysis of linear systems using support functions’, Nonlinear Anal., Hybrid Syst., 2010, 4, pp. 250–262.
    23. 23)
      • 45. Krishna, S.N., Trivedi, A.: ‘Hybrid automata for formal modeling and verification of cyber-physical systems’. CoRR, 2015.
    24. 24)
      • 9. Alur, R.: ‘Formal verification of hybrid systems’. EMSOFT, October 2011, pp. 273–278.
    25. 25)
      • 28. Berz, M., Makino, K.: ‘Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models’, Reliab. Comput., 1998, 4, pp. 361–369.
    26. 26)
      • 14. Chutinan, A., Krogh, B.H.: ‘Computational techniques for hybrid system verification’, IEEE Trans. Autom. Control, 2003, 48, pp. 64–75.
    27. 27)
      • 15. Chutinan, A., Krogh, B.H.: ‘Computing polyhedral approximations to flow pipes for dynamic systems’. 37th IEEE Conf. Decision Control, 1998.
    28. 28)
      • 27. Bak, S., Johnson, T.T.: ‘Periodically-scheduled controller analysis using hybrid systems reachability and continuization’. RTSS, San Antonio, Texas, December 2015.
    29. 29)
      • 19. Fan, C., Kapinski, J., Jin, X., et al: ‘Locally optimal reach set over-approximation for nonlinear systems’. EMSOFT, 2016.
    30. 30)
      • 25. Frehse, G., Bogomolov, S., Greitschus, M., et al: ‘Eliminating spurious transitions in reachability with support functions’. HSCC, 2015.
    31. 31)
      • 22. Frehse, G., Guernic, C.L., Donzé, A., et al: ‘SpaceEx: scalable verification of hybrid systems’. CAV, 2011.
    32. 32)
      • 42. Cimatti, A., Mover, S., Tonetta, S.: ‘SMT-based verification of hybrid systems’. AAAI, 2012.
    33. 33)
      • 44. Carloni, L.P., Passerone, R., Pinto, A., et al: ‘Languages and tools for hybrid systems design’, Found. Trends Electron. Design Autom., 2006, 1, pp. 1–193.
    34. 34)
      • 6. Kumar, R., Zhou, C., Jiang, S.: ‘Safety and transition-structure preserving abstraction of hybrid systems with inputs/outputs’. Proc. 9th Int. Workshop on Discrete Event Systems, Gothenburg, Sweden, May 2008.
    35. 35)
      • 36. Kacprzak, M., Lomuscio, A., Niewiadomski, A., et al: ‘Comparing BDD and SAT based techniques for model checking Chaum's dining cryptographers protocol’, Fundam. Inf., 2006, 72, pp. 215–234.
    36. 36)
      • 32. Frehse, G., Kateja, R., Guernic, C.L.: ‘Flowpipe approximation and clustering in space-time’. HSCC, 2013.
    37. 37)
      • 43. Johnson, T.T., Mitra, S.: ‘Anonymized reachability of hybrid automata networks’. FORMATS, 2014.
    38. 38)
      • 4. Jiang, S.: ‘Reachability analysis of linear hybrid automata by using counterexample fragment based abstraction refinement’. Proc. 2007 American Control Conf., New York, NY, July 2007, pp. 4172–4177.
    39. 39)
      • 2. Henzinger, T.: ‘The theory of hybrid automata’. Lecture Notes in Computer Science, 1996.
    40. 40)
      • 35. Clarke, E.M., Grumberg, O., Peled, D.: ‘Model checking’ (MIT Press, 1999).
    41. 41)
      • 5. Jiang, S.: ‘Abstraction based reachability analysis of concurrent linear hybrid automata’. GM Research Report ECI-293, December 2006.
    42. 42)
      • 46. Duggirala, P.S., Fan, C., Potok, M., et al: ‘Tutorial: software tools for hybrid systems verification, transformation, and synthesis: C2E2, HyST, and TuLiP’. CCA, 2016.
    43. 43)
      • 40. Quesel, J., Mitsch, S., Loos, S., et al: ‘How to prove complex properties of hybrid systems with KeYmaera: a tutorial’, 2012.
    44. 44)
      • 38. Prabhakar, P., Duggirala, P.S., Mitra, S., et al: ‘Hybrid automata-based CEGAR for rectangular hybrid systems’, Form. Methods Syst. Des., 2013, 46, pp. 105–134.
    45. 45)
      • 29. Makino, K., Berz, M.: ‘Rigorous integration of flows and ODEs using Taylor models’. SNC, 2009.
    46. 46)
      • 13. Dang, T., Maler, O.: ‘Reachability analysis via face lifting’. HSCC, 1998.
    47. 47)
      • 41. Quesel, J., Mitsch, S., Loos, S., et al: ‘How to model and prove hybrid systems with KeYmaera: a tutorial on safety’, STTT, 2015, 18, pp. 67–91.
http://iet.metastore.ingenta.com/content/journals/10.1049/iet-cps.2016.0042
Loading

Related content

content/journals/10.1049/iet-cps.2016.0042
pub_keyword,iet_inspecKeyword,pub_concept
6
6
Loading
Print this page
This is a required field
Please enter a valid email address