Think Stitch
PRINCIPIA  最近の更新


プロセスの比較 1: トレース

この文書は SyncStitch ユーザガイド 第14章からの抜粋です。

トレースによるプロセスの比較

この章と次の章では2つのプロセスを比較する機能について説明します。プロセスを比較する機能を使うと、設計したプロセスが仕様を満たしているかどうか検査することができます。

SyncStitch は基準の異なる2種類の比較を行うことができます。 この章ではそのうちの1つであるトレースによる比較について説明します。

はじめに、プロセスを比較するとはそもそも何をどうすることなのか、ということについて考えます。 結論として比較を行うための1つの基準を示します。次にリーダ・ライタ問題を例に、トレースによる比較の使い方と結果の見方を説明します。

この章で説明する項目:

  • トレースとトレース集合 traces(P)
  • トレース比較とトレース違反
  • 安全性

プロセスの比較とは?

はじめに、「2つのプロセスが同じとはどういう意味か」ということを考えてみます。 プロセスは状態遷移図またはプロセス式で表すことができます。 だからといってプロセスが同じとは状態遷移図が同じという意味ではありません。 例えば次の2つの状態遷移図を考えます。左の方は状態が1つ、右の方は2つありますから、異なる状態遷移図です。

しかしどちらもイベント a だけを限りなく発生させるという点では同じプロセスを表していると考えられます。 比較したいのは表現の形ではなくて、それが表している動作です。

ここで比較したい動作は、システムを利用する立場から見た動作です。 設計においてプロセスを比較する直接の目的は、設計したシステムが仕様を満たしていることを確認することです。 さらに根本に戻って、なぜ仕様を満たさなければならないのかというと、仕様が利用者と設計者の間の合意だからです。 利用者は仕様を見て、システムが何をして何ができるのかを知り、自分の目的を果たすために役に立つと判断します。 設計者は、利用者が仕様から期待している動作を満たすために、仕様を満たす設計を行わなければなりません。 したがって仕様を満たしているかどうかを判断するために行うプロセスの比較では、システムを利用者の立場から見た動作について問題にする必要があります。 システム内部の作りや内部の動作は異なっていてもかまいません。

システムを利用する立場から見た動作とは、システムを外から見たときに見える動作ということです。 システムを外から見たときに見えるのは、利用者とシステムの間の相互作用です。 具体的にはイベントの発生とチャネル通信です。 チャネル通信は原理的にイベントの発生と同じように扱うことができますから、イベントだけを考えればよいことになります。 これに対して内部遷移は外から見ることができないので、内部イベント tau は対象のイベントにはしません。 終了イベント tick は見ることができると考えます。 そうでなければ停止と終了を区別できないからです。

すると考えるべき問題は、外から見えるイベントだけに注目したときに、プロセスが同じかどうかを、プロセスの表現から判断する方法を求めることです。 この問題に対するアプローチは2つあります。1つはプロセスの表現を直接比較する基準を作ることです。 この基準は、表現の違いや内部動作の違いを無視するものでなければなりません。 もう1つは、プロセスの表現を、同じかどうか判断できる別の表現に変換することです。 ここでは後者のアプローチを取ります。理由は、比較のために用意する表現が他の用途でも役に立つからです。

トレース

外から見えるシステムの動作を表すために、発生するイベントをただ集めても十分ではありません。 同じイベントを発生させるプロセスはいくらでもあるからです。 次に考えるべきはイベントが発生する順序です。そこでシステムを起動してからある時間だけ観察して、その間に発生したイベントと順序を記録するとします。 観察の結果は、発生したイベントを発生した順番に並べた列として表すことができます。 このイベントの列が、システムの1つの動作を表していると考えることができます。

プロセスが発生させることのできるイベントの列を、プロセスのトレースといいます。トレースはプロセスを外から観察したときに見ることのできるイベントの列です。 「トレース」という言葉の元の意味は「足跡」という意味です。 まさにプロセスが実行後に残した足跡というわけです。

