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

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

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

May

9

マルチスレッドプログラムのモデリングと検証の技術

旧タイトル:並行システムの設計検証

Organizing : 株式会社 PRINCIPIA

Hashtag :#SyncStitch
Registration info

一般

8000 (Pre-pay)

FCFS
5/10

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 の理論を,ほとんど数式を使わずに正確に解説します.さらにツールを使って視覚的に体験することで理解を深めることができます.

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

プログラム

プロセスのモデル化

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

相互作用と並行合成

  • プロセス間相互作用とは何か?
  • 並行合成
  • チャネル通信
  • バッファ
  • キュー
  • 共有メモリ
  • ミューテックス
  • デッドロック

内部遷移・非決定性・発散

  • 内部遷移・内部イベント
  • 非決定性
  • 発散(ライブロック)

プロセスの振る舞いと正当性

  • トレース
  • 拒否
  • 正当性の条件
  • 安全性・活性(ライブネス)

トレース集合による安全性検査

  • トレース検査
  • 事例:ランデブ

失敗集合による正当性検査

  • 失敗検査
  • 事例:リングバッファ

※ 進捗に応じて,一部内容をスキップさせていただく場合があります.

講師について

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

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

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

セミナー参加の前提条件

前提知識

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

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

必要なもの

  • ツールがインストールされたノート PCとマウス
  • Zoom ミーティングに参加するための機材(マイク・イヤホン等)

Zoom URL

CONNPASS のメッセージにてお知らせします。

配布物

スライド資料(PDF)とモデルファイルを CONNPASS のメッセージにて配布します.

使用するツール

CSP 理論に基づいたモデリングと検査が可能な SyncStitch というツールを使用します.このツールで学んだ考え方と記法は他のツール(FDR, PAT, LTSA, ProB)でも活用できます(※これらのツール間でも細かい差異はあります).

注意事項

  • 配布スライド資料の公開は禁止です.配布モデルファイルはご自由にお使いください.
  • 2020年4月25日に行われた「並行システムの設計検証入門」の改題です。内容は同じです。

参考書

連絡先

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

Media View all Media

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

Ended

2020/05/09(Sat)

12:00
18:00

You cannot RSVP if you are already participating in another event at the same date.

Registration Period
2020/04/22(Wed) 00:00 〜
2020/05/09(Sat) 11:30

Location

Zoom

オンライン

Zoom

Organizer

Attendees(5)

hirofumi

hirofumi

マルチスレッドプログラムのモデリングと検証の技術 に参加を申し込みました!

kento

kento

マルチスレッドプログラムのモデリングと検証の技術 に参加を申し込みました!

takasek

takasek

マルチスレッドプログラムのモデリングと検証の技術 に参加を申し込みました!

tacke_jp

tacke_jp

マルチスレッドプログラムのモデリングと検証の技術 に参加を申し込みました!

asya-kawai

asya-kawai

マルチスレッドプログラムのモデリングと検証の技術 に参加を申し込みました!

Attendees (5)