Advertisement

Combined Bounded and Symbolic Model Checking for Incomplete Timed Systems

  • Georges Morbé
  • Christian Miller
  • Christoph Scholl
  • Bernd Becker
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8855)

Abstract

We present a hybrid model checking algorithm for incomplete timed systems where parts of the system are unspecified (so-called black boxes). Here, we answer the question of unrealisability, i.e., “Is there a path violating a safety property regardless of the implementation of the black boxes?” Existing bounded model checking (BMC) approaches for incomplete timed systems exploit the power of modern SMT solvers, but might be too coarse as an abstraction for certain problem instances. On the other hand, symbolic model checking (SMC) for incomplete timed systems is more accurate, but may fail due to the size of the explored state space. In this work, we propose a tight integration of a backward SMC routine with a forward BMC procedure leveraging the strengths of both worlds. The symbolic model checker is hereby used to compute an enlarged target which we then try to hit using BMC. We use learning strategies to guide the SMT solver’s search into the right direction and manipulate the enlarged target to improve the overall accuracy of the current verification run. Our experimental results show that the hybrid approach is able to verify incomplete timed systems which are out of the scope for BMC and can neither be solved in reasonable time using SMC. Furthermore, our approach compares favourably with UPPAAL-TIGA when considering timed games as a special case of the unrealisability problem.

Keywords

Model Check Symbolic Model Check Bound Model Check Time Automaton Error Path 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alur, R.: Timed automata. Theoretical Computer Science (1999)Google Scholar
  2. 2.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science (1994)Google Scholar
  3. 3.
    Behrmann, G., Cougnard, A., David, R., Fleury, E., Larsen, K.G., Lime, D.: Uppaal tiga user-manualGoogle Scholar
  4. 4.
    Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-tiga: Time for playing games! In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 121–125. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  5. 5.
    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  6. 6.
    Bouyer, P., Bozzelli, L., Chevalier, F.: Controller synthesis for MTL specifications. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 450–464. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  7. 7.
    Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Form. Methods Syst. Des (2001)Google Scholar
  8. 8.
    Damm, W., Dierks, H., Disch, S., Hagemann, W., Pigorsch, F., Scholl, C., Waldmann, U., Wirtz, B.: Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces. Sci. Comput. Program. (2012)Google Scholar
  9. 9.
    Damm, W., Disch, S., Hungar, H., Jacobs, S., Pang, J., Pigorsch, F., Scholl, C., Waldmann, U., Wirtz, B.: Exact state set representations in the verification of linear hybrid systems with large discrete state space. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 425–440. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  10. 10.
    Dutertre, B., de Moura, L.: The YICES SMT solver. Tech. rep., Computer Science Laboratory, SRI International (2006)Google Scholar
  11. 11.
    Ehlers, R., Mattmüller, R., Peter, H.-J.: Combining symbolic representations for solving timed games. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 107–121. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  12. 12.
    Faella, M., La Torre, S., Murano, A.: Automata-theoretic decision of timed games. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, pp. 94–108. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  13. 13.
    Faella, M., La Torre, S., Murano, A.: Dense real-time games. In: LICS (2002)Google Scholar
  14. 14.
    Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems (an extended abstract). In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 229–242. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  15. 15.
    Miller, C., Gitina, K., Becker, B.: Bounded model checking of incomplete real-time systems using quantified smt formulas. In: Proc. of MTV (2011)Google Scholar
  16. 16.
    Miller, C., Gitina, K., Scholl, C., Becker, B.: Bounded model checking of incomplete networks of timed automata. In: Proc. of MTV (2010)Google Scholar
  17. 17.
    Miller, C., Scholl, C., Becker, B.: Verifying incomplete networks of timed automata. In: Proc. of MBMV (2011)Google Scholar
  18. 18.
    Morbé, G., Scholl, C.: Fully symbolic tctl model checking for incomplete timed automata. In: Proc. of AVOCS (2013)Google Scholar
  19. 19.
    Morbé, G., Scholl, C.: Fully symbolic TCTL model checking for complete and incomplete real-time systems. Reports of SFB/TR 14 AVACS 104, SFB/TR 14 AVACS (September 2014), http://www.avacs.org
  20. 20.
    Morbé, G., Pigorsch, F., Scholl, C.: Fully symbolic model checking for timed automata. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 616–632. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  21. 21.
    Nopper, T., Miller, C., Lewis, M.D.T., Becker, B., Scholl, C.: Sat modulo bdd – a combined verification approach for incomplete designs. In: MBMV (2010)Google Scholar
  22. 22.
    Scholl, C., Disch, S., Pigorsch, F., Kupferschmid, S.: Computing optimized representations for non-convex polyhedra by detection and removal of redundant linear constraints. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 383–397. Springer, Heidelberg (2009)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Georges Morbé
    • 1
  • Christian Miller
    • 1
  • Christoph Scholl
    • 1
  • Bernd Becker
    • 1
  1. 1.Department of Computer ScienceUniversity of FreiburgFreiburgGermany

Personalised recommendations