離散型生産システムのための挙動表現モデルと検証システムの開発‐研究支援における研究内容と進捗状況‐
宮崎大学 工学部教育研究支援技術センター
高塚 佳代子はじめに近年の離散型生産システムを効率的に運用するためには，適切な運用戦略や制御システムを与えることが特に重要である．しかし，リアクティブかつ並列に非決定的な動作をするこの種のシステムの複雑な挙動を適切に表現できるようなモデル自体，まだ確立されていない．以上の点を踏まえ，本研究では，このような対象の挙動モデルを構築し，モデルに基づく制御系設計手法を提案するとともに，設計されたシステムが正しく動作するかどうかを検証するための手法を確立することを目的とする．
キーワード： 離散型生産システム 挙動表現モデル モデルに基づく設計 性質検証
1. 背景と目的
ネットワーク型生産システム，組み立て式プラント，バッチ型プラントといった様々なシステムがあり，これらは離散型生産システムと呼ばれている．そして，これらは，リアクティブ性，並行性，非決定性，操作上の自由度の多さといった問題を共通に持っている．
このようなシステムを効率的に運用するためには，適切な運用戦略や制御システムを与えることが特に重要である．しかし，この種のシステムの複雑な挙動を適切に表現できるようなモデル自体，まだ確立されていない．
以上の点を踏まえ，本研究では，以下の(1)～(4)を目的とした研究を進めている．
(1)離散型生産システムの挙動モデルを開発すること．
(2)生産システム固有の特徴を踏まえたモデル化手法を確立すること．
(3)開発した挙動モデルを使用した「モデルに基づく制御系設計手法」を提案すること．
(4)設計されたシステムが正しく動作するかどうかを検証するための検証手法を確立すること．
本稿では，これらの目的に対する研究の内容と進捗状況について説明する．
2. 挙動モデルの開発
2.1 開発の基本方針
まず挙動モデルの開発について説明する．複雑な動作を示す離散型生産システムの挙動モデルに求められる要件は，次の通り．
①人が見て理解し易い階層的認識が表現可能②時間制約を伴う事象駆動動作が表現可能③「リアクティブ・システム」としての表現が可能④並列動作主体間での通信・同期・排他制御が表現可
能⑤次々と入ってくる処理対象の動作が表現可能
本研究では，まず，これらの要件を最も良く満たす既存のモデルとして時間ステートチャートを採用した．
これは，システムの持つ階層的な並列動作構造をAND/OR ツリーの形でうまく表現でき，状態遷移の条件で実時間制約を扱え，ブロードキャスト通信の概念を持つようなモデルである．更にそこへ，通信・同期を表現する(要件④)ために必要な出力イベントの発火時刻の記述方法と，次々と入ってくる処理対象の動作を表現する(要件⑤)ために必要な「トークン識別子」を導入し，“拡張時間ステートチャート”を開発した．
2.2 拡張内容
開発した挙動モデル「拡張時間ステートチャート」のベースとなる時間ステートチャートについて説明した後，拡張部分について説明する．1)

時間ステートチャート「ステートチャート」とは，オートマトンを階層性や並行性を表現できるように拡張したものであり，「時間ステートチャート」とは，状態遷移の条件で実時間制約を扱えるよう，通常のステートチャートを拡張したものである．

拡張 1 ( 出力イベントとイベントプールの導入)
まず，通信・同期を表現可能にするために，出力イベントに関する 2 つの記述方法を導入した．即ち，一つは，出力イベントの発火可能期間を指定できるような記述方法を導入し，もう一つは，出力された複数のイベントの扱いが AND 型なのか XOR 型なのかを指定

a(10,∞)a(20,∞)
APct=0B
Qc(10,∞)
c(30,∞)
C5≦t≦10, aD

図 1 出力イベントの記述の例

ACB

D

①
BC BD AD
従来型動作モデル

BD(2)

BDAD

AC②BC

AC

BC

AC
BC

AC

BD

拡張型動作モデルAD

