セミナーの内容

マルチスレッドプログラミングや組込みシステムのように，複数のコンポーネントが並行に動作するシステムの設計は難しいといわれています．このセミナーでは並行に動作するコンポーネントからなるシステム（並行システム）の設計を支援する理論と設計検証の基礎について，ツールを使いながら学びます．

このセミナーで習得できる技術は設計検証の技術です．設計した並行システムが期待した振る舞いをもっていること，つまり要求や仕様を満たしているということをツールを使って設計段階で検証する技術を学ぶことができます．

「手を動かせば理解は後からついてくる」というコンセプトで進めます．まずはツール上で手を動かし，視覚的なフィードバックを得ることが理解への早道であると考えます．ポイントごとに理論的な説明を行いますが，概念の獲得というのは時間のかかるものです．もし理解に不安が生じても，ツール上で確認する手段を持っていれば確信をもって自分の考えを進めることができるでしょう．

基礎とするのはプロセス代数と呼ばれる分野に属する CSP (Communicating Sequential Processes) という理論です．CSP は クイックソートの発明やプログラムの検証理論である Hoare 論理で有名な Tony Hoare さんによって提唱された理論です．テキストでは数学的になりがちな CSP の理論を，ほとんど数式を使わずに正確に解説します．さらにツールを使って視覚的に体験することで理解を深めることができます．

CSP に基づくシステムの振る舞いの記述は形式仕様記述の一種になります．広く知られている状態に基づいた仕様記述とは少し異なり，状態遷移に付随する相互作用の方に力点を置く記述方法になります．これを体験するとシステムの振る舞いに対する新たな視点を手に入れることができます．対象とするシステムの性質によって適切な記述形式を選択する自由度を増やすことができるでしょう．

プログラム

プロセスのモデル化

• イベント同期
• 選択
• チャネル通信
• 状態変数
• 条件分岐
• ループ

相互作用と並行合成

• プロセス間相互作用とは何か？
• 並行合成
• チャネル通信
• バッファ
• キュー
• 共有メモリ
• ミューテックス
• デッドロック

内部遷移・非決定性・発散

• 内部遷移・内部イベント
• 非決定性
• 発散（ライブロック）

プロセスの振る舞いと正当性

• トレース
• 拒否
• 正当性の条件
• 安全性・活性（ライブネス）

トレース集合による安全性検査

• トレース検査
• 事例：ランデブ

失敗集合による正当性検査

• 失敗検査
• 事例：リングバッファ

※ 進捗に応じて，一部内容をスキップさせていただく場合があります．

講師について

株式会社 PRINCIPIA 代表取締役 初谷 久史

CSP 理論に基づいたモデリング・検査ツール SyncStitch 開発者

国立情報学研究所トップエスイープロジェクト「並行システムの設計検証」講師

セミナー参加の前提条件

前提知識

前提として必要な知識は，プログラミングの知識と状態遷移モデル（オートマトン）の知識です．マルチスレッド（プロセス・タスク）のプログラムを書いたことがあるという程度の知識を仮定します．排他制御といった概念やミューテックス，セマフォといった同期のための機構についての知識を仮定します．

一部，発展的な内容に関する部分では，高校で習う程度の集合の記法（要素 x ∈ A，部分集合 A ⊆ B など）を使います．

必要なもの

• ツールがインストールされたノート PCとマウス
• Zoom ミーティングに参加するための機材（マイク・イヤホン等）

Zoom URL

CONNPASS のメッセージにてお知らせします。

配布物

スライド資料（PDF)とモデルファイルを CONNPASS のメッセージにて配布します．

使用するツール

CSP 理論に基づいたモデリングと検査が可能な SyncStitch というツールを使用します．このツールで学んだ考え方と記法は他のツール（FDR, PAT, LTSA, ProB）でも活用できます（※これらのツール間でも細かい差異はあります）．

注意事項

• 配布スライド資料の公開は禁止です．配布モデルファイルはご自由にお使いください．
• 不測の事態によりセミナーが開催できなかった場合は，参加費用の返却にて対応させていただきます．

参考書

• 並行システムの検証と実装

連絡先

ご質問等がありましたら isaac@principia-m.com までお気軽にご連絡ください．