例えば次の状態遷移図で表されるプロセスを考えます。

このプロセスを実行するシステムを観察すると、次のようなトレースが発生する可能性があります。

()
(a)
(a b)
(a b c)
(d)
(d e)

システムはいつでもまったく同じトレースを発生させるわけではありません。利用者が行う選択によって、上のように異なるトレースが発生することがあります。

観察というのはふつう限られた時間で行うので、その時間内に発生したイベントだけが記録されます。 例えばトレース (a b) は、イベント c が発生する前に観察を終えたということを意味します。 空のトレース () は、観察中に何も起こらなかったということを意味します。

トレース集合

状態遷移図から明らかなように、上に示したトレースの一覧は、このプロセスが発生させることのできるトレースのすべてです。 これ以外にこのプロセスが発生させることのできるトレースはありません。 したがって、あるプロセスが一覧にないトレースを発生させれば、異なるプロセスであることがわかります。 しかしプロセスが発生させるトレースが、いつでも一覧にあるいずれかのトレースと同じであれば、少なくともトレースだけではプロセスを区別することができません。 そこで、プロセスが発生させることのできるトレースをすべて集めたものを、プロセスを比較するための表現として使うことを考えます。

プロセスが発生させることのできるすべてのトレースの集合をトレース集合といいます。 プロセスを比較するための表現として、つまり「もの」として扱うために、数学の集合の考え方を使います。 トレース集合は、状態遷移図、プロセス式と並んで、動作を表すための第3の表現だということです。

プロセスを比較するための基準の1つとして、トレース集合が同じであるということを使います。 この考え方を簡潔に表すために記号を用意します。 プロセス P のトレース集合を記号 traces(P) で表すことにします。 この記号を使うと、2つのプロセス P と Q がトレースを観察している範囲で同じということを

と表すことができます。トレース集合が同じというのは、トレース集合に含まれているトレースがすべて同じという意味です。

トレース集合の導出

ここまでのところで、プロセスのトレース集合がわかれば、プロセスの比較ができるということになりました。次に必要なことは、プロセスの表現である状態遷移図やプロセス式からトレース集合を求めることです。

状態遷移図の場合

状態遷移図からトレース集合を求める手順はほぼ明らかです。 ただし2点だけ注意すべきところがあります。 1つは tau 遷移がある場合、もう1つは循環がある場合です。

内部イベント tau は外から見えないので、トレースに含めません。 したがって例えば、次の2つの状態遷移図は同じトレース集合に対応します。

トレース集合は次のようになります。

()
(a)
(a b)

状態遷移図に循環がある場合は、発生するトレースが無限にあります。いくらでも長いトレースがあるからです。例えば次の状態遷移図を考えます。

このトレース集合はイベント a, b が交互に現れる任意の長さのトレースを持ちます。

()
(a)
(a b)
(a b a)
(a b a b)
(a b a b a)
...

このような場合、すべてのトレースを書き下すことはできません。しかし概念としては無限の要素を持つ集合として考えることができます。無限といってもランダムなわけではなく規則性があるので、あるトレースが与えられたとき、この集合に含まれているかどうかは規則に当てはまるかどうかで判定することができます。同じように、規則を比較することで、無限の要素を持つトレース集合が同じ集合であるかどうか判定することができます。したがってトレース集合が無限の要素を持っていても、プロセスの比較を行うことはできます。

循環を作る遷移がすべて tau 遷移の場合、つまり発散の場合、その部分はトレースに現れません。例えば次のような例を考えます。

内部イベント tau は見えないので、トレース集合は次のようになります。

()
(a)
(a b)

しかしイベント b が発生するかどうかはわかりません。 tau 遷移のループから抜け出す保証がないからです。 そのため、この状態遷移図に対応するトレース集合が何であるかということについては議論の余地があります。ここでは上の集合がこの状態遷移図のトレース集合であると考えておきます。