図 2 動作モデルの拡張
2.3 開発の成果
ここで，開発した挙動モデルを使うと離散型生産システムの複雑な動作がどのように記述されるかを示す．
図 3-(1),(2)は，ネットワーク型生産プラントの一種である「特殊プラスチックフィルム製造プラント」の動作の概観と拠点間のインタラクションを示したものである．本対象は，図 3-(2)で示すように，あちこちの拠点同士での情報のやり取りが錯綜するといった特徴を持
つのだが，開発した挙動モデルを使うと，図 3-(3)のようなすっきりした形で記述できる．ここでの注目すべ
き点は 2 つある．一つは，拡張時間ステートチャートの並行性・階層性，及び，導入された出力イベントの記述方法を用いると，図 3-(2)で示すような複雑なインタラクションが，図 3-(3)で示すように簡潔に記述されるということである．もう一つは，要求のバッファリング幅や再計画の上限設定といった様々なタイプの運用戦略の埋め込みや変更が容易に行えるということである．
(2)生産拠点間のインタラクション(1)対象プラントの概観
・2種類の装置
・5種類の処理

生産計画部門
生産計画部門

①依頼

生産拠点1

生産拠点2

生産計画
部門

生産拠点3・3種類の装置
・22種類の処理

生産拠点4

生産拠点1

拡張 2 ( 複数トークンの扱い)

生産拠点３
生産拠点３

生産拠点２
生産拠点２

22計画成功②依頼 ⑫回答y④⑭③依頼 ⑮回答y

製造計画

21計画成功⑤依頼⑬回答y

⑱計画失敗
⑩依頼
⑯
⑥回答no⑧

生産
生産拠点4拠点４製造計画

⑲計画失敗

⑪依頼

再計画

⑰要求 ⑦回答no⑨回答no・4種類の装置・23種類の処理・5種類の装置・23種類の処理

もう一つの拡張では，元々単一の処理対象を扱うモデルである時間ステートチャートを，「複数の処理対象が次々に入ってくる」といった生産システム特有の動作をモデル化できるようにするための拡張を行った．
まず，挙動モデルの階層性・並行性を展開して得られる従来型の動作モデル(図 2-(1))では， 各ノードにトークンがあるかないかの区別しかできなかったが，次々に入ってくるトークンを識別させるための「トークン識別子」を導入し(図 2-①)，更に，トークンの発生や消滅タイミングを認識できるような仕組みを導入した結果(図 2-②)，個々の処理対象が処理されていく過程を個別に辿れるような望む動作モデルが得られた(図2-(2))．

拡張法
適用

④依頼

再計画

⑳計画失敗

モデル化
「生産拠点1」の内部詳細

システム全体P1plan（生産計画部門）
生産拠点1
生産拠点2

生産拠点3
生産拠点4

＜製造計画＞( 製造計画)

T1.2:≧48 ④
T1.1：=0

req(to拠点1,ｆｒX,1,” ロット番号 ” ,C)②

受理・計画終了

P1wait(バッファリング中 )T1.1≦2

受理(fr拠点 1,” ロット番号 ” ,C)⑥

不受理 (toX ,fr拠点11,” ロット番号 ” ,C)T1.2:=0①

P1ready( 計画期間終了 )

⑦

EO
R

[例 1] (拡張時間ステートチャート)
図 1 は拡張時間ステートチャートの例である．この
図は，システム全体の動作が，基本的には 2 つの動作 Pと Q の並列動作で成り立ち，そのそれぞれが，状態 Aから B への遷移と，C から D への遷移で成り立っている様子を表している．また，イベントの発火時刻や動作モードは次のように指定されている．
・a(10,∞) AND a(20,∞)
状態遷移 B->A が生起したときイベント a(10,∞)かつa(20,∞)を生成し，a(10,∞)は 10 クロック以降，a(20,∞)は 20 クロック以降に発火させよ．
・c(10,∞) XOR c(30,∞)
状態遷移 D->C が生起したとき，イベント c(10,∞)または c(30,∞)を生成し，c(10,∞)ならば 10 クロック以降，c(30,∞)ならば 30 クロック以降に発火させよ．

