Title :
Proving temporal properties of hybrid systems
Author :
Narain, Sanjai ; Rothenberg, Jeff
Author_Institution :
Rand Corp., Santa Monica, CA, USA
Abstract :
A formal technique, DMOD, for modeling hybrid systems is presented. It is based on utilizing intuitions about the causality relation, and the logic of definite clauses with the SLD-resolution proof procedure. An algorithm to simulate with DMOD models is presented. Then, a general framework in which temporal properties of hybrid systems can be formulated and proved (given that those systems are modeled using DMOD) is outlined. These ideas are illustrated by proving a liveness property about a railroad crossing.<>
Keywords :
digital simulation; theorem proving; DMOD; SLD-resolution proof procedure; causality relation; hybrid systems; liveness property; railroad crossing; Calculus; Continuous time systems; Differential equations; Disk drives; Logic; Manipulators; Manufacturing processes; Robots; Temperature; Turning;
Conference_Titel :
Simulation Conference, 1990. Proceedings., Winter
Conference_Location :
New Orleans, LA, USA
Print_ISBN :
0-911801-72-3
DOI :
10.1109/WSC.1990.129523
