新機能 イベント詳細画面に「参加者への情報」欄を追加しました。イベント管理者、発表者、参加者(抽選中や補欠は除く)だけに表示されるフィールドです。詳しくはこちら

新機能 オンラインイベントが検索できるようになりました。オンラインイベントとして検索できるようにするには こちら をご確認ください

このエントリーをはてなブックマークに追加

Jul

14

並行システムの設計検証 第3回 デッドロック

Organizing : 株式会社 PRINCIPIA

Hashtag :#SyncStitch
Registration info

一般

3000 (Pre-pay)

FCFS
3/10

About Prepayment

About Prepayment Contact Info:

(Only shown to attendees.)

Cancel/Refund Policy:

お申し込み後のキャンセルはできません.セミナーについての説明をよくお読みいただき,十分ご検討の上お申し込みください.お支払いいただくのは資料(スライド資料とモデルファイル)の代金です.

Print receipt data:

発行しない (詳しくはこちら)

Description

セミナーの内容

第3回のテーマはデッドロックです.並行システムに特徴的なデッドロックはなぜ発生するのか,そのメカニズムを解説します.ツール SyncStitch にはデッドロックを検出する機能があります.その使い方を解説します.

第3回 プログラム

  • 相互作用のモデル化2:共有メモリ(共有変数)
  • ミューテックスによる排他制御
  • デッドロック
  • デッドロック検査

シリーズの構成

  • 第1回 プロセスのモデル化
  • 第2回 相互作用と並行合成
  • 第3回 デッドロック
  • 第4回 part 1: 内部遷移・隠蔽・非決定性・発散,part 2: 振る舞いとは何か
  • 第5回 part 1: 正当性,part 2: トレース集合による安全性検査
  • 第6回 安定失敗集合による正当性検査

講師について

株式会社 PRINCIPIA 代表取締役 初谷 久史

CSP 理論に基づいたモデリング・検査ツール SyncStitch 開発者

国立情報学研究所トップエスイープロジェクト「並行システムの設計検証」講師

セミナー参加の前提条件

前提知識

前提として必要な知識は,プログラミングの知識と状態遷移モデル(オートマトン)の知識です.マルチスレッド(プロセス・タスク)のプログラムを書いたことがあるという程度の知識を仮定します.排他制御といった概念やミューテックス,セマフォといった同期のための機構についての知識を仮定します.

一部,発展的な内容に関する部分では,高校で習う程度の集合の記法(要素 x ∈ A,部分集合 A ⊆ B など)を使います.

必要なもの

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.

Group

PRINCIPIA

Number of events 47

Members 180

Public

2020/07/14(Tue)

21:00
22:30

Please login to register

Registration Period
2020/06/21(Sun) 00:00 〜
2020/07/14(Tue) 20:30

Location

Zoom

オンライン

Zoom

Organizer

Attendees(3)

tukejonny

tukejonny

並行システムの設計検証 第3回 デッドロック に参加を申し込みました!

niszet

niszet

並行システムの設計検証 第3回 デッドロック に参加を申し込みました!

kikuyuta

kikuyuta

並行システムの設計検証 第3回 デッドロック に参加を申し込みました!

Attendees (3)