勉強会：【マルレク】Deep Specificationの世界
【マルレク】ソフトウェア・エンジニアリングの新しい潮流 -- Deep Specificationの世界
■ 日時：2019/9/24 19:00ｰ21:00
■ 感想
→ ソフトウェア開発の新しい徴候
SWの記述に問題が無いか(How)の検証から
SWの仕様に問題が無いか(What/Why)の記述に移行するという見方
→ AIが深化していく中で必要になる技術
10年後に価値のある技術者でいるためには必要なスキル
今から準備が必要な分野であると感じている
→ 形式手法、自動証明、欲しいSWの記述方法について
DSLとして研究していきたいと思っている
■ 開催・資料
- 講演資料 www.marulabo.net
（セミナ・メモ）
● 第一部 大規模システム開発の問題
・航空機の開発
→ 対規模事故：ボーイング737MAX → センサ異常
→ 使用ミス、コードミス → 仕様と実装の分離 → 上流/下流
→ 自動操縦
・分散システムの開発
→ Timeout/Node faluer/Msg delivery
→ Kubernetes faluer → クラスタ構成
・ハードウェア開発
→ HW設計 → 形式手法(モデルチェック) → 小さなコンポーネント
→ CPU脆弱性 → Spectre/Meltdown
→ 攻撃者 → 投機的実行
→ CPUの仕様が完全では無い → RISCV
・開発コスト
→ 開発費の高騰 → システムの変化に対応できない
→ 軍用機の開発 → 戦闘機1台 → GNP越え(既得権益)
→ DRON → 安価
・高速化
→ 人間と機械の時間のギャップ
→ 機械のコードの実行が追いつかない
→ Latency as an Effect
→ ネットワークプログラム → 実行のブロック
・開発ツールは信頼できるか？
● 第二部 Deep Specificationの世界
・ソフトウェア・エンジニアリングの展望
→ テスト・デバッグ・コードレビュー
→ 形式的手法 → プログラムの正しさを証明する
→ デバッグ/証明、テスト/仕様か、コードレビュー/仕様レビュー
・Deep Specificationとは何か？
→ 小規模な検証済みコンポーネント → 大型システムの構築
→ rich, two-sided, formai, live
→ モジュール → 動作可能な仕様
→ two-sided → CertiKOS/CompCert
→ Compsition
→ 証明エンジンの充実
・Deep Specificationのプロジェクト
→ CertikOS, Kami
→ Verified Software Toolchain
・形式的手法によるCPUとネットワークの検証
・進行中のプロジェクト
● 第三部 プログラムと論理
・形式的手法の二つの起源
・形式的手法をめぐる20世紀の「論争」
・ダイクストラの21世紀へのメッセージ
・証明支援システム Coq
・Deep Specification – Software Foundation
以上
