Bounded model checking of Time Petri Nets using SAT solver

IEICE Electronics Express

Kazutami Arimoto²  Yoichiro Sato²  Tomoyuki Yokogawa²  Hisashi Miyazaki¹  Masafumi Kondo¹  Sousuke Amasaki² 

[1] Kawasaki University of Medical Welfare;Okayama Prefectural University

关键词: symbolic model checking;    bounded model checking;    Time Petri Net;    SAT solver;   

DOI  :  10.1587/elex.11.20141112

学科分类：电子、光学、磁材料

来源: Denshi Jouhou Tsuushin Gakkai

【 摘 要 】

References(10)To carry out performance evaluation of an asynchronous system, the system is modeled as Time Petri Net (TPN) and an iteration of Petri net simulations produces its performance index. The TPN model needs to satisfy required properties such as deadlock freeness. We proposed a symbolic representation of TPN for SAT-based bounded model checking. In the proposed encoding scheme, firing of transitions and elapsing of place delays are expressed as boolean formulas discretely. Our representation can work with relaxed �?-step semantics which enables to perform each step by two or more transitions. We applied the encoding to example TPN models and checked the deadlock freeness using SAT solver. The results of experiments demonstrated the effectiveness of the proposed representation.

【 授权许可】

Unknown