新機能 イベントメッセージの予約機能を追加しました。イベント主催者様は、参加者へのメッセージ送信を事前に予約できます。詳しくはこちらをご確認ください。

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

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

Jul

29

並行システムの設計検証 第5回 正当性,トレース集合による安全性検査

Organizing : 株式会社 PRINCIPIA

Hashtag :#SyncStitch
Registration info

一般

3000 (Pre-pay)

FCFS
4/10

About Prepayment

About Prepayment Contact Info:

(Only shown to attendees.)

Cancel/Refund Policy:

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

Print receipt data:

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

Description

セミナーの内容

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

パート1のテーマは正当性です.設計した並行システムのモデルが仕様を満たしているとはどういうことかということを改めて解説します.入出力で特徴づけられる計算するプログラムとは異なり,ユーザや他のシステムと継続的に相互作用(通信)するシステムの正当性についての解説は貴重なものだと思います.

パート2のテーマはトレース集合による安全性検査です.ツールを使って安全性検査を行う方法と事例を紹介します.

第5回 プログラム

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

Ended

2020/07/29(Wed)

21:00
22:30

Registration Period
2020/06/21(Sun) 00:00 〜
2020/07/29(Wed) 20:30

Location

Zoom

オンライン

Zoom

Organizer

Attendees(4)

yutk

yutk

並行システムの設計検証 第5回 正当性,トレース集合による安全性検査 に参加を申し込みました!

tukejonny

tukejonny

並行システムの設計検証 第5回 正当性,トレース集合による安全性検査 に参加を申し込みました!

TakeshiHori

TakeshiHori

並行システムの設計検証 第5回 正当性,トレース集合による安全性検査 に参加を申し込みました!

totomaru

totomaru

並行システムの設計検証 第5回 正当性,トレース集合による安全性検査 に参加を申し込みました!

Attendees (4)