従来法適用(1) AC

挙動モデルできるような記述方法を導入した．なお，出力イベン
トを指定された時間帯で発火させるための仕組みとして，出力イベントの全てを一旦格納する「イベントプール」と，それらの一括管理を行う「イベントプール・マネージャ」を導入した．なおイベントプールの内容の提示はブロードキャスト方式を採用している．

P1result

T1.1>2＜再計画＞
RP1plan

製造計画（製造依頼に対する活動）
再計画（製造依頼に対する回答を受けた活動）「生産拠点1」の内部(3)拡張時間
ステートチャート

(再計画)

C＜3
≦13≦ C

不受理 (to拠点 1,ｆｒX,P,” ロット番号 ” ,C)
製造要求

EO
RRP1result(ok)

T1.3≦ 1req(to拠点3, fr拠点1,P,” ロット番号 ” ,C+1)
req(to拠点4, fr拠点1,P, ” ロット番号 ” ,C+1)
不受理 (toX,ｆｒ拠点2,P, ” ロット番号 ” ,C)

⑪

T1.4:
≧29

RP1wait
不受理 (to拠点 2,ｆｒX, (バッファP,” ロット番号 ” ,C)
リング中 )
不受理 (ｆｒ拠点2,P,” ロット番号 ” ,C)

RP1result(no)⑫

T1.4:=0RP1plan( 再計画期間終了 )T1.3>1
T1.3>1

・再計画の上限設定
・要求のバッファリング幅

図 3 拡張時間ステートチャートによる動作記述

5-(2))，図中 P で示すようなアークの先端が集中するといった構造的特徴を持つ部分として顕在化する．
(1)フローショップ型生産システム ＜FA 実験装置＞
パーツフィーダ

ストッパー

搬出コンベア

搬入コンベアアームロボット

判別センサー

処理全体 (ユーザ仕様)

Q

C→D1→D2 F

PR・ P・E
Q・ ・・FC →D1 →D2
・ ・・

A1→A2→B(2)

図 4 プロセスネットワーク型モデル作成手順
3.2 プロセスネットワーク型モデルの例
図 5-(1)で示すような 2 工程のフローショップ型生産システムである FA 実験装置を例として，
プロセスネットワーク型モデルの例を示す．本例題の特徴の一つは，アームロボットが，搬入コンベア端から 4 つの処理装置を持つターンテーブルへ，または，ターンテーブルから搬出コンベア端へ，処理対象の搬送が可能なので，5 箇所からの使用要求が競合する制御部位を持っているという点である．先に述べたように，このような制御部位は，作成されたプロセスネットワーク上では(図工程C→A1→A2→B
PR(B→E) XOR (D1→F) (1) A1→A2→B E
C→D1→D2

ストッカー

ターンテーブル

2ボックス

第1工程

(2)プロセスネットワーク型モデル
Parts Feeder｛L1, L2｝･･ ････ ･･ ･･ ･P･ ･･･ ･･･ ･･･ ･ ･ ････ ･｛P&P
L2,L3,

Conveyer2＆S1｛L18,L19,L20｝

to{L6..}

Conveyer2＆S1｛L18,L19,L20｝

Conveyer2＆S1｛L18,L19,L20｝

Conveyer2＆S1｛L18, L19,L20｝

L4｝

Conveyer1｛L4,L5, L7｝

3.1 プロセスネットワーク型モデルの導入開発したモデル化手法の手順は，次の通り．
1. 先ず，頻繁な同期制御を必要とする処理同士は一つのノードにまとめる(図 4-(1))．こうすることにより，頻繁な同期制御が必要な処理は，同じ動作マネージャによって管理されるようになる．
2. 更に，それ以外に同期を必要とする処理同士に対してはアークを導入する(図 4-(2))．
以上の手順でモデルは得られる．
ところで，実際，この手のシステムで一番問題になるのは，どこでどういった制御をしないといけないかを見つけることである．このようなモデルを作っておくと，それを見つけ易いという大きな利点がある．例
えば，図中では，点 P で示すようなアークの先端が集中するといった構造的特徴を持つ部分として制御部位が顕在化している．

押し出しシリンダー

第ピック＆プレース

3. 生産システム固有の特徴を踏まえたモデル化手法の確立
以上述べたような挙動モデルの開発については，基本的にはほぼ完成されており，今後はこれを活用した研究が中心になると考えている．
上述したような拡張時間ステートチャートには，実は，その表現力の柔軟性ゆえ，出来あがったモデルに個人差が生じやすいという問題がある．その問題に対応するために，拡張時間ステートチャートの持つ自由度を一部制限し，その代わりに系統的に生成させる手法を現在開発している．具体的なアイディアは，生産システムが本来持っている「プロセスネットワーク型の構造」を生かすということである．2)

