TY  - JOUR
T1  - SYMTC: Towards a Symbolic Model Checking for the Codesign
AU - , R. Boudour AU - , M.T. Kimour 
JO  - Asian Journal of Information Technology
VL  - 4
IS  - 11
SP  - 1055
EP  - 1060
PY  - 2005
DA  - 2001/08/19
SN  - 1682-3915
DO  - ajit.2005.1055.1060
UR  - https://makhillpublications.co/view-article.php?doi=ajit.2005.1055.1060
KW  - Model checking
KW  -timed automata
KW  -DBM
KW  -on the fly strategy
KW  -TCTL
AB  - 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.
ER  -