Authors : R. Boudour and M.T. Kimour
Abstract: The verification of finite-state systems by model-checking often requires to generate (a large part of) the state space of the system under analysis. In this study, we aim 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.
R. Boudour and M.T. Kimour , 2005. SYMTC: Towards a Symbolic Model Checking for the Codesign . Asian Journal of Information Technology, 4: 1055-1060.