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

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

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

Jun

30

並行システムの設計検証 第1回 プロセスのモデル化

Organizing : 株式会社 PRINCIPIA

Hashtag :#SyncStitch
Registration info

一般

1000 (Pre-pay)

FCFS
10/15

About Prepayment

About Prepayment Contact Info:

(Only shown to attendees.)

Cancel/Refund Policy:

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

Print receipt data:

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

Description

セミナーの内容

マルチスレッドプログラミング,ネットワークプログラミング,組込みプログラミングのように,複数のコンポーネントが並行に動作するシステムの設計は難しいといわれています.このセミナーでは並行に動作するコンポーネントからなるシステム(並行システム)の設計を支援する理論と設計検証の基礎について,ツールを使いながら学びます.

このセミナーで習得できる技術は設計検証の技術です.設計した並行システムが期待した振る舞いをもっていること,つまり要求や仕様を満たしているということをツールを使って設計段階で検証する技術を学ぶことができます.

「手を動かせば理解は後からついてくる」というコンセプトで進めます.まずはツール上で手を動かし,視覚的なフィードバックを得ることが理解への早道であると考えます.ポイントごとに理論的な説明を行いますが,概念の獲得というのは時間のかかるものです.もし理解に不安が生じても,ツール上で確認する手段を持っていれば確信をもって自分の考えを進めることができるでしょう.

基礎とするのはプロセス代数と呼ばれる分野に属する CSP (Communicating Sequential Processes) という理論です.CSP は クイックソートの発明やプログラムの検証理論である Hoare 論理で有名な Tony Hoare さんによって提唱された理論です.断片的なノウハウの集合に過ぎなかった並行システムの設計を,理論を使うことで数学的に検証できるようになります.さらにツールを使って視覚的に体験することで理解を深めることができます.

CSP に基づくシステムの振る舞いの記述は形式仕様記述の一種になります.広く知られている状態に基づいた仕様記述とは少し異なり,状態遷移に付随する相互作用の方に力点を置く記述方法になります.これを体験するとシステムの振る舞いに対する新たな視点を手に入れることができます.対象とするシステムの性質によって適切な記述形式を選択する自由度を増やすことができるでしょう.

セミナーは全6回からなるシリーズとなります.第1回はプロセスのモデル化です.並行システムを構成する各コンポーネントの振る舞いをプロセスとしてモデル化する方法を解説します.

第1回 プログラム

  • イベント同期
  • 選択
  • チャネル通信
  • 状態変数
  • 条件分岐
  • ループ
  • 練習問題

シリーズの構成

  • 第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重に申し込みをしても一方はキャンセルできません.
  • 2020年4月25日に開催した「並行システムの設計検証入門セミナー」および2020年5月9日に開催した「マルチスレッドプログラムのモデリングと検証の技術」とほぼ同内容です。1日集中セミナーを6回に再構成したものです。

参考書

連絡先

ご質問等がありましたら isaac@principia-m.com までお気軽にご連絡ください.

Media View all Media

If you add event media, up to 3 items will be shown here.

Ended

2020/06/30(Tue)

21:00
22:30

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

Location

Zoom

オンライン

Zoom

Organizer

Attendees(10)

niszet

niszet

並行システムの設計検証 第1回 プロセスのモデル化 に参加を申し込みました!

TakeshiHori

TakeshiHori

並行システムの設計検証 第1回 プロセスのモデル化 に参加を申し込みました!

tukejonny

tukejonny

並行システムの設計検証 第1回 プロセスのモデル化 に参加を申し込みました!

RyosukeNakagawa

RyosukeNakagawa

並行システムの設計検証 第1回 プロセスのモデル化 に参加を申し込みました!

Nobu19800

Nobu19800

並行システムの設計検証 第1回 プロセスのモデル化 に参加を申し込みました!

totomaru

totomaru

並行システムの設計検証 第1回 プロセスのモデル化 に参加を申し込みました!

minekoa (みねこあ)

minekoa (みねこあ)

並行システムの設計検証 第1回 プロセスのモデル化に参加を申し込みました!

Tute

Tute

並行システムの設計検証 第1回 プロセスのモデル化 に参加を申し込みました!

kikuyuta

kikuyuta

並行システムの設計検証 第1回 プロセスのモデル化 に参加を申し込みました!

shigemi1014

shigemi1014

I joined 並行システムの設計検証 第1回 プロセスのモデル化!

Attendees (10)