募集内容 |
一般 3000円(前払い)
先着順
|
---|---|
申込者 | 申込者一覧を見る |
開催日時 |
2020/07/08(水) 21:00 ~ 22:30
|
募集期間 |
2020/06/21(日) 00:00
〜 |
会場 |
Zoom オンライン |
前払いについて |
前払いについての連絡先: (参加者にのみ公開されます) |
キャンセル・参加費用の払い戻しについて主催者からの説明: お申し込み後のキャンセルはできません.セミナーについての説明をよくお読みいただき,十分ご検討の上お申し込みください.お支払いいただくのは資料(スライド資料とモデルファイル)の代金です. |
|
領収データの発行: 発行しない (詳しくはこちら) |
イベントの説明
セミナーの内容
第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 までお気軽にご連絡ください.
資料 資料をもっと見る/編集する
資料が投稿されると、最新の3件が表示されます。