Arm Robot
L7, L9, L10｛L6,Merge to{L8}‐type
T1｛L8,L10,L11 L14 ｝｛L16,｝ ｛L12,L14, L15,

T2
｛L8,L10,L11 L14 ｝

Conveyer2
L17 ｝
Dispatch
‐type

L16｝

Merge
‐type
to{L13}to{L8}

Turnｔable
L8｛

T3｛L8,L10,L11 L14 ｝｝ ｛L13｝

Dispatch‐type

T4｛L8,L10,L11 L14 ｝

to{L12..}

図 5 プロセスネットワーク型モデルによる記述例
4. 離散型生産システムの制御系設計への適用
4.1 拡張時間ステートチャートとプロセスネットワー
ク型モデルの活用上で開発した 2 つの挙動モデルが，「制御系のモデルに基づく系統的設計」に活用できるということが分かり，
現在その設計手法の開発を行っている(図6 参照)．
具体的に，この手法でやりたいことは，ユーザが与えるプラント仕様,制御仕様をコントローラへ形式的・システマティックに橋渡しする事だが，着目して欲しい点は，そこでは，今まで開発してきたモデル(プロセスネットワーク,拡張時間ステートチャート)が重要な要素技術になっているということにある．現在は，制御に関する要求仕様が埋め込まれた挙動モデルからその制御動作を実機上で実現するのに必要な様々な情報を，いくつかの「テンプレート」を用いて系統的に抽出させる方法について研究を進めている．3)
4.2 制御系設計手法の流れ開発した制御系の設計手法でやっていることを FA実験装置の例で説明する．まず，対象プラントの動作仕様(図 7-(D1))から得られるモデルの雛形に対し制御を被せるとプロセスネットワーク型モデルが完成し(図 7-(D2))，それを拡張時間ステートチャートへ変換することにより，制御が埋め込まれた挙動モデルが得られる(図 7-(D3))．次に，その拡張時間ステートチャートから，各種テンプレートを用いることにより，制御に関する仕様を実機上で実現するために必要な様々な情報がシステマティックな手順で抽出できる(図 7-(D4))．
こうしてできるものを制御モジュールと呼び，これがコントローラへの入力データとなり，コントローラのドライバを駆動することになる．
5. 動作検証手法の開発設計された挙動モデルがきちんと動作するのかどうかをシステマティックな手順で検証するための手法について説明する．4)
5.1 検証の必要性
離散型生産システムにおいて「何のための検証が必要なのか？」というと，「スケジューリングや制御則によってユーザが恣意的に決定している部分」に対する検証が必要である．例えば，図 8 で示すようなバッチ型プラントに対し，「重合缶反応は長くとも 80 分で打ち切る」という制御則を導入した場合，安全面を考慮した「全ての処理対象に関し，重合缶 A1 での処理開始後 150 クロック以内に重合缶 A2 での処理が終了するか？」のような内容が「検証したいこと」として考えられる．
5.2 検証手法開発の経緯
本研究では，上述するようなシステムのための検証の枠組みを次のようにして開発した．まず，「複数のプロセスが並行動作し，かつ，タイミング制約が厳しい」といった生産システムと実時間並行ソフトウェアの特性の類似性に着目した結果，実時間並行ソフトウェアの既存の検証手法を採用した．そして，それを離散型生産システムのために拡張した．具体的には，既存の手法が持つ挙動モデル「時間ステートチャート」，それが示し得る可能世界である「時間 Kripke 構造」，及び，それ(可能世界)の生成手法をそれぞれ拡張することにより，離散型生産システムの検証手法を開発した．
5.3 検証手法の基本構造
図 9 は，上述の拡張の結果得られた本検証手法の基本構造を示している．具体的には，拡張時間ステートチャートで記述した対象世界の挙動を，これが引き起こし得る可能世界である拡張時間 Kripke 構造に展開し，論理式「TCTL」で書かれた調べたい性質に関する検証を可能世界上で全数探索的に行わせるという流れである．実際，この枠組み自体はプログラム検証では一般的な構造であるが，それに対して先に述べたような拡張をすることにより，本手法が得られた．

