Advertisement

Verifying Complex Continuous Real-Time Systems with Coinductive CLP(R)

  • Neda Saeedloei
  • Gopal Gupta
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6031)

Abstract

Timed automata have been used as a powerful formalism for specifying, designing, and analyzing real-time systems. We consider the generalization of timed automata to Pushdown Timed Automata (PTA). We show how PTA can be elegantly modeled via logic programming extended with co-induction and constraints over reals. We propose a general framework based on constraint logic programming and co-induction for modeling/verifying real-time systems. We use this framework to develop an elegant solution to the generalized railroad crossing problem of Lynch and Heitmeyer. Interesting properties of the system can be verified merely by posing appropriate queries.

Keywords

Logic Programming Safety Property Approach Signal Wall Clock Time Constraint Logic Programming 
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., Dill, D.L.: Automata for modeling real-time systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322–335. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  2. 2.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Baker, T.P. (ed.): Proceedings of the 30th IEEE Real-Time Systems Symposium, RTSS 2009, Washington, DC, USA, December 1-4 (2009); Baker, T.P. (ed.): IEEE Real-Time Systems Symposium. IEEE Computer Society, Los Alamitos (2009)Google Scholar
  4. 4.
    Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: SFM, pp. 200–236 (2004)Google Scholar
  5. 5.
    Dang, Z.: Binary reachability analysis of pushdown timed automata with dense clocks. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 506–518. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  6. 6.
    Gupta, G., Bansal, A., Min, R., Simon, L., Mallya, A.: Coinductive logic programming and its applications. In: Dahl, V., Niemelä, I. (eds.) ICLP 2007. LNCS, vol. 4670, pp. 27–44. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  7. 7.
    Gupta, G., Pontelli, E.: A constraint-based approach for specification and verification of real-time systems. In: IEEE Real-Time Systems Symp., pp. 230–239 (1997)Google Scholar
  8. 8.
    Heitmeyer, C.L., Lynch, N.A.: The generalized railroad crossing: A case study in formal verification of real-time systems. In: IEEE RTSS, pp. 120–131 (1994)Google Scholar
  9. 9.
    Jaffar, J., Maher, M.J.: Constraint logic programming: A survey. J. Log. Program. 19/20, 503–581 (1994)CrossRefMathSciNetGoogle Scholar
  10. 10.
    Jaffar, J., Santosa, A.E., Voicu, R.: A CLP proof method for timed automata. In: RTSS, pp. 175–186 (2004)Google Scholar
  11. 11.
    Lee, E.A.: Cyber physical systems: Design challenges. In: ISORC (May 2008)Google Scholar
  12. 12.
    Puchol, C.: A solution to the generalized railroad crossing problem in Esterel. Technical report, Dep. of Comp. Science, The University of Texas at Austin (1995)Google Scholar
  13. 13.
    Simon, L., Bansal, A., Mallya, A., Gupta, G.: Co-logic programming: Extending logic programming with coinduction. In: ICALP, pp. 472–483 (2007)Google Scholar
  14. 14.
    Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science. Formal Models and Sematics (B), vol. B, pp. 133–192. MIT Press, Cambridge (1990)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Neda Saeedloei
    • 1
  • Gopal Gupta
    • 1
  1. 1.Department of Computer ScienceUniversity of Texas at DallasRichardson

Personalised recommendations