セミナーの内容

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

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

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

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

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

セミナーは全4回からなるシリーズとなります．第1回は「プロセスと相互作用」です．並行システムを構成する各コンポーネントの振る舞いをプロセスとしてモデル化しシステムを構成する方法を解説します．

プログラム

プロセスのモデル化

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

相互作用と並行合成

• プロセス間相互作用
• 同期とインターリーブ
• イベント同期による相互作用
• チャネル通信
• 並行合成
• 相互作用のモデル化：バッファとキュー

シリーズの構成

• 第1回 プロセスと相互作用
• 第2回 デッドロック・ライブロック
• 第3回 安全性検査
• 第4回 正当性検査

講師について

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

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

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

セミナー参加の前提条件

前提知識

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

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

必要なもの

• ツール SyncStitch
• マウス

配布物と Zoom meeting URL

セミナー開始時刻までにCONNPASS のメッセージにてお知らせします。

同じメッセージを複数回送信する場合があります。あらかじめご了承ください。

使用するツール

CSP 理論に基づいたモデリングと検査が可能な SyncStitch というツールを使用します。

注意事項

• 配布スライド資料の公開は禁止です。配布モデルファイルはご自由にお使いください。
• 不測の事態が生じセミナーを開催または完遂できなかった場合は、日を改めて再開催することで対処させていただきます。
• 都合により申し込み後に参加できなくなった場合は、同等のセミナーを再演する際にご参加いただけるよう配慮しますのでご連絡ください。

参考書

• 並行システムの検証と実装，磯部祥尚
• Communicating Sequential Processes, C. A. R. Hoare
• The Theory and Practice of Concurrency, A.W. Roscoe
• Concurrent and Real-time Systems: The CSP Approach, Steve Schneider
• Understanding Concurrent Systems, A.W. Roscoe

連絡先

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