SYMTC: An Efficient Symbolic Model Checker for Embedded Systems

In this study, we aimed at improving the performances of state space construction by using an efficient method to avoid state explosion problem in model checking through the use of-DBM (Difference Bounded Matrices) and on the fly strategy. This approach requires at any time, only the needed states to be in memory and allows for checking several properties, especially, safety, bounded liveness and temporal correctness, which are the most important ones in reactive systems. The specifications are expressed in timed automata and TCTL for the system and properties, respectively. The effectiveness of our approach has been demonstrated on many academic examples. The results obtained demonstrate that it is able to verify several properties that could not be checked by other state-of-the-art tools.