情報科学科の計算機科学概論の最後の二回分を担当して，科学技術者倫理を担当することになりました．まずは，初回の技術者倫理について．

まずは中央自動車道のトンネル事故の例を出して，社会基盤の事故が国民生活に与える深刻な影響を思い出してもらいました．トンネル事故が国民生活に与えた影響は大きいのですが，情報科学の分野からはするとかなり意識の遠くにあるものです．でも，情報化社会になって情報システムが社会のすみずみにまで入りこんでいる現状で，情報基盤の事故は死亡事故に直結する事例はあまりないものの，大きな影響が出ています．

この日の前半では，情報基盤における大きな事故の例とその原因，もしかすると国民の生命にもかかわる影響について紹介し，情報基盤開発の信頼性を評価するための国際標準について説明しました．この国際標準で最も高いレベルでは，ソフトウェアの仕様を形式的手法によって記述し，その信頼性を形式的手法にもとづいて証明し，形式的手法に裏付けられたテスト手法を採用することが求められています．もちろん，このような開発手法の適用が求められるのは，軍事システムやごく一部の高度の信頼性が求められるソフトウェアです．

授業の後半では，形式的な手法の事例を中心に紹介していきました．最初は四色定理を始めとする，数学の定理の長大な証明を形式化した事例などです．後半の後半では，このような形式手法をソフトウェアの信頼性の証明への応用を紹介しました．

ちなみに，seL4という実時間オペレーティングシステムの形式的証明の場合，プログラム一行あたり700ドルかかったそうです．それでも，従来の手法だと1000ドルかかるので，効率的なんだそうです．

スライドを楽しんでいただいた方は，授業での配布資料もご覧下さい．スライドのネタとなった文献リストも含まれています．