[IT3-1305] リアルタイムOS検証演習

ねらい / Aim

  • 車載ソフトウェアなどの機能安全規格で求められている
    形式手法を実用可能な技術にする / apply formal methods, which are required in some functional safety standards

演習の目標 Mission

  • Find a bug in the implementation of a real Real-Time Operating System
    実際のリアルタイムOSのバグを発見する

手段 Means

  • Formal methods, including model checking
    モデル検査をはじめとする形式手法

概要 Overview

  • 2単位
  • 名古屋大学との共同実施
    collaborative work with Nagoya university
  • 集中講義+PBL演習+名古屋大学での発表

スケジュール Schedulre

  • 2013年度第一回目開催
    • 集中講義 / Intensive lectures
      • 8月6日(火)午後
      • 8月12日(月)午後
    • (演習前半)
    • 中間レビュー会および特別講義 /
      Interim meeting and a special lecture
      • 8月30日(金)
      • 名古屋大学から講師を招聘予定
    • (演習後半)
    • 最終報告回 / Final report meeting
      • 9月27日(金)
      • 名古屋大学にて開催
  • 2013年度第二回目開催
    • 集中講義 / Intensive lectures
      • 11月1日(金)13:30-18:20
      • 11月5日(火)15:00-20:00
    • (演習前半)
    • 中間レビュー会および特別講義 /
      Interim meeting and a special lecture
      • 11月26日(火)15:00-18:20
      • 名古屋大学本田先生講義含む
    • (演習後半)
    • 最終報告回 / Final report meeting
      • 12月20日(金)13:30-16:40
      • 名古屋大学にて開催

関連URL

将棋ソフト、初めて現役男性プロ棋士破る 
http://www.nikkei.com/article/DGXNASDG3002J_Q3A330C1CR8000/

担当教員

高井(takai@is.naist.jp)