Bounded model checking of Time Petri Nets using SAT solver

被引：2

作者：

Yokogawa, Tomoyuki ^{[1
]}

Kondo, Masafumi ^{[2
]}

Miyazaki, Hisashi ^{[2
]}

Amasaki, Sousuke ^{[1
]}

Sato, Yoichiro ^{[1
]}

Arimoto, Kazutami ^{[1
]}

机构：

[1] Okayama Prefectural Univ, Okayama 7191197, Japan

[2] Kawasaki Univ Med Welf, Kurashiki, Okayama 7010193, Japan

来源：

IEICE ELECTRONICS EXPRESS | 2015年 / 12卷 / 02期

关键词：

symbolic model checking; bounded model checking; Time Petri Net; SAT solver;

D O I：

10.1587/elex.11.20141112

中图分类号：

TM [电工技术]; TN [电子技术、通信技术];

学科分类号：

0808 ; 0809 ;

摘要：

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 there exists-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.

引用

页数：7

共 50 条

[41] Improving state class constructions for CTL* model checking of time Petri nets
Hadjidj R.
Boucheneb H.
[J]. International Journal on Software Tools for Technology Transfer, 2008, 10 (2) : 167 - 184
[42] Refining the SAT decision ordering for bounded model checking
Wang, C
Jin, HS
Hachtel, GD
Somenzi, F
[J]. 41ST DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2004, 2004, : 535 - 538
[43] On the Community Structure of Bounded Model Checking SAT Problems
Baud-Berthier, Guillaume
Giraldez-Cru, Jesus
Simon, Laurent
[J]. THEORY AND APPLICATIONS OF SATISFIABILITY TESTING (SAT 2017), 2017, 10491 : 65 - 82
[44] Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph
Traonouez, Louis-Marie
Lime, Didier
Roux, Olivier H.
[J]. FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, PROCEEDINGS, 2008, 5215 : 280 - 294
[45] Bounded model checking of software using SMT solvers instead of SAT solvers
Armando A.
Mantovani J.
Platania L.
[J]. International Journal on Software Tools for Technology Transfer, 2009, 11 (1) : 69 - 83
[46] Bounded model checking of software using SMT solvers instead of SAT solvers
Armando, A
Mantovani, J
Platania, L
[J]. MODEL CHECKING SOFTWARE, PROCEEDINGS, 2006, 3925 : 146 - 162
[47] Efficient distributed SAT and SAT-based distributed Bounded Model Checking
Malay K. Ganai
Aarti Gupta
Zijiang Yang
Pranav Ashar
[J]. International Journal on Software Tools for Technology Transfer, 2006, 8 (4-5) : 387 - 396
[48] Efficient distributed SAT and SAT-based distributed bounded model checking
Ganai, MK
Gupta, A
Yang, ZJ
Ashar, P
[J]. CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, PROCEEDINGS, 2003, 2860 : 334 - 347
[49] Efficient software product-line model checking using induction and a SAT solver
He, Fei
Gao, Yuan
Yin, Liangze
[J]. FRONTIERS OF COMPUTER SCIENCE, 2018, 12 (02) : 264 - 279
[50] Efficient software product-line model checking using induction and a SAT solver
Fei He
Yuan Gao
Liangze Yin
[J]. Frontiers of Computer Science, 2018, 12 : 264 - 279

← 1 2 3 4 5 →