×

Verifying complex continuous real-time systems with coinductive CLP(R). (English) Zbl 1284.68365

Dediu, Adrian-Horia (ed.) et al., Language and automata theory and applications. 4th international conference, LATA 2010, Trier, Germany, May 24–28, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-13088-5/pbk). Lecture Notes in Computer Science 6031, 536-548 (2010).
Summary: 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.
For the entire collection see [Zbl 1187.68004].

MSC:

68Q45 Formal languages and automata
68N17 Logic programming
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

Uppaal
PDFBibTeX XMLCite
Full Text: DOI