新着イベント

新機能イベント参加者限定の懇親会やミニイベント開催に対応した「サブイベント機能」をリリースしました。イベント運営を簡素化し、参加者の登録漏れや確認漏れを防ぐのにご活用ください。主催の方はサブイベントを作成するから、参加者の方はサブイベントが設定されているイベントに参加するから詳細をご確認いただけます。

6月
8
トレース比較器を作って学ぶマルチスレッドプログラミング

主催 : 株式会社 PRINCIPIA

ハッシュタグ：#形式手法

募集内容	一般 6000円（前払い）先着順 5/10人
申込者	申込者一覧を見る
開催日時	2024/06/08(土) 13:00 ～ 18:00 Googleカレンダー icsファイル
募集期間	2024/04/13(土) 00:00 〜 2024/06/08(土) 12:30まで
会場	Zoom オンライン
前払いについて	前払いについての連絡先: (参加者にのみ公開されます)
	キャンセル・参加費用の払い戻しについて主催者からの説明: お申し込み後のキャンセルはできません．セミナーについての説明をよくお読みいただき，十分ご検討の上お申し込みください
	領収データの発行: 発行しない(詳しくはこちら)
出席登録	(イベント開始時間の2時間前から終了時間まで、参加者のみに公開されます)

イベントの説明

セミナーの内容

「デッドロック発見器を作って学ぶマルチスレッドプログラミング ★メッセージ通信編★」の続編です．

デッドロック発見器ではイベント同期という単純なしくみを使って様々な相互作用が表現できることを見ました．相互作用を決めるとシステム全体の振る舞いも状態遷移という形で計算することができ，その過程でデッドロックを発見することができました．

イベントを基礎とした相互作用にはもう1つ優れている点があります．それはシステムの振る舞いを仕様と比較することによって設計の正しさを検証できるという点です．

システムの振る舞いは外部から観測可能なイベントを発生順に並べた列として表すことができます．これをトレースといいます．システムが発生しうるトレースがすべて仕様で許容されたものであれば，システムの振る舞いはかなりの精度で正しいということができます．

一般にシステムは停止せずに動作を継続しますから，いくらでも長いトレースがありえます．さらにシステムが生成しうるトレースの種類も無限になる可能性があります．そうすると有限のメモリしか持たない計算機で有限の時間内に仕様と実装のトレースを比較することは不可能であるように思えますが，興味深いことに模倣（simulation）という考え方を使うとこれが可能になります．この模倣を計算することによって仕様と実装のトレースを比較するプログラムがトレース比較器です．

このセミナーのゴールはトレース比較器を作って仕様とシステムの振る舞いを比較できるようになることです．

以下の例では，初期状態から緑色の遷移をたどって同じトレースがありますが，最後の赤い状態のところで，仕様にはないイベントをシステムが発生していることがわかります．

状態遷移図

トレースは外部から観測可能なイベントだけを含むようにします．ユーザが関心を持つのは外部から見える動作だけで，内部のつくりは関係ないからです．

しかしシステムはコンポーネントを組み合わせて作りますから，その間で行われる相互作用のためのイベントも含まれています．これは内部の都合であって，ユーザには関係しません．

そこでこのような内部で使われるイベントを外から見えなくする処理を行います．これを隠蔽といいます．システムに隠蔽処理をしてからトレース比較を行うということです．

プログラムの正しさを検証するツールの中には，仕様は仕様記述言語，実装はモデリング言語と，仕様・実装で異なる表現形式を使うものがあります．これに対してトレース比較器はどちらも状態遷移で表します．この対称性のおかげで面白いことができます．仕様と実装を交換して比較することです．もし双方向の比較に成功したら，この2つはまったく同じトレースを含んでいるということになります．つまりトレース比較器を使うと状態遷移の等価性を判定することができます．ただし，これには1つ条件があります．実装に非決定性という性質がないことです．これについては発展的な内容としてセミナー内で紹介します．

トレース比較器はシステムの全体の振る舞いだけでなく，要求段階で検討するようなシナリオなども比較することができます．仕様検討や設計の試行錯誤など，プログラム開発の初期段階を支援してくれる強力な武器になると思います．