講演抄録/キーワード |
講演名 |
2008-10-17 11:00
ビットエラー通信路におけるスケーラブルCANの動作解析 ○鵜飼謙児・坂部俊樹・高田広章・倉地 亮・酒井正彦・草刈圭一朗・西田直樹(名大) SS2008-37 |
抄録 |
(和) |
スケーラブルCANプロトコルとは,従来のCAN (Controller Area Network)プロトコルを改良し,最高通信速度を10倍以上に高速化した通信プロトコルである.
本論文では,スケーラブルCANプロトコルのビットエラー時における振る舞いをモデル検査の手法を用いて解析する.まず,エラーのない通信路上のスケーラブルCANプロトコルのモデルをSMV 言語により記述し,記述したモデルが妥当であること,すなわち,所望の性質を有することをモデル検査ツールNuSMVを用いて検証する.次に,通信路をビットエラー通信路に置き換えたモデルで,再度,妥当性検証を行う.その結果として得られる反例を解析することによって,ビットエラー時にもスケーラブルCANプロトコルが正しく振る舞うように修正するための示唆を与える. |
(英) |
Scalable CAN protocol is an improvement of the original CAN (Controller Area Network) protocol so that more than ten times higher speed communication is available. In this paper, we analyze behavior of Scalable CAN on a bit-error channel by using a model checking tool,
NuSMV. We first describe in the SMV language a model of Scalable CAN on an error free channel and specifications which express desired properties of Scalable CAN. We verify by using NuSMV that this model satisfies the specifications. We next modify the model by replacing the error free channel with a bit-error channel. Model checking of the modified model for the specifications produces a counter example. We analyze the counter example and give suggestions for correcting Scalable CAN on a bit-error channel. |
キーワード |
(和) |
スケーラブルCAN / モデル検査 / 動作解析 / / / / / |
(英) |
Scalable CAN / Model Checking / Behavior Analysis / / / / / |
文献情報 |
信学技報, vol. 108, no. 242, SS2008-37, pp. 61-66, 2008年10月. |
資料番号 |
SS2008-37 |
発行日 |
2008-10-09 (SS) |
ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
SS2008-37 |