All Title Author
Keywords Abstract

SYMTC: An Efficient Symbolic Model Checker for Embedded Systems

Keywords: Model checking , timed automata , DBM , on the fly strategy , TCTL

Full-Text   Cite this paper   Add to My Lib


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.


comments powered by Disqus

Contact Us


微信:OALib Journal