2024-03-29T10:49:57Zhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_oaipmhoai:ipsj.ixsq.nii.ac.jp:000619982023-04-27T10:00:04Z01164:01384:05667:05668
周期性を持つ非同期通信システムのモデリングに関する研究A study about the modeling of the asynchronous communication system with periodicityjpnhttp://id.nii.ac.jp/1001/00061998/Technical Reporthttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_action_common_download&item_id=61998&item_no=1&attribute_id=1&file_no=1Copyright (c) 2009 by the Information Processing Society of Japan九州大学大学院システム情報科学研究院九州大学大学院システム情報科学研究院九州大学大学院システム情報科学研究院九州大学大学院システム情報科学研究院 越智, 優大森, 洋一日下部, 茂荒木, 啓二郎並列分散システムのモデル検査を行う場合,状態爆発を考慮したモデルでなければならない.本論文では通信経路上の信頼性は完全ではない代わりに,周期的な通信を行うことでサービスを提供する Vehicle Information and Communication System (VICS) というシステムに対して,システムの構成要素をサブシステムとみなして分解するモデリング手法を提案する.各サブシステムに対してモデル検査を行い,その結果を統合する.この時,サブシステム内部でも状態機械が並列動作をするが,データの値に依存しない抽象化によりモデルを作成する.最後に,対象システム全体をモデル検査しなくとも,提案するモデリング手法で検証が可能な条件を示す.State explosion is a ma jor problem of model checking. But, it happens easily in case of parallel and distributed system. We tried to reduce the combinational complexity at modeling level by dividing the whole system into state-transitional subsystems. The idea is that when subsystems are connected by repeating and not-assured communication paths such as Vehicle Information and Commu- nication System (VICS), we can concentrate to verify each subsystem because the reliability of the system is firm. Finally we show the system condition that we can validate our proposing model without whole system model check.AN10112981研究報告ソフトウェア工学(SE)200931(2009-SE-163)2172242009-03-112009-08-18