@inproceedings{oai:ipsj.ixsq.nii.ac.jp:00086022,
 author = {青木, 利晃 and 佐藤, 信 and 谷, 充弘 and 矢竹, 健朗 and Toshiaki, Aoki and Makoto, Satoh and Mitsuhiro, Tani and Kenro, Yatake},
 book = {組込みシステムシンポジウム2012論文集},
 month = {Oct},
 note = {車載ソフトウェアの安全性や信頼性に関する問題は，社会において非常に大きな関心となりつつある．最近では，車載システムに特化された機能安全の世界標準も策定されており，実社会では，トヨタ車の電子スロットル制御システムの検証が NASA により実施されたという事案も生じている．このような問題を背景に，我々は，車載オペレーティングシステムの検証手法の研究と実践を行っている．我々が対象としている OS は， OSEK/VDX に準拠するものである．本論文では，モデル検査とテスト手法を組み合わせて，設計検証から実装のテストまでシームレスに検証を行う手法，および，実際の製品への適用について紹介する．, The safety and reliability of automotive systems are becoming a big concern in our daily life. Actually, a functional safety standard which is specilized in automotive systems has been proposed by ISO. In addition, electorical throttle systems have been inspected by NASA due to the unintended acceleration problem of Toyota's cars. To follow such recent circumstance, we are studying about practical vericiation of automotive operating systems. The operating system which we focus on is the one conforming OSEK/VDX standard. In this paper, we show an approach to seamlessly connect design verification with implementation testing based on model checking, and its application to a real product.},
 pages = {178--187},
 publisher = {情報処理学会},
 title = {モデル検査とテストによる車載オペレーティングシステムのシームレスな検証},
 volume = {2012},
 year = {2012}
}