ビットエラー通信路におけるスケーラブルCANの動作解析

摘要

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