×

zbMATH — the first resource for mathematics

Analysis of linear hybrid systems in CLP. (English) Zbl 1185.68406
Hanus, Michael (ed.), Logic-based program synthesis and transformation. 18th international symposium, LOPSTR 2008, Valencia, Spain, July 17–18, 2008. Revised selected papers. Berlin: Springer (ISBN 978-3-642-00514-5/pbk). Lecture Notes in Computer Science 5438, 55-70 (2009).
Summary: In this paper we present a procedure for representing the semantics of linear hybrid automata (LHAs) as constraint logic programs (CLP); flexible and accurate analysis and verification of LHAs can then be performed using generic CLP analysis and transformation tools. LHAs provide an expressive notation for specifying real-time systems. The main contributions are (i) a technique for capturing the reachable states of the continuously changing state variables of the LHA as CLP constraints; (ii) a way of representing events in the LHA as constraints in CLP, along with a product construction on the CLP representation including synchronisation on shared events; (iii) a framework in which various kinds of reasoning about an LHA can be flexibly performed by combining standard CLP transformation and analysis techniques. We give experimental results to support the usefulness of the approach and argue that we contribute to the general field of using static analysis tools for verification.
For the entire collection see [Zbl 1157.68006].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68N17 Logic programming
68Q45 Formal languages and automata
Software:
LOGEN; PPL; Uppaal
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science 138(1), 3–34 (1995) · Zbl 0874.68206 · doi:10.1016/0304-3975(94)00202-T
[2] Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 209–229. Springer, Heidelberg (1993) · doi:10.1007/3-540-57318-6_30
[3] Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994) · Zbl 0803.68071 · doi:10.1016/0304-3975(94)90010-8
[4] Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. J. Software Tools for Technology Transfer 8(4-5), 449–466 (2006) · Zbl 05075103 · doi:10.1007/s10009-005-0215-8
[5] Bagnara, R., Ricci, E., Zaffanella, E., Hill, P.M.: Possibly not closed convex polyhedra and the Parma Polyhedra Library. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 213–229. Springer, Heidelberg (2002) · Zbl 1015.68215 · doi:10.1007/3-540-45789-5_17
[6] Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004) · Zbl 1105.68350 · doi:10.1007/978-3-540-30080-9_7
[7] Benoy, F., King, A.: Inferring argument size relationships with CLP(R). In: Gallagher, J.P. (ed.) LOPSTR 1996. LNCS, vol. 1207, pp. 204–223. Springer, Heidelberg (1997) · doi:10.1007/3-540-62718-9_12
[8] Brzoska, C.: Temporal logic programming in dense time. In: ILPS, pp. 303–317. MIT Press, Cambridge (1995)
[9] Carloni, L.P., Passerone, R., Pinto, A., Sangiovanni-Vincentelli, A.L.: Languages and tools for hybrid systems design. Found. Trends Electron. Des. Autom. 1(1/2), 1–193 (2006) · Zbl 1143.68346 · doi:10.1561/1000000001
[10] Codish, M., Taboch, C.: A semantic basic for the termination analysis of logic programs. The Journal of Logic Programming 41(1), 103–123 (1999) · Zbl 0948.68114 · doi:10.1016/S0743-1066(99)00006-0
[11] Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th Annual ACM Symposium on Principles of Programming Languages, pp. 84–96 (1978) · doi:10.1145/512760.512770
[12] Debray, S., Ramakrishnan, R.: Abstract Interpretation of Logic Programs Using Magic Transformations. Journal of Logic Programming 18, 149–176 (1994) · Zbl 0795.68037 · doi:10.1016/0743-1066(94)90050-7
[13] Delzanno, G., Podelski, A.: Model checking in CLP. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 223–239. Springer, Heidelberg (1999) · doi:10.1007/3-540-49059-0_16
[14] Du, X., Ramakrishnan, C.R., Smolka, S.A.: Real-time verification techniques for untimed systems. Electr. Notes Theor. Comput. Sci. 39(3) (2000) · Zbl 0971.68101
[15] Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying CTL properties of infinite-state systems by specializing constraint logic programs. In: Leuschel, M., Podelski, A., Ramakrishnan, C., Ultes-Nitsche, U. (eds.) Proceedings of the Second International Workshop on Verification and Computational Logic (VCL 2001), pp. 85–96 (2001); tech. Report DSSE-TR-2001-3, University of Southampton
[16] Gallagher, J.P., Henriksen, K.S.: Abstract domains based on regular types. In: Demoen, B., Lifschitz, V. (eds.) ICLP 2004. LNCS, vol. 3132, pp. 27–42. Springer, Heidelberg (2004) · Zbl 1104.68377 · doi:10.1007/978-3-540-27775-0_3
[17] Gallagher, J.P., Henriksen, K.S., Banda, G.: Techniques for scaling up analyses based on pre-interpretations. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol. 3668, pp. 280–296. Springer, Heidelberg (2005) · Zbl 1165.68332 · doi:10.1007/11562931_22
[18] Genaim, S., Codish, M.: Inferring termination conditions of logic programs by backwards analysis. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS, vol. 2250, pp. 681–690. Springer, Heidelberg (2001) · Zbl 1275.68046
[19] 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) · Zbl 1213.68177 · doi:10.1007/978-3-540-74610-2_4
[20] Gupta, G., Pontelli, E.: A constraint-based approach for specification and verification of real-time systems. In: IEEE Real-Time Systems Symposium, pp. 230–239 (1997) · doi:10.1109/REAL.1997.641285
[21] Halbwachs, N., Proy, Y.E., Raymound, P.: Verification of linear hybrid systems by means of convex approximations. In: LeCharlier, B. (ed.) SAS 1994. LNCS, vol. 864, pp. 223–237. Springer, Heidelberg (1994) · doi:10.1007/3-540-58485-4_43
[22] Henriksen, K.S., Banda, G., Gallagher, J.P.: Experiments with a convex polyhedral analysis tool for logic programs. In: Workshop on Logic Programming Environments, Porto (2007)
[23] Henriksen, K.S., Gallagher, J.P.: Abstract interpretation of PIC programs through logic programming. In: Proceedings of SCAM 2006, Sixth IEEE International Workshop on Source Code Analysis and Manipulation (2006) · doi:10.1109/SCAM.2006.1
[24] Henzinger, T.A.: The theory of hybrid automata. In: Clarke, E.M. (ed.) Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, pp. 278–292. IEEE Computer Society Press, Los Alamitos (1996) · Zbl 0959.68073 · doi:10.1109/LICS.1996.561342
[25] Jaffar, J., Maher, M.: Constraint Logic Programming: A Survey. Journal of Logic Programming 19/20, 503–581 (1994) · Zbl 00639141 · doi:10.1016/0743-1066(94)90033-7
[26] Jaffar, J., Santosa, A.E., Voicu, R.: A CLP proof method for timed automata. In: Anderson, J., Sztipanovits, J. (eds.) The 25th IEEE International Real-Time Systems Symposium, pp. 175–186. IEEE Computer Society, Los Alamitos (2004) · doi:10.1109/REAL.2004.5
[27] Katoen, J.-P.: Concepts, algorithms, and tools for model checking. A lecture notes of the course ”Mechanised Validation of Parallel Systems” for 1998/99 at Friedrich-Alexander Universitat, Erlangen-Nurnberg, p. 195 (1999)
[28] Leuschel, M., Fontaine, M.: Probing the depths of CSP-M: A new fdr-compliant validation tool. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 278–297. Springer, Heidelberg (2008) · Zbl 05362221 · doi:10.1007/978-3-540-88194-0_18
[29] Leuschel, M., Jørgensen, J.: Efficient specialisation in Prolog using the hand-written compiler generator LOGEN. Elec. Notes Theor. Comp. Sci. 30(2) (1999) · Zbl 0958.68036
[30] Leuschel, M., Massart, T.: Infinite state model checking by abstract interpretation and program specialisation. In: Bossi, A. (ed.) LOPSTR 1999. LNCS, vol. 1817, pp. 63–82. Springer, Heidelberg (2000) · Zbl 0964.68086 · doi:10.1007/10720327_5
[31] Mesnard, F.: Towards automatic control for CLP(\(\chi\)) programs. In: Proietti, M. (ed.) LOPSTR 1995. LNCS, vol. 1048, pp. 106–119. Springer, Heidelberg (1996) · doi:10.1007/3-540-60939-3_8
[32] Nilsson, U., Lübcke, J.: Constraint logic programming for local and symbolic model-checking. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS, vol. 1861, pp. 384–398. Springer, Heidelberg (2000) · Zbl 0983.68119 · doi:10.1007/3-540-44957-4_26
[33] Pemmasani, G., Ramakrishnan, C.R., Ramakrishnan, I.V.: Efficient real-time model checking using tabled logic programming and constraints. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, vol. 2401, pp. 100–114. Springer, Heidelberg (2002) · Zbl 1045.68520 · doi:10.1007/3-540-45619-8_8
[34] Peralta, J.C., Gallagher, J.P.: Convex hull abstractions in specialization of CLP programs. In: Leuschel, M.A. (ed.) LOPSTR 2002. LNCS, vol. 2664, pp. 90–108. Springer, Heidelberg (2003) · Zbl 1278.68052 · doi:10.1007/3-540-45013-0_8
[35] Podelski, A.: Model checking as constraint solving. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 22–37. Springer, Heidelberg (2000) · Zbl 0966.68121 · doi:10.1007/978-3-540-45099-3_2
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.