Synthesising certificates in networks of timed automata

Buy article PDF
© The Institution of Engineering and Technology
Published 29/07/2012

Abstract

The authors present an automatic method for the synthesis of certificates for components in embedded real-time systems. A certificate is a small homomorphic abstraction that can transparently replace the component during model checking: if the verification with the certificate succeeds, then the component is guaranteed to be correct; if the verification with the certificate fails, then the component itself must be erroneous. The authors give a direct construction, based on a forward and backward reachability analysis of the timed system, and an iterative refinement process, which produces a series of successively smaller certificates. In their experiments, model checking the certificate is several orders of magnitude faster than model checking the original system.

Inspec keywords: automata theory; embedded systems; formal verification; iterative methods; reachability analysis

Other keywords: iterative refinement process; backward reachability analysis; homomorphic abstraction; certificate synthesis; forward reachability analysis; model checking; timed automata; embedded real-time systems

Subjects: Interpolation and function approximation (numerical analysis); Combinatorial mathematics; Formal methods; Automata theory

References

    1. 1)
    2. 2)
      • Namjoshi, K.S.: `Certifying model checkers', Proc. 13th Int. Conf. on Computer Aided Verification, (CAV 2001), 18–22 July 2001, Paris, France, p. 2–13, (LNCS, 2102)
    3. 3)
      • Alur, R., Courcoubetis, C., Halbwachs, N., Dill, D.L., Wong-Toi, H.: `Minimization of timed transition systems', Proc. Third Int. Conf. on Concurrency Theory, (CONCUR 1992), 24–27 August 1992, Stony Brook, NY, USA, p. 340–354, (LNCS, 630)
    4. 4)
    5. 5)
      • Dierks, H., Kupferschmid, S., Larsen, K.G.: `Automatic abstraction refinement for timed automata', Proc. Fifth Int. Conf. on Formal Modeling and Analysis of Timed Systems, (FORMATS 2007), 3–5 October 2007, Salzburg, Austria, p. 114–129, (LNCS, 4763)
    6. 6)
    7. 7)
    8. 8)
      • Balarin, F.: `Approximate reachability analysis of timed automata', Proc. 17th IEEE Real-Time Syst. Symp., (RTSS 1996), 4–6 December 1996, Washington, DC, USA, p. 52–61
    9. 9)
      • Daws, C., Tripakis, S.: `Model checking of real-time reachability properties using abstractions', Proc. Fourth Workshop on Tools and Algorithms for the Construction and Analysis of Systems, (TACAS 1998), 28 March–4, April 1998, Lisbon, Portugal, p. 313–329, (LNCS, 1384)
    10. 10)
    11. 11)
      • Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: `Partial order reductions for timed systems', Proc. 9th Int. Conf. on Concurr. Theory, (CONCUR 1998), 8–11 September 1998, Nice, France, p. 485–500, (LNCS, 1466)
    12. 12)
      • Daws, C., Yovine, S.: `Reducing the number of clock variables of timed automata', Proc. 17th IEEE Real-Time Systems Symp., (RTSS 1996), 4–6 December 1996, Washington, DC, USA, p. 73–81
    13. 13)
      • Laroussinie, F., Larsen, K.G.: `Compositional model checking of real time systems', Proc. Sixth Int. Conf. on Concurrency Theory, (CONCUR 1992), 21–24 August 1995, Philadelphia, PA, USA, p. 27–41, (LNCS, 962)
    14. 14)
      • Laroussinie, F., Larsen, K.G.: `CMC: a tool for compositional model-checking of real-time systems', Proc. 11th Int. Conf. on Formal Description Techniques for Distributed Systems and Communication Protocols, (FORTE 1998), 3–6 November 1998, Paris, France, p. 439–456, (IFIP Conf. Proc., 135)
    15. 15)
      • Cobleigh, J.M., Giannakopoulou, D., Păsăreanu, C.S.: `Learning assumptions for compositional verification', Proc. Ninth Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, (TACAS 2003), 7–11 April 2003, Warsaw, Poland, p. 331–346, (LNCS, 2619)
    16. 16)
      • Alur, R., Madhusudan, P., Nam, W.: `Symbolic compositional verification by learning assumptions', Proc. 17th Int. Conf. on Computer Aided Verification, (CAV 2005), 6–10 July 2005, Edinburgh, Scotland, UK, p. 548–562, (LNCS, 3576)
    17. 17)
      • Alur, R., Cerny, P., Madhusudan, P., Nam, W.: `Synthesis of interface specifications for Java classes', Proc. 32nd Ann. Symp. on Principles of Programming Languages, (POPL 2005), 12–14 January 2005, Long Beach, CA, USA, p. 98–109
    18. 18)
      • Holzmann, G.: The spin model checker, primer and reference manual, 2003 (Addison-WesleyReading, MA)
    19. 19)
      • Finkbeiner, B., Schewe, S., Brill, M.: `Automatic synthesis of assumptions for compositional model checking', Proc. 26th Int. Conf. on Formal Methods for Networked and Distributed Systems, (FORTE 2006), 26–29 September 2006, Paris, France, p. 143–158, (LNCS, 4229)
    20. 20)
      • Finkbeiner, B., Peter, H.-J., Schewe, S.: `RESY: requirement synthesis for compositional model checking', Proc. 14th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, (TACAS 2008), 31 March–3 April 2008, Budapest, Hungary, p. 463–466, (LNCS, 4963)
    21. 21)
      • Bengtsson, J.: `Clocks, DBM, and states in timed systems', 2002, PhD, Uppsala University
    22. 22)
      • Finkbeiner, B., Peter, H.-J., Schewe, S.: `Synthesizing certificates in networks of timed automata', Proc. 29th IEEE Real-Time Systems Symp., (RTSS 2008), 30 November–3 December 2008, Barcelona, Spain, p. 183–194
Print this page
This is a required field
Please enter a valid email address