ビットエラー通信路におけるスケーラブル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プロトコルとは，従来のCAN（Controller Area Network）プロトコルを改良し，最高通信速度を10倍以上に高速化した通信プロトコルである．本論文では，スケーラブルCANプロトコルのビットエラー時における振る舞いをモデル検査の手法を用いて解析する．まず，エラーのない通信路上のスケーラブルCANプロトコルのモデルをSMV言語により記述し，記述したモデルが妥当であること，すなわち，所望の性質を有することをモデル検査ツールNuSMVを用いて検証する．次に，通信路をビットエラー通信路に置き換えたモデルで，再度，妥当性検証を行う．その結果として得られる反例を解析することによって，ビットエラー時にもスケーラブルCANプロトコルが正しく振る舞うように修正するための示唆を与える．