全部 标题 作者
关键词 摘要

OALib Journal期刊
ISSN: 2333-9721
费用:99美元

查看量下载量

相关文章

更多...

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

Abstract:

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.

Full-Text

Contact Us

service@oalib.com

QQ:3279437679

WhatsApp +8615387084133