Statecharts is a formal speicification language for reactive systems and has been used successfully in industries. It provides two time models; one is synchronous time model and the other is asynchronous one. Every transition in synchronous time model takes one time unit to fire, whereas some transitions in asynchronous time model are executed instantly without elapsing time.
Although Statecharts has been widely used for real-time systems, the real-time verification methods for them, either cannot handle asynchronous time model, or increase the size of state space to check, by introducing an additional variable to the model.
This paper presents algorithms for symbolic real-time model checking and real-time computation. These algorithms count only unit-length transitions and count them implicitly. Therefore, they are compatible with both time models of Statecharts as well as can compute elapsed time without additional variables.
We have implemented the proposed algorithms by extending an existing symbolic model checker, NuSMV, and present the experimental results that show the performance advantages in terms of both time and memory.