プロセスが発散するということは設計に問題があるということです。この場合、先にや るべきことは発散をなくすことです。実際の開発で、発散の後に何が起こりうるかを問 題にすることはほとんどありません。そのため発散の後のトレースを気にする必要はあ りません。

プロセス式の場合

次にプロセス式からトレース集合を求める場合について考えます。プロセス式の構成要素のうち、状態遷移図の構成要素に対応するイベント同期、チャネルの送受信、選択 alt, 非決定的選択 ndc, 場合わけ if については、どのようなトレースを発生させるか明らかです。問題は並行合成と隠蔽です。

並行合成については、第9章と第11章で単一の状態遷移図に変換する方法を説明しました。これを使えば状態遷移図を経由してトレース集合を求めることができます。

プロセス式に隠蔽 (hide X P) がある場合は次のようにします。 まず隠蔽の対象になっているプロセス P がプロセス式である場合は、状態遷移図に変換します。 次に状態遷移図の遷移のうち、隠蔽リスト X に含まれているイベントやチャネルの付いている遷移を、すべて tau 遷移に置き換えます。 結果として得られた状態遷移図は、元のプロセス式 (hide X P) と同じプロセスを表しています。これからトレース集合を求めることができます。

利用者と設計者の立場の違い

トレース集合を、プロセス内部の作りを表す状態遷移図やプロセス式から求めることについて、説明しておきたい点があります。トレースはプロセスを外から観察したときに得られるものですが、だからといってトレース集合が観察で得られるわけではありません。トレース集合は、プロセスが発生させることのできるすべてのトレースの集合です。ポイントは「すべて」というところにあります。観察の時間が限られているように、ふつうは観察の回数にも限りがあります。トレース集合を観察から得ることができないのは、限られた時間、限られた回数の観察ではすべてのトレースを得ることができないことがあるからです。1回の観察の時間を延ばしても、回数を増やしても、有限である限りは同じことです。

例えば、トレース (a b) について説明をしたときに、「イベント c が発生する前に観察を終えた」といいました。 これは状態遷移図でイベント c が起こることを知っているからいえることであって、外から見ている観察者にはわからないことです。 別の観察でトレース (a b c) が得られれば、トレース (a b) の後にイベント c が起こる可能性のあることがわかります。 ではトレース (a b c) の後に何かイベントが起こるということがわかるでしょうか。 何度観察を行ってもイベントは発生しないかもしれません。 観察時間を延ばしても発生しないかもしれません。 ではイベントは発生しないといえるでしょうか。 これはいえません。 なぜなら、もう少し長い時間観察していたら、あるいは次の観察で、イベントが発生するかもしれないからです。

トレース集合を求めるには、プロセス内部の作りについての情報が必要です。具体的には状態遷移図かプロセス式が必要です。 このことは一見、利用者の立場から見るという考え方と矛盾しているように思われるかもしれません。 しかしそうではありません。 トレースが異なっていれば、利用者は必ず違いに気づきます。 しかしトレース集合が異なっていても、異なる部分に相当するトレースがたまたま発生しなければ、利用者は気がつきません。 これはトレース集合が観察では得られないのと同じことです。 設計者はこのような運のよい偶然に期待することはできません。 利用者が気づく可能性のある違いが発生しないことを、設計者は確実に保証しなければなりません。 これを保証するためにはプロセス内部の作りについての情報が必要だということです。 プロセスが同じかどうかの判断の基準は、あくまでも利用者の立場から見えるものになりますが、それを保証する設計者の立場では、プロセス内部の情報が必要だということです。 このことは、次の章で非決定性を持つプロセスを区別するときにも必要になります。

仕様と実装の比較

