Sciweavers

LATA
2010
Springer

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

14 years 7 months ago
Verifying Complex Continuous Real-Time Systems with Coinductive CLP(R)
Timed automata has 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 PTAs can be elegantly modeled via logic programming extended with coinduction and constraints over reals. We use this logic programming realization of a PTA 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 to this coinductive constraint logic program.
Neda Saeedloei and Gopal Gupta
Added 02 Mar 2010
Updated 02 Mar 2010
Type Conference
Year 2010
Where LATA
Authors Neda Saeedloei and Gopal Gupta
Comments (0)