※ connpass からお申し込みができない場合、isaac@principia-m.com までご連絡ください。

セミナーの内容

第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 までお気軽にご連絡ください。