「2つのプロセスが同じとはどういう意味か」ということについて、「トレース集合が同じである」という1つの基準を得ました。 次に「仕様を満たすとはどういう意味か」ということについて考えます。システムの仕様を表すプロセスと、設計したシステムを表すプロセスがあるとき、設計したシステムが仕様を満たすという条件は、2つのプロセスが同じということではありません。仕様では実装に対する選択の幅が与えられていることがあるからです。選択の幅は非決定的選択を使って表されます。仕様に含まれる非決定的選択は、どれを選んで実装してもよいという意味になります。結果として、設計したシステムが仕様を満たしていたとしても、2つのプロセスが異なる場合があります。したがって仕様を満たしているかどうかを判断するためには、「プロセスが同じである」ということとは別の基準が必要になります。

例えば次のプロセスを考えます。これが仕様を表しているとします。名前を SPEC とします。非決定的選択があるので、どちらを選んで実装してもよいという意味になります。

次のプロセスは設計で作ったシステムのプロセスだとします。名前を IMP とします。以後、設計で作ったプロセスのことを実装のプロセスと呼ぶことにします。実装といってもコードで書かれたプログラムやコンパイルされたオブジェクトのことではなくて、状態遷移モデルのことです。実装のプロセス IMP は仕様のプロセス SPEC が持つ非決定的選択の選択肢の1つと一致するので、仕様を満たします。

各プロセスのトレース集合は次のようになります。

()
(a)
(a b)
(c)
()
(a)
(a b)

プロセス IMP は仕様 SPEC を満たしているのに、このようにトレース集合 が異なるので、同じプロセスではありません。

プロセス SPEC と IMP のトレース集合を見比べると、プロセス IMP のトレースはすべてプロセス SPEC のトレースでもあることがわかります。数学的にいうと、traces(IMP) は traces(SPEC) に含まれているということです。一般に仕様を表すプロセスのトレース集合と、仕様を満たすプロセスのトレース集合の間にはこのような関係が成り立ちます。理由は次のように考えるとわかります。

もし仕様が持っていないトレースを実装が発生させるとしたら、仕様を満たしていないことになるからです。より詳しく考えてみるために、このようなトレースの1つを s とします。s に含まれるイベントを前から順番に見ていくと、途中までは仕様にも同じものがあるかもしれませんが、どこかで必ず仕様にないイベント e が現れることになります。この位置に対応する仕様の状態と実装の状態を考えると、仕様にはイベント e のついた遷移がないのに、実装の状態にはあることになります。実装はこのような遷移を勝手に付け加えているわけですから、仕様に違反しているということになります。したがって逆にいえば、実装が仕様を満たしているならば、実装のトレースはすべて仕様にも含まれているということになります。

すると仕様と実装のプロセスを比較するにはトレース集合が等しいかどうかではなくて、実装のトレース集合が仕様のトレース集合に含まれているかどうかを調べればよいということになります。数学的に記号で書くと、次のようになります。

記号 ⊆ は「含まれている」という意味を表します。実装が仕様を満たしていることを確認するために、実装を表すプロセスのトレース集合が仕様を表すプロセスのトレース集合に含まれているかどうか調べることを、トレース比較と呼ぶことにします。含まれていない場合をトレース違反といいます。

仕様に非決定的選択がある場合、仕様を表すプロセスのトレース集合には各選択肢に対応するトレースがすべて含まれています。一方、実装は選択肢の一部を任意に選ぶことができますから、選ばなかった選択肢の先に対応するトレースが欠けることになります。この場合、実装を表すプロセスのトレース集合は、仕様を表すプロセスのトレース集合の部分になります。仕様に非決定性がない場合と、実装がすべての選択肢を実装している場合は、2つのトレース集合が一致します。

トレース比較とトレース集合の一致

ときに2つの状態遷移モデルが全く同じ動作をするかどうか知りたいことがあります。 例えばコンポーネントを改良したときに、変更の前後で外から見た動作が変わっていないかどうかを確かめたい場合などです。

このためには2つのプロセスのトレース集合が同じであることが必要です。トレース集合が同じであるかどうかはトレース比較を使って調べることができます。2つの集合が同じであるとは、それぞれが他方に含まれているということだからです。したがって