6. 提案手法の妥当性・有効性の実証的検証
以上説明してきた一連の提案手法の妥当性と有効性を検証するために，バッチ型化学プラント，FA 実験装置，ネットワーク型生産システムなどを対象に検証のための実験を一部始めている．その結果，上で述べたような限定された範囲において，図 10 で示すような結果が確認されている．具体的には，挙動表現モデルに関しては，ここで示す全ての具体例に対して，それが有効であることが確認されている．また，性質検証手法に関しては，部分的に，その有効性が確認されている．一方，プロセスネットワークによるモデル化手法，及び，モデルに基づく制御系設計手法に関しては，今後，これとは違ったアプローチも含めて検討が必要であると考える．

7. まとめ・挙動モデルの開発： 離散型生産システムのための挙動モデル「拡張時間ステートチャート」を開発した．
・モデル化手法の開発： プロセスネットワーク型モデルを用いて拡張時間ステートチャートを合理的に限定しつつ系統的に生成する手法を考案した．
・制御系設計手法の開発： 開発した 2 つの挙動モデ
ルを重要な要素技術として活用した制御系設計手法の枠組みを開発した．
・動作検証手法の開発： 設計された挙動モデルがきちんと動作するのかどうかをシステマティックな手順で検証するための手法を開発した．
参考文献
1) 高塚 冨田, 時間ステートチャートの拡張と「イベントプール」を用いた Kripke 構造生成法の開発, 計測自動制御学会システム・情報部門第 42 回離散事象システ
ム研究会講演論文集, 2007, pp39-44
2) Takatsuka Hirano Tomita, On a Formal Methodfor Modeling Discrete Production Systems based on
Process-Network Architecture --With application tomodeling of FA experiment device--, AdCONIP’ 02,
pp281-286
3) Takatsuka Tomita, On Model-based Approach forDeveloping Control Systems of Event-Driven Manufacturing
Systems, INDIN06, p699-706
4)Takatsuka Tomita，On Modeling and Algorithm
for verifying behavior of Discrete Parallel Production
Systems, PSE Asia 2002, pp277-282

A

制御仕様を実機上で実現するための様々な情報制御仕様がユーザ埋め込まれている
仕様記述
挙動モデル
(D1)

実行モジュール群(D3)拡張 (D4)

(D2)

プロセスInput ・制御仕様
Input
ネットワーク・プラント仕様 モデル○ 制御リストモジュー
ルState1条 ○ 干渉モジュール時間
実行
Outputステート モジュール
チャート

生成手法

変換手法 抽出手法

制御モジュール
導入ルール

状態分割
ルール

DIO Board
解読 Direct
実行 I/O
Cable

Mini FA Plant

テンプレート

検証
結果

修正

図 6 挙動表現モデルを活用した制御系設計手法の枠組み(D1)対象の動作仕様(D2)プロセスネットワーク型モデル･ ･･ ･ ･･ ･ ･ ･ ･･ ････ ･･･ ･ ･ ･･････ ･･･ ･ ･････ ･ ･ ･ ･ ･ ･ ･ ･ ･･･ ･･･ ･ ･･･････ ･ ･･････ ･ ･･･ ･ ･ ･ ･･･ ･ ･ ･ ･･･ ･ ･ ･ ･･･ ･Parts Feeder｛L1, L2 ｝

