http://iet.metastore.ingenta.com
1887

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

  • PDF
    2.1803579330444336MB
  • HTML
    460.33203125Kb
  • XML
    286.1318359375Kb
Loading full text...

Full text loading...

/deliver/fulltext/iet-cps/2/2/IET-CPS.2016.0042.html;jsessionid=20c7skvjxomas.x-iet-live-01?itemId=%2fcontent%2fjournals%2f10.1049%2fiet-cps.2016.0042&mimeType=html&fmt=ahah

References

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