[前へ戻る]
   

 授業科目
 Course Title
プログラム意味論
Programming Semantics
 担当者
 Instructor
教授   木下 佳樹  前学期 金曜日2時限
講師   武山 誠  前学期 金曜日2時限
 単 位
 Credit
2

到達目標 Target to be Reached
システム妥当性確認に関する基本的な理解を得ること

 
授業内容 Course Content
本年度は、2015年度まで、8年間にわたって担当者らが続けてきた研究プロジェクトに関する結果を紹介する。以下の項目について講義する。
1) システムの確実性(assurance)、検証と妥当性確認(verification and validation)。
2) システムのディペンダビリティ。開放情報システム。 開放情報システムに関するディペンダビリティ(Open systems dependability, OSD)
3) 確実性表明(assurance case)の構造と内容。
4) 構造化された確実性表明(structured assurance case). GSN (Goal Structured Notation), CAE model (Claim, Argument and Evidence)
5) 形式化された確実性表明(formalised assurance case). FACIA (Formal Assurance Case In Agda)
6) OSDに関する確実性表明。FFO (Formal assurance case Framework for Open systems dependability) の構造と内容。
7) 自動車機能安全のための開発ライフサイクルモデル
8) 防災システムのライフサイクルモデル
 
授業計画 Course Planning
1. 概論。検証(verification)と妥当性確認(validation)。
2. システムの確実性(assurance)。確実性表明(assurance case)の構造と内容。
3. 形式理論と命題論理の自然演繹
4. 構造化された確実性表明。GSNおよびCAEによる確実性表明と自然演繹。
5. Agda言語。
6. Agdaによる形式理論の記述。
7. Agdaによる形式アシュランスケース記述フレームワークFACIAと証明記述との対応。
8. システムのディペンダビリティ。開放情報システム。 開放情報システムに関するディペンダビリティ(Open systems dependability, OSD)
9. OSDに関する確実性表明。FFO (Formal assurance case Framework for Open systems dependability) の構造と内容。
10. 自動車車載システムへの応用I。ISO26262によるシステム開発モデル。
11. 自動車車載システムへの応用II。AFSCF (Automobile Functional Safety Case Framework)の構造と内容。
12. 演習I
13. 地域防災計画への応用I。災害対策基本法にもとづく防災システムとISO/IEC/IEEE 15288に基づくシステムライフサイクル。
14. 地域防災計画への応用II。6W1HおよびDPPにもとづく地域防災計画ライフサイクルモデル。
15. 演習II
 
授業運営 Course Management
講義と演習による。人数によってはセミナー形式とする。随時レポートを提出させる。

 
評価方法 Evaluation Method
講義と演習による。人数によってはセミナー形式とする。随時レポートを提出させる。
 
オフィスアワー Office Hour (s)
金曜日13:30-15:00 2-226 (木下)
 


 
 
 
[前へ戻る]