@techreport{oai:ipsj.ixsq.nii.ac.jp:00027223,
 author = {山口, 聖二 and 伊地知, 孝仁 and 谷本, 匡亮 and 中田, 明夫 and 東野, 輝夫 and Seiji, Yamaguchi and Takahito, Ijichi and Tadaaki, Tanimoto and Akio, Nakata and Teruo, Higashino},
 issue = {122(2004-SLDM-117)},
 month = {Dec},
 note = {本稿では，主に車内通信などに利用されているシリアスバスプロトコルであるCAN (Control Area Network)プロトコルについて，実時間制約検証を効率よく行うことができるような仕様を抽象化したモデルを提案する．提案モデルでは，メッセージ送信時のバス使用権の取得や通信におけるエラー発生時の処理，クロックサイクル消費の扱いなどの点で抽象化を行う．その結果，実際のシステムでバス上を流れる波形を考慮する必要がなくなるため，検証の高速化を実現できる．また，静的解析と異なり，具体的なバス通信動作および通信エラー処理をシミュレート可能である．提案する抽象化モデルに基づいて，ユニット毎の動作記述，バスクロック単位での動作確認が可能なシミュレータを試作する．試作したシミュレータを文献[5]の例題に適用し，シミュレーション結果を比較することによち，提案モデルの有効性を示す．, In this paper, we propose a model for CAN (Control Area Network) protocol, which is a serial bus protocol mainly used for the communications in car system. Our model is an abstraction of the specification of CAN protocol, aimed at improving performance of dynamic verification (simulation) of real-time constraints for bus communication. In our proposed model, we abstract bus arbitration, error handling, and clock cycle handling. By the proposed abstraction, we need not perform a costly waveform simulation. Moreover, unlike static analyses, we can also check correctness of the system behavior in the presence of bus communication errors by simulation. We have implemented a simulator based on our proposed abstracted model. In the simulator, we can specify a concrete I/O behavior for each unit of a bus system, enabling us to check whether real-time constraints are satisfied in the specified behavior setting, as well as influence of bus communication errors. We present some experimental results to show that our abstraction is appropriate and effective for the real-time constraint verification.},
 title = {実時間制約検証に特化したCANバスモデルの提案とシミュレータの試作},
 year = {2004}
}