Conveyer2＆S1 （59） Conveyer2＆S1 （60） Conveyer2＆S1 （61） Conveyer2＆S1 （ 62）｛L18, L19,L20 ｝ ｛L18, L19,L20 ｝ ｛L18, L19,L20 ｝ ｛L18, L19,L20 ｝

（ 1）

（ 4）

（2）

（5 2）

（3 ）
P&P
｛ L2, L3,L4｝

（7）

（5）

Conveyer1｛ L4,L5, L7 ｝
（6）

（39 ）

（ 37）

（9 ）

To｛ L6..}
（ 63）

（5 3）

（5 7）

（54）

（ 50 ）

Conveyer2｛ L16, L17, L18 ｝

（ 51）

（8）

Control①
Module

（ 41）

（ 56）

Control Module④（ 11）～（ 14）（19 ）～（22 ）（ 26 ）
Air Robot｛L6, L7, L9, L10 ｝｛L12, L14, L15, L16｝（ 64）

T o｛L12..}

（1 5）
（ 16）
（ 17）

（ 35）

（23）

｛L8Turnｔable｝ ｛L13｝（ 70 ）（ 24 ） （ 25）Control
Module②To｛L8 }
（65）

To
｛L13}
（ 66）～（ 69）Control
Module③（48）

T1｛ L8,L10, L11

（ 18）

（ 30）

（ 33 ）（ 31 ）

（ 42）

（ 46）

T1
｛ L8,L10, L11（ 43）T1｛ L8,L10, L11

L14 ｝

（ 34）

（3 2）

（47 ）

L14 ｝

（ 36）

１4個のノードと4個の制御モジュール(D3)拡張時間
ステートチャート
ARA6
AR A6ARPF - A1

PF - B1PF - A1 ´

PF - B1 ´PF e - A2

PF - B2
PPB2

TTA1 3
AR A12>=6C2AR

A 14

A RA 9T

A 10A9PF - READYAReTT

AR A9T

AR>=3

AR

A14>=3A RA 14>=3

A RA 14TTT

AR A14

AR

A 15

AR

A 15

AR

A 16

O CA 16

AR

Event module

A RA 16>=3AR

R EA DYAR

R EA DY
C1IC
TTA 8TTAR A14T
TTAR A14A RA 15>=3TT

C1C3C1A8A8READY

TT- A2A8TT

PP- B2
TTA8 >=8>=3PP B2A8TT

TT

PPB3>=

B4´

READY

TT

A8TTA8 >=8AR A12AR A12A 13

TT
A RA10READY

TT

TT

READY

TT

A 13T

AR A14TT

A13
TTA1 3>=8TTA1 3TT

A13READYTT
TTA1 3>=8TTA 1 3T

A8TT

TT
TTA1 3>=8TTA8TT

AR A0TT

TT

T
TTA8 >=8TTA 8PP B2A8TT
ARA 10PP- B3- A3A 3>=

A8>=3TTA 8TT

PPPPA 13TT

TT

TTT

R EA DYConveyer1 End Sensing

T

TTA1 3T
A RA 14

REA DYA 13TTTARA 14TTTTR EA DY

PP B4PPA4PP- A4PP´

ICA 4C2ICA4TTA8ICB4- A4PPA4, A5ICC2ICB4TTA1 3C2ICB4 B5>=20

TTA1 3C2ICB5 3
TTA1

B4, B5

ICA 4A 5>=20
ICA5PPA RICC1IC- B4A7IC

B7

ICA7>=3PP

A 4 >=PP

B4 >=6PP- READY

A RB7
R EA DY

PFB1
PPA4PartsFeeder

T1C1ICB7> =3AR A7IC

PFA 1

PP B4Pick& Convey - Arm Turn tableer1Robot
Placedriver

T2Conveyer 1

AR A12A8

