Forward symbolic model checking for real time systems

Synchronous languages are widely used in industrial applications for the design and implementation of real-time embedded and reactive systems and are also well-suited for real-time verification purposes, since they have clean formal semantics. In this paper we focus on the real-time temporal logic JCTL, which can directly support the real-time formal verification of synchronous programs for the design of systems in earlier (high-level) as well as in later (low-level) design stages, creating a bridging between industrial real-time descriptions and formal real-time verification. We extend the model-checking capabilities of JCTL, by introducing new forward symbolic model-checking techniques, allowing JCTL to benefit from both, forward-, as well as traditional backward state traversal methods and of course, their combination.