を確認するには、順序を入れ替えてトレース比較を2回行えばよいことになります。

トレース比較がプロセスを区別する能力

トレース集合によってプロセスを比較する方法では、区別したいのに区別できない場合があります。例えば次の2つのプロセスを考えます。

左のプロセスには非決定性があり、右のプロセスにはないので、外から見た動作が異なる場合があります。具体的には、利用者がイベント c を提示したとき、右のプロセスは必ず同期しますが、左のプロセスはデッドロックすることがあります。しかしこの2つのプロセスは同じトレース集合を持っているので、トレース比較では区別することができません。この意味で、トレース比較がプロセスを区別する能力は期待より低いということになります。このことは、外から見える動作はトレースだけではないというということを意味します。トレース比較を改良して、より精密にプロセスを区別できるようにする方法を次の章で説明します。

イベントが必ず発生するという条件

トレース比較には、「あるイベントが必ず発生する」という条件を表すことができないという弱点があります。仕様が実装に対して要求する条件の強さは、仕様と実装を比較するために使用する基準の厳しさに対して相対的に決まります。トレース比較がプロセスを区別する能力が低いために、条件が弱くなることが原因です。

例えば、次のプロセスが仕様を表しているとします。仕様が意図する条件は、イベント a が発生した後で必ずイベント b が発生することです。それを強制するために、実装のトレース集合が仕様のトレース集合に含まれているだけでなく、同じであることを要求するとします。

しかし同じトレース集合を持つプロセスの中には、次のようなプロセスがあります。非決定的選択で下の分岐が選ばれた場合、イベント a が発生しても、そのあとイベント b が起こることはありません。このプロセスを実装とした場合、トレース比較では仕様に対する違反を見つけることができません。

問題の原因がプロセスを区別する能力の低さと同じであることから、この問題も次の章で解決されます。

安全性

トレース比較の能力が低いからといって役に立たないというわけではありません。仕様と実装の比較で見たように、実装が仕様で許されていない動作をしていないかどうかを判別することができます。トレース比較の意味は「一方のプロセスが発生させるトレースは、もう一方のプロセスも発生させることができる」ということです。これは実装が仕様を満たすために十分な条件ではありませんが必要な条件です。

実装が仕様で許されていない動作をするということは、何か悪いことが起こっているということです。実装が仕様で許されている範囲のことだけを行い、悪いことが起こらないという性質を安全性といいます。トレース比較は安全性を確認するために使うことができます。

トレース比較のまとめ

トレース比較のポイントについてまとめておきます。

  • プロセスが発生させる、外から見えるイベントの列をトレースといいます。
  • プロセスが発生させることのできるすべてのトレースの集合をトレース集合といいます。プロセス P のトレース集合を記号 traces(P) で表します。
  • トレース集合は状態遷移図またはプロセス式から求められます。
  • 2つのプロセス P と Q が同じであるためには、トレース集合が同じであることが必要です。記号で書くと traces(P) = traces(Q) です。
  • 実装プロセス IMP が仕様プロセス SPEC を満たすために必要な条件は、IMP のトレース集合が SPEC のトレース集合に含まれていることです。記号で書くと traces(IMP) ⊆ traces(SPEC) です。これを判定することをトレース比較といいます。
  • traces(IMP) ⊆ traces(SPEC) が成り立たない場合をトレース違反といいます。
  • traces(P) = traces(Q) を確認することは、traces(P) ⊆ traces(Q) と traces(Q) ⊆ traces(P) を両方確認することと同じです。
  • 実装が仕様に書かれていることだけを行い、悪いことをしないという性質を安全性といいます。トレース比較は安全性の確認に使うことができます。
  • トレース比較では非決定性のあるプロセスを区別できません。
  • トレース比較ではイベントが必ず発生するという条件を表すことができません。
2013/09/03
© 2013,2014,2015 PRINCIPIA Limited