ソフトウェア基礎科学（2006年度）

• 担当教員：小林直樹(内線7177)，住井英二郎
• 講義日：金曜３時限
• 講義室：情報科学研究科棟中講義室
• 休講の予定：1/19（金）
• 成績：試験とレポートで総合的に判断する。 試験は，2/2（金）13:00〜14:30に中講義室にて行う。ノート等の持ち込みは不可。
  • 試験の問1の解答例と講評
  • 試験の問2〜問5の解答例と解説
• 講義内容： 本年度は，並行プログラムや並行システムの記述・検証に用いる標準的な 計算モデルであるCCS, π計算について解説します．
• 講義に関する質問，問い合わせ先（小林担当分）： soft-kiso at kb dot ecei dot tohoku dot ac dot jp (at を"@"で，dot を"."でおきかえること）
• 教科書等：
  • Robun Milner, Communicating and mobile systems: the π-calculus, Cambridge University Press
  • Robin Milner, Communication and Concurrency, Prentice Hall
• 参考ソフトウェア
  • Concurrency Workbench of the New Century

    CCSのプロセスや様相μ計算の論理式を記述し，プロセスの等価性や論理式の充足性について調べることができるツール．プロセスの遷移をシミュレートしてくれる機能もあり．Windows, Linux, Solarisマシンへの インストールは容易．

• 講義関連資料
  • CCSに関する参考資料
  • Concurrency Workbench for the New Century 用の alternating bit protocolの記述例
  • Concurrency Workbench for the New Century 用の Petersonの排他制御アルゴリズムの記述例
  • Concurrency Workbench for the New Century 用の 「２つのプロセスが同時にクリティカルセクションに入ることはない」という仕様の記述例 （mutexが正しい仕様でmutex_wrongは間違った仕様）
• 講義を受ける上での注意事項
  • （大学初等教育レベルの）数学（特に情報数学），論理学の基本知識を持っていることを前提とする． 例えば，関数，2項関係，関係の合成，関係の反射推移的（reflexive transitive closure）， 同値関係 などの定義，論理記号（∀，∃）の意味を知らない人は，離散数学や情報数学の 入門書に目を通すこと．（電気情報系の学生なら，情報数学や情報論理学の講義でやっているはず．） これらのことを全く習っていない人は，早めに担当教員に相談すること．
  • わからないことがあれば講義の途中でも積極的に質問をすること．
  • 前回の講義の復習をしてから次回の講義に望むこと． 講義の冒頭で簡単な復習はするが，基本的な定義，用語は各自で確認しておくこと．
• レポート課題と解答例（小林出題分．１〜2回までは住井先生出題）
  • 第2回レポートの解答例
  • 第3回レポート（締切り：12月22日(金)）

    講義で扱った容量が2のバッファを容量が1のバッファを２つつなげて実現する例について、 実装（Sys）と仕様（Spec）がweak bisimulationの関係にあることを示せ。 （(Sys,Spec)を含むweak bisimulationを図または数学の2項関係の記法を用いて示せばよい）。 Sys とSpecの正確な定義はこちら。

  • 第4回レポート（締切り：1月26日(金) 注：締切りを延しました）

    講義で扱ったalternating bit protocol を以下のように変更した場合にプロトコルとして 正しく振る舞うかを答えよ（yes/noの答えだけでなく、理由または Concurrency Workbenchを用いた 検証結果をつけて答えよ．Concurrency Workbench用のalternating bit protocolの記述例は こちら）． 講義でやった送信者側と受信者側のプロトコルの記述はこちら

    • 1. 受信側のタイムアウト（+τ.Reply_b の部分）を削除した場合
    • 2. 送信側のタイムアウト（+τ.Sending_ib の部分）を削除した場合
    • 3. 受信側と送信側のタイムアウトを共に削除した場合
• レポートについて（電子的に提出することを推奨する．紙で提出する場合は講義の前後に教員に直接手渡し）
  • 提出先： soft-kiso at kb dot ecei dot tohoku dot ac dot jp (at を"@"で，dot を"."でおきかえること）
  • レポートの形式：
    • Subject: に report01: <学籍番号>のように，レポート番号，学籍番号を記入
    • 本文の最初にも，レポート番号，学籍番号，氏名を記入
    • レポート本体は，テキスト形式が望ましい．やむをえない場合（グラフをつけなければならない等の 場合）には，PDFまたはポストスクリプトでも可． Wordファイル(.doc)，latexのsource file等は不可
    • レポートには，問題に対する解答だけでなく，どうやってその解答を得たのかの説明もつけること． プログラムにはコメントもつけること． プログラムの実行結果，実行時間等をつける場合には，実行した環境（特に自宅のパソコンなどで実行した場合）も記述すること．