PP B2PP
PPA2
PPA2L14 ｝

Intervene module

TTA 1 3A RA12>=6AR

AR A14T
TT>=3A RA 10e ARA 10

AR A6-eA8
PPA2（ 49）

（ 40）

A RA 15

AR A10T
TT（ 38）

A 12

A 14>=3A10READY

C1PDBTARTTA 1 3A RA 12>=6AR>=3TTA8T
AR A10T
A RA10A RA 10PF -READYREADY

PDATe >=32

TTA 8>=3ARA 10T

AR A14PFB1AR A9T

PPB2 AR sA 10A RA 10T

A RA10T

A RA 14T

AR>=3TTA 8ARPPA2

AR A14A RA 7

PFB1 >=1

PPA2eA7

ARA 7>=3

PFA1 > =1e

L14 ｝(D4)制御モジュール

AR A6>=3

PFA1PF READY（ 45）（ 44）

T1｛ L8,L10, L11

T3Conveyer
2 & S1

Conveyer Conveyer
2 & S2
2 & S3ControlModule(1)

Control
Module(2)

Control
Module(3)

T4
Conveyer
2 & S4ControlModule(4)

階層3、１７７個の状態から成る

図 7 制御系設計手法の流れ

NamemoduleIconv-Interference
Process

A1 -{PFParts feeder Treatment
Call
Conveyer1
part
EventCondi- PF- - READY
Watch-End-of-Linetion
CallTreatment
part
PDAT- -e ・・・- ・・Treat - Intervene Iconv
Part・Treat- Leave PF
PF- READY
mentment
part
Broadcast IC-End-of-Line
Parts Feeder End
Call

Conveyer1
stop
Conveyer1advance

partEnterB

PC

Input

State1件 条○ イベントモジュール
Event5部 ○ タイマーモジュール
State1 Sta
Event5
Leave
処 件条
部 ○ プロセスモジュール
State1 te1Sta
Event5
Leave
理 処件条
Call
Ac
部件
State1 t1 te1
Event5部 理処
Leave
Sta
Call
Broad
EvAc部
Event5 entt1te1
部理処
Leave
Sta
Call
Ac
cast
Broad
Enter
StaEv
部理Leave te2
Sta
t1te1
1 Sta
CallAccastent
Broad
EvEnter部
te1
t1Ac
1Sta
Call
castent
Broad
Ev
te2
Enter
t1
1 Sta
castent
Broad
Ev
te2
Enter1St
castenteEnter

性質検証

コントローラ（インタプリタ）

PF -A1177個の実行モジュール(コントローラへの入力データ)

#0原料ﾀﾝｸ#1原料ﾀﾝｸ#0原料ﾀﾝｸ

A1重合缶

B1重合缶

C1重合缶

A2重合缶

B2重合缶

C2重合缶

洗浄装置

ｽﾄﾚｰｼﾞﾀﾝｸ

図 8 バッチ型化学プラント

対象システムの挙動モデル（拡張時間ステートチャート）

検証性質仕様 調べたい
性質
（TCTL形式）例：E((start∨C）∪B)=<25

挙動モデルが引き起こし得る可能世界に展開

拡張時間
Kripke構造
生成器

拡張時間Kripke構造

モデルチェッカ（ラベリングアルゴリズム）

検証結果

可能世界とそれらの到達可能性を表すネットワーク構造

調べたい性質に関する検証を可能世界上で全数探索的に行わせる

図 9 検証手法の基本構造

実験結果

確認済み： 済
一部確認済み： (済)有効： ○
一部有効： ●
別なアプローチの検討を要する： 要検討

ネットワーク型
検証対象 バッチ型
化学プラント FA実験装置 生産システム
研究テーマ
○
○
○
済済
済
挙動表現モデル
(済) ●
(済) ●
(済) ●
性質検証手法プロセスネットワーク○
要検討によるモデル化手法 済 要検討 済
モデルに基づく
要検討 (済) ●要検討
制御系設計手法

図 10 提案手法の有効性を検証するための実験の結果