An efficient symbolic model checker

In computer systems, the goal is to achieve methods and tools that can check models automatically: model checking. The model checking problem is the large states space. One solution is to use the symbolic model checking combined with compact data structures. The main of this paper is to design and implement a powerful new tool to check important properties in critical systems based on the concept of symbolic state and DBM data structures (Difference Bound Matrices). The specifications are expressed using timed automata system and realtime logic for properties. The obtained results are compared with those in the literature.Key words: symbolic model checking - timed automata - TCTL–on the fly - DBM