Registration info |
一般 ¥3000 (Pre-pay)
FCFS
|
---|---|
About Prepayment |
About Prepayment Contact Info: (Only shown to attendees.) |
Cancel/Refund Policy: お申し込み後のキャンセルはできません.セミナーについての説明をよくお読みいただき,十分ご検討の上お申し込みください.お支払いいただくのは資料(スライド資料とモデルファイル)の代金です. |
|
Print receipt data: 発行しない (詳しくはこちら) |
Description
セミナーの内容
第2回のテーマは相互作用と並行合成です.はじめにプロセス間相互作用とは何かについて改めて考察します.プロセス間相互作用を適切に定めると,プロセスを合成することができるようになり,システム全体の振る舞いが自動的に決定することがわかります.
第2回 プログラム
- プロセス間相互作用
- 同期とインターリーブ
- イベント同期による相互作用
- チャネル通信
- 並行合成
- 相互作用のモデル化:バッファとキュー
シリーズの構成
- 第1回 プロセスのモデル化
- 第2回 相互作用と並行合成
- 第3回 デッドロック
- 第4回 part 1: 内部遷移・隠蔽・非決定性・発散,part 2: 振る舞いとは何か
- 第5回 part 1: 正当性,part 2: トレース集合による安全性検査
- 第6回 安定失敗集合による正当性検査
講師について
株式会社 PRINCIPIA 代表取締役 初谷 久史
CSP 理論に基づいたモデリング・検査ツール SyncStitch 開発者
国立情報学研究所トップエスイープロジェクト「並行システムの設計検証」講師
セミナー参加の前提条件
前提知識
前提として必要な知識は,プログラミングの知識と状態遷移モデル(オートマトン)の知識です.マルチスレッド(プロセス・タスク)のプログラムを書いたことがあるという程度の知識を仮定します.排他制御といった概念やミューテックス,セマフォといった同期のための機構についての知識を仮定します.
一部,発展的な内容に関する部分では,高校で習う程度の集合の記法(要素 x ∈ A,部分集合 A ⊆ B など)を使います.
必要なもの
- PC(マウスが必要です)
- ツール SyncStitch https://github.com/hatsugai/SyncStitch/releases
Zoom URL
CONNPASS のメッセージにてお知らせします。
配布物
スライド資料(PDF)とモデルファイルを CONNPASS のメッセージにて配布します.
使用するツール
CSP 理論に基づいたモデリングと検査が可能な SyncStitch というツールを使用します.このツールで学んだ考え方と記法は他のツール(FDR, PAT, LTSA, ProB)でも活用できます(※これらのツール間でも細かい差異はあります).
注意事項
- 配布スライド資料の公開は禁止です.
- 各回を2回ずつ開催します.都合の良い回を選んで参加してください.申し込み後に都合が悪くなってもう一方の回に参加したい場合,別の曜日の回には申し込まずにご連絡ください.もう一方の回に参加できるよう調整します.2重に申し込みをしても一方はキャンセルできません.
参考書
連絡先
ご質問等がありましたら isaac@principia-m.com までお気軽にご連絡ください.
Media View all Media
If you add event media, up to 3 items will be shown here.