Proving temporal properties of hybrid systems
Sanjai Narain, Jeff Rothenberg · NCSU Libraries Repository (North Carolina State University Libraries) · 1990
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. >