Art

J-GLOBAL ID：202002259420423537   Reference number：20A1394815

Symbolic Representation of Time Petri Nets for Efficient Bounded Model Checking

効率的な境界モデル検査のための時間Petriネットの記号表現

Author (6)： IGAWA Nao (Okayama Prefectural University) ,  YOKOGAWA Tomoyuki (Okayama Prefectural University) ,  AMASAKI Sousuke (Okayama Prefectural University) ,  KONDO Masafumi (Kawasaki University of Medical Welfare) ,  SATO Yoichiro (Okayama Prefectural University) ,  ARIMOTO Kazutami (Okayama Prefectural University)
Material： IEICE Transactions on Information and Systems (Web)  (IEICE Trans Inf Syst (Web))
Volume： E103.D  Issue： 3  Page： 702-705(J-STAGE)  Publication year： 2020 
JST Material Number： U0469A  ISSN： 1745-1361  Document type： Article
Article type： 原著論文  Country of issue： Japan (JPN)  Language： ENGLISH (EN)

Thesaurus term： *model checking ,  *Time ,  *Petri net ,  representation ,  system ,  verification ,  reliability (property) ,  modeling ,  possibility ,  Logic ,  constraint condition (restriction) ,  *symbolic representation ,  difference ,  time constraint
Semi thesaurus term： safety-critical systems ,  modeling ,  *bounded model checking ,  formal verification ,  satisfiability

Author keywords (4)： formal verification ,  Time Petri Net ,  SMT Solver ,  difference logic

JST classification (2)： Computer system development  (JD02010R) ,  Reliability  (KB04040H)

Reference (22)：

• [1] S. Bernardi, J. Campos, and J. Merseguer, “Timing-Failure Risk Assessment of UML Design Using Time Petri Net Bound Techniques,” IEEE Trans. Industr. Inform., vol.7, no.1, pp.90-104, 2011. 10.1109/tii.2010.2098415
• [2] Y.H. Kacem, A. Magdich, A. Mahfoudhi, C. Mraidha, and W. Karamti, “Using MDE and Priority Time Petri Nets for the schedulability analysis of Embedded Systems modeled by UML activity diagrams,” Proc. IEEE 19th Int'l Conf. and Workshops on Eng. Comp. Based Syst. (ECBS 2012), pp.316-323, 2012. 10.1109/ecbs.2012.6487436
• [3] P. Merlin and D. Farber, “Recoverability of Communication Protocols-Implications of a Theoretical Study,” IEEE Trans. Comm., vol.24, no.9, pp.1036-1043, Sept. 1976. 10.1109/tcom.1976.1093424
• [4] B. Berthomieu, P.-O. Ribet, and F. Vernadat, “The tool TINA-Construction of abstract state spaces for Petri nets and Time Petri nets,” International Journal of Production Research, vol.42, no.14, pp.2741-2756, 2007. 10.1080/00207540412331312688
• [5] D. Lime, O.H. Roux, C. Seidner, and L.-M. Traonouez, “Romeo: A parametric model-checker for petri nets with stopwatches,” Proc. 15th Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), pp.54-57, 2009. 10.1007/978-3-642-00768-2_6

Terms in the title (3)： 境界モデル検査 ,  Petriネット ,  記号表現