SSK 株式会社 新社会システム総合研究所

TOP調査レポートTOP > レポート詳細ページ

レポートカテゴリー

レポートのお問合せ

レポートについてのお問合せは

E-mail:nbd@ssk21.co.jp

まで、お気軽にご連絡ください。

調査会社一覧

No.R06V0023

PAT3によるモデル検証

~"PAT3によるモデル検証"は、リアルタイム、並行処理を必要とする組込みシステムに有効!~

出版日 2013年3月
価格
印刷タイプ 50,400円(税込)
ページ数 A4判 202ページ
発行<調査・編集> (株)トリケップス

申込フォームお問合せ

乱丁・落丁以外のご返品につきましては、原則としてお申し受けできませんのでご了承ください。

レポート内容

■概要■
 大規模高度システムのための組み込みソフトウェア開発では、安全性と信頼性が大きな問題となっています。とりわけ、自動車、エレベータ、ロボット、鉄道、医療、宇宙機器などの産業機器、或いは民生機器では高信頼化が要求されています。組み込みシステムでの機能安全規格として、IEC61508(機能安全規格)、ISO26262(自動車)などの上位レベルでは形式手法(CCS,CSP,HOL,LOTOS,OBJ,VDM,Z, 時相論理, 他) を使う事を高く推奨(HR)されています。従って証明されたシステム設計方法は特別なものではなく、ヨーロッパでは当然のように実施されています。
 自動車、列車の制御、通信、制御、ロボットなどの様に高機能で高性能な領域に入りますと、リアルタイム処理、高度で複雑な並行処理プログラミング技法が要求されます。一般に使われていますZ/B/Event-B/Alloy/VDMなどの形式手法ツールでは要求仕様の検証が主であり、リアルタイム処理、並行処理、通信、割り込み等の振る舞いの検証は十分でないだけでなくアーキテクチャーの検証は非常に難しいです。そこで注目されるのがCSPモデルです。
 CSP(Communicating Sequential Processes)は、元Oxford大学のTony Hoareが1978年に考案し英国を中心に欧州で研究実用化が進められ、その結果としてInmos社から並列処理言語occamと並列プロセッサTransputerが生み出されました。90年代後半にTransputerが消えてからも、2000年以降CSPモデルを採用したハードウェア、ソフトウェアは数多く見られる様になりました。この背景には、アプリケーションが複雑化するにつれて、CSPモデルの有効性が再注目されている様に思います。
 CSPはプロセス代数の一つでありプロセスの振る舞いを数学的に記述できする事ができます。その後にモデル検証ツールを用いてモデルが正しいかどうかの検証をします。CSPモデルの検証ツールには、LTSA/SPIN/FDR2/PAT3/Verum/Moby/ProB/CONPASU/CSP-Proverなどがあります。特にPAT3はReal-Time CSPなどサポートされていますので、組み込み系のアプリケーションのモデル検証として使えます。
 PAT3には多くの機能が用意されていますが、とりわけCSPモデルが中心となってますので、ある程度CSPの理解が必要とされます。テキストの構成は、英国Surrey大学のSteve Schneider教授のテキスト「Concurrent and Real-time Systems-The CSP Approach」を主として使い、CSPのデザインパターンを用意し、それらをPAT3のコードに書き直す事から入ります。
 このデザインパターンはプログラミングの構造と同じなのでoccam-π/JCSP/XCなどのプログラミング技法へと展開する事ができます。基礎的なデザインパターンの構造が理解できますと、更に複雑なプロセスモデルを考える事ができます。この操作はLEGOマシンの仕組みと同じです。プロセスの遷移法則と代数的法則はプログラム言語の意味を理解するのに役立ちますので添付いたしました。
 CSPコンストラクタの法則性に関してTony Hoare、Bill Roscoe、Steve Schneiderのテキストには書かれていますが、もう少し基本的で有益な内容がTony Hoare、Jim Woodcock、Xinbei Tangらの資料の中にありますので、その中から抽出し追加致しました。

