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

Jul

21

並行システムの設計検証 第4回 内部遷移・隠蔽・非決定性・発散,振る舞いとは何か

Organizing : 株式会社 PRINCIPIA

Hashtag :#SyncStitch
Registration info

一般

3000 (Pre-pay)

FCFS
10/15

About Prepayment

About Prepayment Contact Info:

(Only shown to attendees.)

Cancel/Refund Policy:

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

Print receipt data:

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

Description

セミナーの内容

第4回は2つのパートからなります.

パート1のテーマは内部遷移・隠蔽・非決定性・発散です.並行システムには再現したりしなかったりする現象があることはよく知られています.その概念を明確にし発生メカニズムを解説します.さらにデッドロックと並んで並行システムに特徴的な問題であるライブロック(発散)という現象について解説します.ツール SyncStitch にはライブロックを発見する機能があります.その使い方を解説します.

パート2のテーマは「振る舞いとは何か」です.設計した並行システムが仕様を満たしているかどうかを検証するためには,まずその検証の対象であるシステムの「振る舞い」とは何かを明確にする必要があります.これについて詳細に解説します.おそらくはいままで聞いたことがない貴重な情報だと思います.

第4回 プログラム

パート1 内部遷移・隠蔽・非決定性・発散

  • 内部イベントと内部遷移
  • 隠蔽
  • 非決定性
  • 発散
  • 発散検査

パート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 96

Members 244

Ended

2020/07/21(Tue)

21:00
22:30

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

Location

Zoom

オンライン

Zoom

Organizer

Attendees(10)

niszet

niszet

並行システムの設計検証 第4回 内部遷移・隠蔽・非決定性・発散,振る舞いとは何か に参加を申し込みました!

shigemi1014

shigemi1014

I joined 並行システムの設計検証 第4回 内部遷移・隠蔽・非決定性・発散,振る舞いとは何か!

tukejonny

tukejonny

並行システムの設計検証 第4回 内部遷移・隠蔽・非決定性・発散,振る舞いとは何か に参加を申し込みました!

kikuyuta

kikuyuta

並行システムの設計検証 第4回 内部遷移・隠蔽・非決定性・発散,振る舞いとは何か に参加を申し込みました!

ゆうぞら

ゆうぞら

並行システムの設計検証 第4回 内部遷移・隠蔽・非決定性・発散,振る舞いとは何か に参加を申し込みました!

RyosukeNakagawa

RyosukeNakagawa

並行システムの設計検証 第4回 内部遷移・隠蔽・非決定性・発散,振る舞いとは何か に参加を申し込みました!

TakeshiHori

TakeshiHori

並行システムの設計検証 第4回 内部遷移・隠蔽・非決定性・発散,振る舞いとは何か に参加を申し込みました!

Nobu19800

Nobu19800

並行システムの設計検証 第4回 内部遷移・隠蔽・非決定性・発散,振る舞いとは何か に参加を申し込みました!

Tute

Tute

並行システムの設計検証 第4回 内部遷移・隠蔽・非決定性・発散,振る舞いとは何か に参加を申し込みました!

minekoa (みねこあ)

minekoa (みねこあ)

並行システムの設計検証 第4回 内部遷移・隠蔽・非決定性・発散,振る舞いとは何か に参加を申し込みました!

Attendees (10)