文献

J-GLOBAL ID：202002259420423537   整理番号：20A1394815

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

Symbolic Representation of Time Petri Nets for Efficient Bounded Model Checking

著者 (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)
資料名： IEICE Transactions on Information and Systems (Web)  (IEICE Transactions on Information and Systems (Web))
巻： E103.D  号： 3  ページ： 702-705(J-STAGE)  発行年： 2020年 
JST資料番号： U0469A  ISSN： 1745-1361  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 英語 (EN)

抄録/ポイント： セーフティクリティカルシステムは,形式的検証手法で信頼性を分析するために,時間Petriネット(TPN)を用いてしばしばモデル化される。本論文は,充足可能性解決に基づく境界モデル検査を導入してTPNのための効率的検証方法を提案した。提案方法は,差異論理(DL)によってTPNの時間制約を表現して,検証のためにSMTソルバを使用した。また,その有効性を実験で実証した。(翻訳著者抄録)

シソーラス用語： *モデル検査 ,  *時間 ,  *Petriネット ,  表現 ,  システム ,  検証 ,  信頼性 ,  モデリング ,  可能性 ,  論理 ,  制約条件
準シソーラス用語： セーフティクリティカルシステム ,  モデル化 ,  *記号表現 ,  *境界モデル検査 ,  形式的検証 ,  差異 ,  時間制約 ,  充足可能性

著者キーワード (4件)： 形式的検証 ,  時間Petriネット ,  SMTソルバー ,  差分論理

分類 (2件)： 計算機システム開発  (JD02010R) ,  信頼性  (KB04040H)

引用文献 (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

タイトルに関連する用語 (3件)： 境界モデル検査 ,  Petriネット ,  記号表現