The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. ex. Some numerals are expressed as "XNUMX".
Copyrights notice
The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. Copyrights notice
Les systèmes critiques pour la sécurité sont souvent modélisés à l'aide de Time Petri Nets (TPN) pour analyser leur fiabilité avec des méthodes de vérification formelles. Cet article propose une méthode de vérification efficace pour TPN introduisant une vérification de modèle bornée basée sur la résolution de satisfiabilité. La méthode proposée exprime les contraintes temporelles du TPN par différence logique (DL) et utilise des solveurs SMT pour la vérification. Son efficacité a également été démontrée par une expérience.
Nao IGAWA
Okayama Prefectural University
Tomoyuki YOKOGAWA
Okayama Prefectural University
Sousuke AMASAKI
Okayama Prefectural University
Masafumi KONDO
Kawasaki University of Medical Welfare
Yoichiro SATO
Okayama Prefectural University
Kazutami ARIMOTO
Okayama Prefectural University
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Copier
Nao IGAWA, Tomoyuki YOKOGAWA, Sousuke AMASAKI, Masafumi KONDO, Yoichiro SATO, Kazutami ARIMOTO, "Symbolic Representation of Time Petri Nets for Efficient Bounded Model Checking" in IEICE TRANSACTIONS on Information,
vol. E103-D, no. 3, pp. 702-705, March 2020, doi: 10.1587/transinf.2019EDL8086.
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2019EDL8086/_p
Copier
@ARTICLE{e103-d_3_702,
author={Nao IGAWA, Tomoyuki YOKOGAWA, Sousuke AMASAKI, Masafumi KONDO, Yoichiro SATO, Kazutami ARIMOTO, },
journal={IEICE TRANSACTIONS on Information},
title={Symbolic Representation of Time Petri Nets for Efficient Bounded Model Checking},
year={2020},
volume={E103-D},
number={3},
pages={702-705},
abstract={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.},
keywords={},
doi={10.1587/transinf.2019EDL8086},
ISSN={1745-1361},
month={March},}
Copier
TY - JOUR
TI - Symbolic Representation of Time Petri Nets for Efficient Bounded Model Checking
T2 - IEICE TRANSACTIONS on Information
SP - 702
EP - 705
AU - Nao IGAWA
AU - Tomoyuki YOKOGAWA
AU - Sousuke AMASAKI
AU - Masafumi KONDO
AU - Yoichiro SATO
AU - Kazutami ARIMOTO
PY - 2020
DO - 10.1587/transinf.2019EDL8086
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E103-D
IS - 3
JA - IEICE TRANSACTIONS on Information
Y1 - March 2020
AB - 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.
ER -