お知らせ 【重要なお知らせ】iOSアプリの運用および提供を2024年6月3日(月)を以て終了いたします。詳細は お知らせをご覧ください。

お知らせ connpassではさらなる価値のあるデータを提供するため、イベントサーチAPIの提供方法の見直しを決定しました。2024年5月23日(木)より 「企業・法人」「コミュニティ及び個人」向けの2プランを提供開始いたします。ご利用にあたっては利用申請及び審査がございます。詳細はヘルプページをご確認ください。

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

Apr

28

並行システムの設計検証入門セミナー

ツールを使いながら並行システムの基礎を学ぶハンズオンセミナーです.

Organizing : 株式会社 PRINCIPIA

並行システムの設計検証入門セミナー
Hashtag :#SyncStitch
Registration info

一般

9000 (Pre-pay)

FCFS
2/10

Attendees
TakayukiTakeuchi
negi23
View Attendee List
Start Date
2024/04/28(Sun) 12:00 ~ 18:00
Registration Period

2024/04/03(Wed) 00:00 〜
2024/04/28(Sun) 12:00まで

Location

Zoom

オンライン

About Prepayment

About Prepayment Contact Info:

(Only shown to attendees.)

Cancel/Refund Policy:

お申込み後のキャンセルはできません。セミナーについての説明をよくお読みいただき、十分ご検討の上お申し込みください。

Print receipt data:

発行しない (詳しくはこちら)
出席登録
(イベント開始時間の2時間前から終了時間まで、参加者のみに公開されます)

Description

セミナーの内容

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

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

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

基礎とするのはプロセス代数と呼ばれる分野に属する CSP (Communicating Sequential Processes) という理論です。CSP は クイックソートの発明やプログラムの検証理論である Hoare 論理で有名な Tony Hoare さんによって提唱された理論です。教科書では数学的になりがちな CSP の理論を、ほとんど数式を使わずに正確に解説します。さらにツールを使って視覚的に体験することで理解を深めることができます。

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

プログラム

プロセスのモデル化

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

相互作用と並行合成

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

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

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

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

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

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

  • トレース検査
  • 事例:リーダ・ライタ問題

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

  • 失敗検査
  • 事例:イベントオブジェクトによる通信キューの実装

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

講師について

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

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

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

セミナー参加の前提条件

前提知識

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

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

必要なもの

  • ツール SyncStitch がインストールされた MS-Windows PC (マウスが必須です)

以下のページの Releases から syncstitch-4.3.1-win.zip をダウンロードしてください。

https://github.com/hatsugai/SyncStitch

mac, Linux でもビルドすれば動作しますが、当方で動作確認ができないため、サポート外とさせていただきます。ご自分でリスクを取られる分にはかまいません。

配布物と Zoom meeting URL

セミナー開始時刻までにCONNPASS のメッセージにてお知らせします。

同じメッセージを複数回送信する場合があります。あらかじめご了承ください。

使用するツール

CSP 理論に基づいたモデリングと検査が可能な SyncStitch というツールを使用します。

注意事項

  • 配布スライド資料の公開は禁止です。配布モデルファイルはご自由にお使いください。
  • 不測の事態が生じセミナーを開催または完遂できなかった場合は、日を改めて再開催することで対処させていただきます。
  • 都合により申し込み後に参加できなくなった場合は、同等のセミナーを再演する際にご参加いただけるよう配慮しますのでご連絡ください。

参考書

連絡先

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

Media View all Media

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

Feed

hatsugai

hatsugai published 並行システムの設計検証入門セミナー.

04/03/2024 19:00

並行システムの設計検証入門セミナー を公開しました!

Ended

2024/04/28(Sun)

12:00
18:00

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

Registration Period
2024/04/03(Wed) 00:00 〜
2024/04/28(Sun) 12:00

Location

Zoom

オンライン

Zoom

Organizer

Attendees(2)

TakayukiTakeuchi

TakayukiTakeuchi

並行システムの設計検証入門セミナー に参加を申し込みました!

negi23

negi23

並行システムの設計検証入門セミナー に参加を申し込みました!

Attendees (2)