Interpolation Based Unbounded Model Checking for Time Petri Nets

被引：0

作者：

Igawa, Nao ^{[1
]}

Yokogawa, Tomoyuki ^{[1
]}

Amasaki, Sousuke ^{[1
]}

Komoku, Kiyotaka ^{[1
]}

Sato, Yoichiro ^{[1
]}

Arimoto, Kazutami ^{[1
]}

机构：

[1] Okayama Prefectural Univ, 111 Kuboki, Okayama 7191197, Japan

来源：

2018 IEEE 7TH GLOBAL CONFERENCE ON CONSUMER ELECTRONICS (GCCE 2018) | 2018年

关键词：

unbounded model checking; interpolation; Time Petri Net; SMT Solver; MathSAT;

D O I：

暂无

中图分类号：

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

学科分类号：

0808 ; 0809 ;

摘要：

Safety critical systems are often modeled using Time Petri Net (TPN) for analyzing its reliability with formal verification methods. This paper proposed a safety verification method for TPN introducing unbounded model checking based on over-approximation of the state space. The proposed method expresses time constraints of TPN by Difference Logic (DL) and uses an SMT solver for verification. DL is a sub-theory of linear arithmetic obtained by restricting each inequality between a difference of two variables and a constant. Its effectiveness was also demonstrated with an experiment.

引用

页码：619 / 623

页数：5

共 50 条

[21] Model checking of Signal Interpreted Petri Nets
Weng, XY
Litz, L
[J]. 2001 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN, AND CYBERNETICS, VOLS 1-5: E-SYSTEMS AND E-MAN FOR CYBERNETICS IN CYBERSPACE, 2002, : 2748 - 2752
[22] Scenario-based timing consistency checking for time Petri nets
Li Xuandong
Bu Lei
Hu Jun
Zhao Jianhua
Zhang Tao
Zheng Guoliang
[J]. FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2006, 2006, 4229 : 388 - 403
[23] SMT-Based Reachability Checking for Bounded Time Petri Nets
Polrola, Agata
Cybula, Piotr
Meski, Artur
[J]. FUNDAMENTA INFORMATICAE, 2014, 135 (04) : 467 - 482
[24] Implementing model checking and equivalence checking for time petri nets by the RT-MEC tool
Bystrov, AV
Virbitskaite, IB
[J]. PARALLEL COMPUTING TECHNOLOGIES, 1999, 1662 : 194 - 199
[25] Decidable Classes of Unbounded Petri Nets with Time and Urgency
Akshay, S.
Genest, B.
Helouet, L.
[J]. APPLICATION AND THEORY OF PETRI NETS AND CONCURRENCY, PETRI NETS 2016, 2016, 9698 : 301 - 322
[26] Efficient abstraction refinement in interpolation-based unbounded model checking
Li, Bing
Somenzi, Fabio
[J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2006, 3920 : 227 - 241
[27] 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
[28] Specification and model checking of temporal properties in time Petri nets and timed automata
Penczek, W
Pólrola, A
[J]. APPLICATIONS AND THEORY OF PETRI NETS 2004, PROCEEDINGS, 2004, 3099 : 37 - 76
[29] Assessing Time Behaviour in Disaster Management by Using Petri Nets and Model Checking
Cicirelli, Franco
Nigro, Libero
[J]. 2023 INTERNATIONAL CONFERENCE ON INFORMATION AND COMMUNICATION TECHNOLOGIES FOR DISASTER MANAGEMENT, ICT-DM, 2023, : 181 - 186
[30] Model checking of time Petri nets using the state class timed automaton
Lime, Didier
Roux, Olivier H.
[J]. DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2006, 16 (02): : 179 - 205

← 1 2 3 4 5 →