Symbolic Representation of Time Petri Nets for Efficient Bounded Model Checking

Nao IGAWA  Tomoyuki YOKOGAWA  Sousuke AMASAKI  Masafumi KONDO  Yoichiro SATO  Kazutami ARIMOTO  

IEICE TRANSACTIONS on Information and Systems   Vol.E103-D   No.3   pp.702-705
Publication Date: 2020/03/01
Online ISSN: 1745-1361
DOI: 10.1587/transinf.2019EDL8086
Type of Manuscript: LETTER
Category: Software System
formal verification,  Time Petri Net,  SMT Solver,  difference logic,  

Full Text: PDF(99.9KB)>>
Buy this Article

Safety critical systems are often modeled using Time Petri Nets (TPN) for analyzing their reliability with formal verification methods. This paper proposed an efficient verification method for TPN introducing bounded model checking based on satisfiability solving. The proposed method expresses time constraints of TPN by Difference Logic (DL) and uses SMT solvers for verification. Its effectiveness was also demonstrated with an experiment.