6月

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

主催 : 株式会社 PRINCIPIA

ハッシュタグ：#SyncStitch

募集内容	一般 1000円（前払い）先着順 10/15人
申込者	申込者一覧を見る
開催日時	2020/06/30(火) 21:00 ～ 22:30 Googleカレンダー icsファイル
募集期間	2020/06/21(日) 00:00 〜 2020/06/30(火) 20:30まで
会場	Zoom オンライン
前払いについて	前払いについての連絡先: (参加者にのみ公開されます)
	キャンセル・参加費用の払い戻しについて主催者からの説明: お申し込み後のキャンセルはできません．セミナーについての説明をよくお読みいただき，十分ご検討の上お申し込みください．お支払いいただくのは資料（スライド資料とモデルファイル）の代金です．
	領収データの発行: 発行しない (詳しくはこちら)

イベントの説明

セミナーの内容

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

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

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

基礎とするのはプロセス代数と呼ばれる分野に属する 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 など）を使います．

必要なもの

PC（マウスが必要です）
ツール SyncStitch https://github.com/hatsugai/SyncStitch/releases

Zoom URL

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

配布物

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

使用するツール

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

注意事項

配布スライド資料の公開は禁止です．
各回を2回ずつ開催します．都合の良い回を選んで参加してください．申し込み後に都合が悪くなってもう一方の回に参加したい場合，別の曜日の回には申し込まずにご連絡ください．もう一方の回に参加できるよう調整します．2重に申し込みをしても一方はキャンセルできません．
2020年4月25日に開催した「並行システムの設計検証入門セミナー」および2020年5月9日に開催した「マルチスレッドプログラムのモデリングと検証の技術」とほぼ同内容です。1日集中セミナーを6回に再構成したものです。