並行システムの設計検証入門セミナー
イベント内容
セミナーの内容
マルチスレッドプログラミングや組込みシステムのように、複数のコンポーネントが並行に動作するシステムの設計は難しいといわれています。このセミナーでは並行に動作するコンポーネントからなるシステム（並行システム）の設計を支援する理論と設計検証の基礎について、ツールを使いながら学びます。
このセミナーで習得できる技術は設計検証の技術です。設計した並行システムが期待した振る舞いをもっていること、つまり要求や仕様を満たしているということをツールを使って設計段階で検証する技術を学ぶことができます。
「手を動かせば理解は後からついてくる」という考えかたで進めます。まずはツール上で手を動かし、視覚的なフィードバックを得ることが理解への早道であると考えます。理論をていねいに説明しますが、概念の獲得というのは時間のかかるものです。もし理解に不安が生じても、ツール上で確認する手段を持っていれば確信をもって自分の考えを進めることができるでしょう。
基礎とするのはプロセス代数と呼ばれる分野に属する CSP (Communicating Sequential Processes) という理論です。CSP は クイックソートの発明やプログラムの検証理論である Hoare 論理で有名な Tony Hoare さんによって提唱された理論です。教科書では数学的になりがちな CSP の理論を、ほとんど数式を使わずに正確に解説します。さらにツールを使って視覚的に体験することで理解を深めることができます。
CSP に基づくシステムの振る舞いの記述は形式仕様記述の一種になります。広く知られている状態に基づいた仕様記述とは少し異なり、状態遷移に付随する相互作用の方に力点を置く記述方法になります。これを体験するとシステムの振る舞いに対する新たな視点を手に入れることができます。対象とするシステムの性質によって適切な記述形式を選択する自由度を増やすことができるでしょう。
プログラム
プロセスのモデル化
- イベント同期
- 選択
- チャネル通信
- 状態変数
- 条件分岐
- ループ
相互作用と並行合成
- プロセス間相互作用とは何か？
- 並行合成
- チャネル通信
- バッファ
- キュー
- 共有メモリ
- ミューテックス
- デッドロック
内部遷移・非決定性・発散
- 内部遷移・内部イベント
- 非決定性
- 発散（ライブロック）
プロセスの振る舞いと正当性
- トレース
- 拒否
- 正当性の条件
- 安全性・活性（ライブネス）
トレース集合による安全性検査
- トレース検査
- 事例：リーダ・ライタ問題
失敗集合による正当性検査
- 失敗検査
- 事例：イベントオブジェクトによる通信キューの実装
※ 進捗に応じて、一部内容をスキップさせていただく場合があります。
講師について
株式会社 PRINCIPIA 代表取締役 初谷 久史
CSP 理論に基づいたモデリング・検査ツール SyncStitch 開発者
国立情報学研究所トップエスイープロジェクト「並行システムの設計検証」講師
セミナー参加の前提条件
前提知識
前提として必要な知識は、プログラミングの知識と状態遷移モデル（オートマトン）の知識です。マルチスレッド（プロセス・タスク）のプログラムを書いたことがあるという程度の知識を仮定します。排他制御といった概念やミューテックス、セマフォといった同期のための機構についての知識を仮定します。
一部、発展的な内容に関する部分では、高校で習う程度の集合の記法（要素 x ∈ A, 部分集合 A ⊆ B など）を使います。
必要なもの
- ツール SyncStitch がインストールされた MS-Windows PC （マウスが必須です）
以下のページの Releases から syncstitch-4.3.1-win.zip をダウンロードしてください。
https://github.com/hatsugai/SyncStitch
mac, Linux でもビルドすれば動作しますが、当方で動作確認ができないため、サポート外とさせていただきます。ご自分でリスクを取られる分にはかまいません。
配布物と Zoom meeting URL
セミナー開始時刻までにCONNPASS のメッセージにてお知らせします。
同じメッセージを複数回送信する場合があります。あらかじめご了承ください。
使用するツール
CSP 理論に基づいたモデリングと検査が可能な SyncStitch というツールを使用します。
注意事項
- 配布スライド資料の公開は禁止です。配布モデルファイルはご自由にお使いください。
- 不測の事態が生じセミナーを開催または完遂できなかった場合は、日を改めて再開催することで対処させていただきます。
- 都合により申し込み後に参加できなくなった場合は、同等のセミナーを再演する際にご参加いただけるよう配慮しますのでご連絡ください。
参考書
連絡先
ご質問等がありましたら isaac@principia-m.com までお気軽にご連絡ください。
注意事項
※ 掲載タイミングや更新頻度によっては、情報提供元ページの内容と差異が発生しますので予めご了承ください。
※ 最新情報の確認や参加申込手続き、イベントに関するお問い合わせ等は情報提供元ページにてお願いします。
新規会員登録
このイベントに申し込むには会員登録が必要です。
アカウント登録済みの方はログインしてください。
※ ソーシャルアカウントで登録するとログインが簡単に行えます。
※ 連携したソーシャルアカウントは、会員登録完了後にいつでも変更できます。
