BEGIN:VCALENDAR VERSION:2.0 PRODID:-//https://techplay.jp//JP CALSCALE:GREGORIAN METHOD:PUBLISH X-WR-CALDESC:並行システムの設計検証入門セミナー X-WR-CALNAME:並行システムの設計検証入門セミナー X-WR-TIMEZONE:Asia/Tokyo BEGIN:VTIMEZONE TZID:Asia/Tokyo BEGIN:STANDARD DTSTART:19700101T000000 TZOFFSETFROM:+0900 TZOFFSETTO:+0900 TZNAME:JST END:STANDARD END:VTIMEZONE BEGIN:VEVENT UID:815771@techplay.jp SUMMARY:並行システムの設計検証入門セミナー DTSTART;TZID=Asia/Tokyo:20210502T120000 DTEND;TZID=Asia/Tokyo:20210502T180000 DTSTAMP:20260416T062510Z CREATED:20210423T142155Z DESCRIPTION:イベント詳細はこちら\nhttps://techplay.jp/event/81577 1?utm_medium=referral&utm_source=ics&utm_campaign=ics\n\n※ connpass か らお申し込みができない場合、isaac@principia-m.com までご 連絡ください。\nセミナーの内容\nマルチスレッドプロ グラミングや組込みシステムのように、複数のコンポ ーネントが並行に動作するシステムの設計は難しいと いわれています。このセミナーでは並行に動作するコ ンポーネントからなるシステム（並行システム）の設 計を支援する理論と設計検証の基礎について、ツール を使いながら学びます。\nこのセミナーで習得できる 技術は設計検証の技術です。設計した並行システムが 期待した振る舞いをもっていること、つまり要求や仕 様を満たしているということをツールを使って設計段 階で検証する技術を学ぶことができます。\n「手を動 かせば理解は後からついてくる」というコンセプトで 進めます。まずはツール上で手を動かし、視覚的なフ ィードバックを得ることが理解への早道であると考え ます。ポイントごとに理論的な説明を行いますが、概 念の獲得というのは時間のかかるものです。もし理解 に不安が生じても、ツール上で確認する手段を持って いれば確信をもって自分の考えを進めることができる でしょう。\n基礎とするのはプロセス代数と呼ばれる 分野に属する CSP (Communicating Sequential Processes) という理 論です。CSP は クイックソートの発明やプログラムの 検証理論である Hoare 論理で有名な Tony Hoare さんによっ て提唱された理論です。教科書では数学的になりがち な CSP の理論を、ほとんど数式を使わずに正確に解説 します。さらにツールを使って視覚的に体験すること で理解を深めることができます。\nCSP に基づくシステ ムの振る舞いの記述は形式仕様記述の一種になります 。広く知られている状態に基づいた仕様記述とは少し 異なり、状態遷移に付随する相互作用の方に力点を置 く記述方法になります。これを体験するとシステムの 振る舞いに対する新たな視点を手に入れることができ ます。対象とするシステムの性質によって適切な記述 形式を選択する自由度を増やすことができるでしょう 。\nプログラム\nプロセスのモデル化\n\nイベント同期\n 選択\nチャネル通信\n状態変数\n条件分岐\nループ\n\n相 互作用と並行合成\n\nプロセス間相互作用とは何か？\n 並行合成\nチャネル通信\nバッファ\nキュー\n共有メモ リ\nミューテックス\nデッドロック\n\n内部遷移・非決 定性・発散\n\n内部遷移・内部イベント\n非決定性\n発 散（ライブロック）\n\nプロセスの振る舞いと正当性\n\ nトレース\n拒否\n正当性の条件\n安全性・活性（ライブ ネス）\n\nトレース集合による安全性検査\n\nトレース 検査\n事例：ランデブ\n\n失敗集合による正当性検査\n\n 失敗検査\n事例：リングバッファ\n\n※ 進捗に応じて、 一部内容をスキップさせていただく場合があります。\ n講師について\n株式会社 PRINCIPIA 代表取締役 初谷 久史 \nCSP 理論に基づいたモデリング・検査ツール SyncStitch 開発者\n国立情報学研究所トップエスイープロジェク ト「並行システムの設計検証」講師\nセミナー参加の 前提条件\n前提知識\n前提として必要な知識は、プログ ラミングの知識と状態遷移モデル（オートマトン）の 知識です。マルチスレッド（プロセス・タスク）のプ ログラムを書いたことがあるという程度の知識を仮定 します。排他制御といった概念やミューテックス、セ マフォといった同期のための機構についての知識を仮 定します。\n一部、発展的な内容に関する部分では、 高校で習う程度の集合の記法（要素 x ∈ A\, 部分集合 A ⊆ B など）を使います。\n必要なもの\n\nツール SyncStit ch がインストールされた PC （マウスが必須です）\n\n 配布物と Zoom meeting URL\nセミナー開始時刻までにCONNPASS のメッセージにてお知らせします。\n同じメッセージ を複数回送信する場合があります。あらかじめご了承 ください。\n使用するツール\nCSP 理論に基づいたモデ リングと検査が可能な SyncStitch というツールを使用し ます。\n注意事項\n\n配布スライド資料の公開は禁止で す。配布モデルファイルはご自由にお使いください。\ n不測の事態が生じセミナーを開催または完遂できなか った場合は、日を改めて再開催することで対処させて いただきます。\n都合により申し込み後に参加できな くなった場合は、同等のセミナーを再演する際にご参 加いただけるよう配慮しますのでご連絡ください。\n\n 参考書\n\n並行システムの検証と実装\n\n連絡先\nご質問 等がありましたら isaac@principia-m.com までお気軽にご連 絡ください。 LOCATION:Zoom オンライン URL:https://techplay.jp/event/815771?utm_medium=referral&utm_source=ics&utm _campaign=ics END:VEVENT END:VCALENDAR