Think Stitch
PRINCIPIA  最近の更新


プロセス RUNA によるプロセスの抽象化

プロセス RUNAを使うとプロセスに対してある種の抽象化を施すことができます。 その方法についてご紹介します。

アルファベットと部分仕様

規模の大きなシステムの場合、例えば仕様を機能に分けて別々に記述することがあります。 この機能ごとに分けて記述された仕様を、ここでは仮に部分仕様と呼ぶことにします。

モデルで使用するすべてのイベントの集合、つまりアルファベット Σ に対して、部分仕様が仕様するイベントの集合 A は一部分だけになるでしょう。 左側の図のような感じです。 より一般的には、アルファベット Σ には設計上コンポーネント間の相互作用で使われるイベントも含まれますから、仕様で使うイベント、つまりシステムの外部から観測することのできるイベントの集合 B は一部分になります。 部分仕様が使うイベントは、さらにその部分になります。 つまり右の図のような関係になります。

システムの設計モデルを作って、内部イベントを隠蔽した後では、外部から観測できるイベントの集合は B になります。 しかし部分仕様はイベント A だけを使って書かれていますから、このままでは比較することができません。

ここでプロセス RUNA を使います。 RUNA は A に属するイベントだけを発生させますから、同期リストにアルファベット Σ を指定して設計プロセスと並行合成すると、A に含まれていないイベントの発生が禁止されます。 したがって、設計プロセスから A に関係する部分だけを切り出すことができます。 並行合成演算子がはさみで、プロセス RUNA は自在定規のような感じです。

こうして切り取ったあとの残りのプロセスであれば、部分仕様と比較することができます。

簡単な例として、音楽プレーヤのモデルを考えます。 プレーヤには play, next, prev の3つのボタンがあって、それぞれ再生停止、次の曲へ移動、前の曲へ移動を意味するものとします。 例えば次のようなモデルを考えることができます。再生中の曲番号は省略しました。 (音の再生開始と停止のイベント snd.start, snd.stop はシグナルイベントだとしておきます。シグナルイベントについては SyncStitch ユーザガイドを見てください。)

いま、再生に関してだけ記述してある部分仕様があるとしましょう。 これと上のモデルを比較するには next, prev イベントがじゃまです。 そこで次のようにして next, prev に関する部分を切り取ります。

(define-process Q
  (let ((A (list play snd.start snd.stop)))
    (par Events Idle (RUN A))))

その結果、状態遷移グラフは次のようになります。 next, prev に関する遷移が切り取られていることが確認できます。

あとは部分仕様と比較検査をすればよいわけです。

プロセス RUNA による抽象化の注意点

プロセス RUNA によるプロセスの抽象化には、1つ注意する点があります。 例で説明します。

電源オフの仕様を追加することにします。 イベント power-off で電源オフ操作を表します。 ボタンを追加すると考えてもいいですし、例えば play ボタンの長押しで power-off イベントが発生すると考えてもいいでしょう。 いずれにしても power-off イベントが発生したら、ほんとに終了してよいかどうか確認することにします(よくない仕様ですけど)。 メッセージを表示して、ユーザからの回答を next, prev ボタンで受け取ることにします。 next ボタンが押されたら終了します。prev ボタンが押されたら Idle 状態に戻ります。

モデルは次のようになります。

再生と終了についてだけみるために、先ほどと同じように next と prev を切り取ります。

(define-process Q1
  (let ((A (list play power-off snd.start snd.stop)))
    (par Events Idle1 (RUN A))))

このプロセスにはデッドロックがあります。

状態遷移グラフは次のようになります。

一般に、機械的な抽象化にはこのような欠点がありますけれども、それでもこの機能に関する部分だけ大雑把に見たいというような場合には便利です。

2013/10/05
© 2013,2014,2015 PRINCIPIA Limited