■執筆者■
松井 和人
NPO法人CSPコンソーシアム 理事
<略歴>
米国ミネソタ大学コンピュータ科学科卒業。1987年に英国半導体メーカInmos社に入社し並列処理プロセッサTransputer、occamのプログラミングの指導をする。その後仏伊STMicroelectronics社に買収されてからCSPモデルのSoC(System-on-Chip)、高速シリアルリンク(IEEE1394/1355)などの技術を推進する。
WoTUG委員会(http://www.wotug.org/)のメンバーとして1989年から1996年までのTransputer/occam国際会議において東京大学國井利泰名誉教授、東北大学野口正一名誉教授の下で会議の運営に携わり、論文集を作成した。2001年から独立し、現在NPO法人CSPコンソーシアム理事、2011年より法政大学大学院情報科学科の兼任講師を務める。CSP研究会の幹事として会議の運営とCSP/occamモデルによる並行プログラミング技法の啓蒙を行っている。

-CONTENTS-

まえがき

<1>CSPプロセス概論
1.CSPプロセスとは
2.アルファベット(Alphabet)
3.正常終了(SKIP)
4.停止(STOP)
5.RUN
6.混乱(CHAOS)
7.イベントの定義
8.接頭辞(Prefix)イベント
9.推論規則(Inference Rules)
10.Prefix選択
11.ラベル付き状態遷移
12.LTSの定義
13.チャネル(Channel)の入出力
14.再帰(Recursion)
15.条件(IF コンストラクタ)
16.繰り返し(WHILE コンストラクタ)
17.選択(Choice)
18.ガード(Guard)付き選択
19.外部選択(External Choice)コンストラクタ
20.内部選択(Internal Choice)コンストラクタ
21.逐次(Sequence)コンストラクタ
22.並行(Concurrent)コンストラクタ
23.隠蔽(Hiding)
24.リネーム(Renaming)
25.パイプ(Pipe)
26.奴隷化(Enslavement)
27.優先度(Priority)
28.割り込み(Interrupt)
29.索引(Index)付き付き並列、選択、インターリーブ

<2>トレースとその意味
1.トレース(Traces)
2.連結(Catenation)
3.制限(Restriction)
4.頭尾(Head and tail)
5.スター(*Star)
6.順序(Ordering)
7.長さ(Length)
8.選抜(Selection)
9.initials/after
10.トレースと実行
11.充足(Satisfaction)
12.TRACEの定義
13.STOP
14.SKIP
15.RUN
16.Prefixイベント
17.Prefix選択
18.チャネル
19.条件
20.隠蔽
21.再帰
22.逐次
23.選択
24.アルファベット並列
25.インターフェース並列
26.インターリーブ
27.割り込み
28.トレース等価性

<3>拒否、失敗、失敗発散
1.拒否(Refusals)
2.拒否の法則
3.安定した拒否(Stable Refusals)
4.失敗(Failures)
5.安定な失敗(Stable Failures)
6.失敗の法則
7.失敗・発散・無限のトレース
8.詳細化(Refinement)

<4>PAT3の構文と使い方
1.PAT3のインストール
2.PAT3のアーキテクチャ
3.PAT3のモデルチェック
4.定数
5.変数
6.チャネル
7.命題
8.Skip、Stop
9.Prefixイベント
10.アルファベット
11.データの操作
12.条件、選択
13.case文
14.while文
15.atomic文
16.急ぐイベント(Urgent Event)
17.外部選択/内部選択
18.逐次合成/並列合成
19.インターリーブ
20.隠蔽
21.ガード(Guard)
22.プロセスの引数とグローバル変数
23.表明(Assertion)の式
24.線形時相論理(Linear Temporal Logic)

<5>デザインパターンとPAT3の使用方法
1.碁盤の移動
2.到達性(Reaches)
3.チャネル入出力
4.簡単な通信プロトコル
5.プロセスCOPY
6.並行
7.アルファベットに同期した並行処理
8.Stop-and-Wait Protocol
9.バッファ
10.スタック(Stack)
11.ABP(Alternating Bit Protocol)
12.パイプ(Pipe)
13.プロセスの選択
14.多重化されたバッファ
15.One2One チャネル(One2N,N2One)
16.共有チャネル(One2Any、Any2One、Any2Any)
17.同期送信(parSend)と同期受信(parRead)
18.インターリーブ
19.マトリックスの掛け算
20.円卓の哲学者
21.PAT3における詳細化

<6>Timed CSPの概論
1.CSPモデルの階層化
2.Timed CSPの表記
3.Timed CSPとPAT3
4.時間の間隔(Intervals of Time)
5.時間付きイベント(Timed Event)
6.時間付きトレース(Timed Traces)
7.時間付き拒否(Timed Refusals)
8.時間付き失敗(Timed Failures)
9.時間詳細化(Timewise Refinement)

<7>Timed-CSPによるPAT3の適用
1.時間オートマタ(Timed Automata)
2.タイマーとの同期
3.時間付きチャネル出力(Timed Output)
4.耐故障システム(Fault Tolerance)
5.時間付きバッファ(Timed Buffer)
6.列車の踏み切り制御

<8>UML図へのPAT3の適用
1.コンポーネント要素
2.遷移
3.シーケンス
4.シーケンス図
5.並行処理
6.パラレル図(1)
7.パラレル図(2)
8.alt図
9.通信図
10.アクティビティ図
11.状態マシン図
12.タイミング図
13.CDプレーヤー

<9>Stateflow図へのPAT3の適用
1.Stateflow図とは
2.排他的(OR)な遷移
3.自己ループル遷移

<付録>
 ・稲盛財団京都賞受賞
 ・数学的背景
 ・CSPで使用される記号と意味

<参考文献>

申込フォームお問合せ

株式会社 新社会システム総合研究所 東京都港区西新橋 2-6-2 友泉西新橋ビル 4F TEL 03-5532-8850