並行プロセスの理論と設計検証入門セミナー
イベント内容
セミナーの内容
マルチスレッドプログラミングや組込みシステムのように，複数のコンポーネントが並行に動作するシステムの設計は難しいといわれています．このセミナーでは並行に動作するコンポーネントからなるシステム（並行システム）の設計を支援する理論と設計検証の基礎について，ツールを使いながら学びます．
このセミナーで習得できる技術は設計検証の技術です．設計した並行システムが期待した振る舞いを持っていること，つまり要求や仕様を満たしているということをツールを使って設計段階で検証する技術を学ぶことができます．
- はじめに「設計したシステムが仕様を満たしているとはどういうことなのか」といった基本的な概念について，理論を背景に明確にします．
- つづいてツールの使い方を解説します．ポイントは4つです．(1) モデル化 (2) 振る舞いの確認 (3) 検査 (4) 誤りの分析
- キューやセマフォといった並行システムの基本的な構成要素と，それらを使った具体的なシステムの例について設計検証の演習を行います．
基礎とするのはプロセス代数と呼ばれる分野に属する CSP (Communicating Sequential Processes) という理論です．CSP は クイックソートの発明やプログラムの検証理論である Hoare 論理で有名な Tony Hoare さんによって提唱された理論です．テキストでは数学的になりがちな CSP の理論を，ほとんど数式を使わずに正確に解説します．さらにツールを使って視覚的に体験することで理解を深めることができます．
プログラム
A. 理論 10:30 - 12:00
- 並行プロセスとは何か
- 相互作用とは何か（イベント同期）
- 並行プロセスにはどんな性質があるのか（デッドロック，ライブロック，非決定性）
- 振る舞いとは何か
- 正当性とは何か（安全性，ライブネス）
- 検証の方法
（昼休憩 12:00 - 13:00）
B. ハンズオン 13:00 - 17:30
- ツールの基本操作
- 基本的なプロセスの観察
- キュー
- 共有変数
- ミューテックスによる排他制御
- セマフォによるリングバッファ
※ 対話による理解の浸透を重視するため，進捗によっては一部予定を変更する場合があります．
講師について
株式会社PRINCIPIA 代表取締役 初谷 久史
CSP 理論に基づいた対話的モデリング・検査ツール SyncStitch 開発者． 国立情報学研究所トップエスイープロジェクト「並行システムの検証と実装」講師．
セミナー参加の特典
セミナーに参加された方には，ツール SyncStitch のパーソナルライセンス（1年間有効，個人のみ使用可，商用利用不可）をご提供させていただきます．
セミナー参加の前提条件
前提知識
前提として必要な知識は，プログラミングの知識と状態遷移モデル（オートマトン）の知識です．マルチスレッド（プロセス・タスク）のプログラムを書いたことがあるという程度の知識を仮定します．排他制御といった概念やミューテックス，セマフォといった同期のための機構についての知識を仮定します．
数学については，高校で習うレベルの集合の考え方と記法（要素 x ∈ A，部分集合 A ⊆ B など）を使います．
必要なもの
以下で説明するツールがインストールされたノートPCが必要です．外付けマウスの準備を強く推奨します．
ツール
このセミナーでは SyncStitch というツールを使用します．SyncStitch は CSP 理論を基礎とする対話的モデリング・検査ツールで，いわゆるモデル検査ツールと呼ばれるツールの1つです．
セミナー参加者には事前にツールの準備をしていただく必要があります．ツールは以下のサイトからダウンロードできます．
インストールの手順についてはこちらをご覧ください．
セミナー当日までに，ツールのインストールと動作確認をお願いします．セミナー当日にインストールする時間は用意されていません．
ツールは MS-Windows 版と Linux 版があります．MS-Windows 版では Windows Subsystem for Linux が必要です．環境によっては正常に動作しない可能性があるので，ツールの動作確認を行ってから参加登録することを強くお勧めします．
ツールのインストールに関するご質問は isaac@principia-m.com までお気軽にお尋ねください．
注意事項
- 本セミナーで行う設計検証は，ツール上で記述した抽象的なモデルに対して行うものです．既存のソースコードを検証するものではありません．
- 昼休憩時にセミナーを行う場所での飲食は可能ですが，ゴミはすべてお持ち帰りいただくことになります．
参考情報
設計検証の事例
SyncStitch による設計検証の事例をご紹介しておきます．このようなことができるという雰囲気を感じていただくためです．セミナーで扱う内容よりもレベルの高いものになります．
並行システムの理論 CSP の紹介資料とビデオ
並行システムの理論 CSP の紹介資料とビデオです．本セミナーよりも高度な内容になります．ビデオは本セミナー講師による発表のものです．
形式手法の紹介資料
本セミナーは，いわゆる形式手法の1つである（広い意味での）モデル検査という分野に属します．形式手法全般と，その中でのモデル検査の位置づけについての参考となる資料をご紹介しておきます．SyncStitch の紹介も含まれています．
注意事項
※ 掲載タイミングや更新頻度によっては、情報提供元ページの内容と差異が発生しますので予めご了承ください。
※ 最新情報の確認や参加申込手続き、イベントに関するお問い合わせ等は情報提供元ページにてお願いします。
