お知らせ 2024年9月1日よりconnpassサービスサイトへのスクレイピングを禁止とし、利用規約に禁止事項として明記します。
9月1日以降のconnpassの情報取得につきましては イベントサーチAPI の利用をご検討ください。

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

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

Jun

29

LTL モデル検査器を作って学ぶマルチスレッドプログラミング

好きな言語でモデル検査器を作りましょう。

Organizing : 株式会社 PRINCIPIA

LTL モデル検査器を作って学ぶマルチスレッドプログラミング
Hashtag :#形式手法
Registration info

一般

6000 (Pre-pay)

FCFS
2/10

Attendees
TakayukiTakeuchi
negi23
View Attendee List
Start Date
2024/06/29(Sat) 13:00 ~ 18:00
Registration Period

2024/05/12(Sun) 00:00 〜
2024/06/29(Sat) 00:00まで

Location

Zoom

オンライン

About Prepayment

About Prepayment Contact Info:

(Only shown to attendees.)

Cancel/Refund Policy:

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

Print receipt data:

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

Description

セミナーの内容

線形時相論理 (Linear Temporal Logic, LTL) にもとづくモデル検査ツールを自分で実装してみようというセミナーです。実装することで仕組みを深く理解できます。自分の好きな言語で作った自分専用のツールというのは愛着のわくものですよね。いろいろと拡張したり、他のツールと組み合わせたりして楽しめます。

モデル検査ツールというのは、プログラムの性質を自動的に検査するツールです。プログラムというのは動くものです。つまり、時間的に変化するものなので、多くの場合、調べたい性質も時間に関係するものになります。

時間に関する性質を表現するために拡張された論理の1つに時相論理というものがあります。よく知られている命題論理に加えて、時間に関する演算子をもっており、これを使って時間に関係するプログラムの性質を表すことができます。

このセミナーで作るモデル検査ツールは、状態遷移モデルとして表したプログラムと、時相論理で表した調べたい性質を入力すると、プログラムが性質を満たしているかどうかを自動的に検査してくれるものです(※1)。検査の結果、満たさないケースがあればレポートしてくれます。それを分析することで、プログラムの誤りを知ることができます。

※1 正確には、時相論理式を外部サービスでオートマトンに変換して、それを入力します。

モデル検査の概要

セミナーは2部構成になっています。第1部では、まずモデル検査の仕組みを説明し、リファレンス実装による設計・実装の方法について解説します。次にモデル検査の実行例を紹介します。第2部では参加者のみなさんに設計・実装をしていただきます。疑問な点を質問したり設計についての相談したりしながら進める形となります。

プログラム

第1部 モデル検査解説

  1. モデル検査の概要
  2. 計算木・パス・原子命題・ラベリング関数・語
  3. 線形時相論理 LTL
  4. Büchi オートマトン
  5. LTL モデル検査のアルゴリズム
  6. リファレンス実装の解説
  7. テスト
  8. 例:排他制御
  9. 公平性
  10. 例:通信システム

※ 知っている人への注:LTL 式を Büchi オートマトンに変換する部分は、既存のサービスを利用します。処理全体の中での位置づけは説明しますが、アルゴリズムの解説は行いません。

第2部 モデル検査器の設計と実装

各自、モデル検査ツールを好きな言語で実装します。

講師について

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

プロセス代数 CSP に基づいた検査ツール SyncStitch 開発者

国立情報学研究所トップエスイープロジェクト「モデル検査特論」講師

セミナー参加の前提条件

前提知識

  • 高校で習う程度の論理の知識(かつ、または、~でない)
  • アルゴリズムの知識:グラフの探索(幅優先探索、深さ優先探索)
  • データ構造の知識:ハッシュ表,キュー

デッドロック発見器のセミナーを受けていなくても理解できる構成です。しかし、デッドロック発見器(共有変数またはメッセージ通信による並行合成器)を持っていれば、組み合わせてより面白い検査ができます。

必要なもの

  • 使用するプログラミング言語の開発環境(リファレンス実装を動かすためには OCaml の開発環境が必要です)
  • Graphviz (dot コマンド):状態遷移グラフを可視化するために使用します.

Zoom URL

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

配布物

スライド資料(PDF)とリファレンス実装のソースコード(OCaml)を CONNPASS のメッセージにて送付します.

プログラムの大きさの目安

モデル検査器のコードの大きさは、OCaml のリファレンス実装で約270行程度です。

注意事項

  • 講師が知らないプログラミング言語については対処が限られます.
  • 配布資料の公開は禁止です.

参考書

連絡先

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

Media View all Media

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

Group

PRINCIPIA

Number of events 120

Members 263

Public

2024/06/29(Sat)

13:00
18:00

Please login to register

Registration Period
2024/05/12(Sun) 00:00 〜
2024/06/29(Sat) 00:00

Location

Zoom

オンライン

Zoom

Organizer

Attendees(2)

TakayukiTakeuchi

TakayukiTakeuchi

LTL モデル検査器を作って学ぶマルチスレッドプログラミング に参加を申し込みました!

negi23

negi23

LTL モデル検査器を作って学ぶマルチスレッドプログラミング に参加を申し込みました!

Attendees (2)