  This paper presents a novel approach to including non-instantaneous discrete
control transitions in the linear hybrid automaton approach to simulation and
verification of hybrid control systems. In this paper we study the control of a
continuously evolving analog plant using a controller programmed in a
synchronous programming language. We provide extensions to the synchronous
subset of the SystemJ programming language for modeling, implementation, and
verification of such hybrid systems. We provide a sound rewrite semantics that
approximate the evolution of the continuous variables in the discrete domain
inspired from the classical supervisory control theory. The resultant discrete
time model can be verified using classical model-checking tools. Finally, we
show that systems designed using our approach have a higher fidelity than the
ones designed using the hybrid automaton approach.
