CVS

center-name

AIST
 センター長挨拶Policy Statement研究テーマ研究活動研究成果Technical Reports書籍共同研究集会支援English
 研修コースニュースレター ・CVS Staff ・アクセス 採用情報  ・お問い合わせ ・更新履歴 ・プレスリリース ・カレンダーHOME 

◆ サブ メニュー ◆
Web版 システム検証の事例報告集

Web版 トップ頁へ

▼ 一覧から探す
  1. 項目一覧

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 9: 一般公開で用いたLEGO用プログラムの検証


実施年度2006
概要 産総研一般公開でCVSは,LEGOを使って作られた車(ロボット)を 操作する簡易プログラム作成を体験する出展を行なった. 展示の際に担当者から,まれに不具合が発生し, 仕様に従った動作をしていないことが報告されたが,原因は不明であった. 不具合の原因を特定するために,モデル検査手法を適用して検証を試みた.
担当者 関澤 俊弦,崔 銀惠,竹内 泉,高橋 孝一
班名 業務項目名:Javaプログラムの検証
寄与
関連する事例

題材

領域 組み込み,アルゴリズム
題材の詳細
CVS/AISTで作成したプログラム
形態 ソースコード
言語 Java + LeJOS (LeJOSはJavaのLEGOコントロール用ライブラリ)
規模 300行位
題材の情報源 なし

検証のデータ

目的
バグ検出
検証内容
到達可能性,安全性
結果
不具合は発見できなかった
検証手法 モデル検査
モデル化法 ソースコードから手動で作成
使用ツール UPPAAL
スケジュール、
労力、時間など


備考

情報源

算譜科学研究速報
(テクニカルレポ-ト)
論文発表
口頭発表
知的財産
その他

産総研ホーム >  組織 >  研究センター >  システム検証研究センター
Copyrights (C) 2005-2010 AIST Research Center for Verification and Semantics, All Rights Reserved.