@techreport{oai:ipsj.ixsq.nii.ac.jp:00080903,
 author = {松原, 正裕 and 櫻井, 康平 and 成沢, 文雄 and 山中, 久光 and Masahiro, Matsubara and Kohei, Sakurai and Fumio, Narisawa and Hisamitsu, Yamanaka},
 issue = {11},
 month = {Feb},
 note = {組込み制御システムではソフトウェア規模の増大により，処理タイミングによりごくまれに発生する不具合がシミュレーション等のテストでは発見できずに潜在する恐れが高まっている．このような不具合を検出するため，非定常の挙動を含む外部環境モデルと，外部環境との境界調整が容易なソフトウェアのスライシング方式を適用してモデル検査を行う手法を考案した．本手法を自動車用ソフトウェアの非再現不具合の原因調査に適用して不具合要因を発見し，本手法の有効性を確認した．, In embedded control systems, potential risks have been increasing because of software defects caused by a timing related problem. These defects are rarely found by simulation and test. To detect such defects, we have proposed model checking application method based on external environment models with unsteady behaviors and the software slicing technique using variable dependency graphs. We have applied the proposed method to an analysis of a non-reproducible defect in automotive control software and demonstrated the usefulness of the method.},
 title = {ハードウェア異常に対応した組込み制御ソフトウェア不具合のモデル検査手法},
 year = {2012}
}