(57)【要約】【課題】      スケジューリング機構の支配下で動作するプロセスを含むシステムの安全性、活性等の検証に適した検証装置等を提供する。【解決手段】    スケジューリング機構の支配下で動作するシステムには、例えば、プロセスＡが動作中に、プロセスＡよりも優先度の高いプロセスＢが割り込み、その後プロセスＢの処理が終わり、プロセスＡに戻ったとき、プロセスＡの状態は、プロセスＢの割り込み前のプロセスＡの状態と変わらないという特徴がある。（Ａ）にあるようなシステムの状態空間で検査を行っても、（Ｂ）にあるように、安全な状態遷移のみで簡約した状態空間だけで検査を行っても、同じ結果を得ることができる。【選択図】  図３
2008243122.tif 000002
【特許請求の範囲】
【請求項１】
スケジューリング機構の下で動作するプロセスを含むシステムを検証する検証装置であって、
任意の状態遷移に対し、状態が変更されるプロセスを決定し、このプロセスが同じになる状態遷移を束ねる束ね手段と、
前記束ね手段による束が１つ以上存在する場合に、１つ以上の束を束ねた太束が与えられた状態を開始点とする全状態遷移群と一致しないとき、任意の太束に含まれる状態遷移αと、与えられた状態（ｓ０）から始まる任意の状態遷移列β０・β１・…・βｎ−１に対し、
（１）全てのｘ∈［０…ｎ−１］に対しβｘ≠αならば、状態α（ｓ０）から始まる状態遷移列β０・β１・…・βｎ−１が存在し、
（２）あるｘ∈［０…ｎ−１］に対しβｘ＝αならば、任意のβｘ＝αとなるｘに対し、状態α（ｓ０）から始まる状態遷移列β０・β１・…・βｘ−１が存在し、（β０・β１・…・βｘ）（ｓ０）＝（β０・β１・…・βｘ−１）（α（ｓ０））である、
という条件（１）及び（２）を満たす太束を構成する太束構成手段と、
を有し、静的に利用可能な情報を使用して、前記システムを記述する状態空間の、与えられた状態を開始点とする全状態遷移群から部分状態遷移群を構成する部分状態遷移群構成手段と、
前記部分状態遷移群構成手段により構成された部分状態遷移群に対応する部分状態空間を構成する部分状態空間構成手段と、
前記部分状態空間構成手段により構成された部分状態空間を使用して検証する部分検証手段
を備える検証装置。
【請求項２】
状態遷移系Ｍ＝（Ｓ，Ｔ，Ｓ０，Ｌ）のシステムの検証を行う検証装置であって、
下記の簡約関数ｒを用いてＭの部分状態遷移系Ｍ’を構成する部分状態遷移系構成手段と、
前記部分状態遷移系構成手段により構成された部分状態遷移系Ｍ’の検証を行う部分検証手段
を備える検証装置。
【数１】
2008243122.tif 000015
【請求項３】
状態遷移系Ｍ＝（Ｓ，Ｔ，Ｓ０，Ｌ）のシステムの検証を行う検証装置であって、
下記の簡約関数ｒを用いてＭの部分状態遷移系Ｍ’を構成する部分状態遷移系構成手段と、
前記部分状態遷移系構成手段により構成された部分状態遷移系Ｍ’の検証を行う部分検証手段
を備える検証装置。
【数２】
2008243122.tif 000016
【請求項４】
スケジューリング機構の下で動作するプロセスを含むシステムを検証する検証方法であって、
束ね手段が、任意の状態遷移に対し、状態が変更されるプロセスを決定し、このプロセスが同じになる状態遷移を束ねるステップと、
太束構成手段が、前記束ねステップによる束が１つ以上存在する場合に、１つ以上の束を束ねた太束が与えられた状態を開始点とする全状態遷移群と一致しないとき、任意の太束に含まれる状態遷移αと、与えられた状態（ｓ０）から始まる任意の状態遷移列β０・β１・…・βｎ−１に対し、
（１）全てのｘ∈［０…ｎ−１］に対しβｘ≠αならば、状態α（ｓ０）から始まる状態遷移列β０・β１・…・βｎ−１が存在し、
（２）あるｘ∈［０…ｎ−１］に対しβｘ＝αならば、任意のβｘ＝αとなるｘに対し、状態α（ｓ０）から始まる状態遷移列β０・β１・…・βｘ−１が存在し、（β０・β１・…・βｘ）（ｓ０）＝（β０・β１・…・βｘ−１）（α（ｓ０））である、
という条件（１）及び（２）を満たす太束を構成する太束ステップと、
を含み、部分状態遷移群構成手段が、静的に利用可能な情報を使用して、前記システムを記述する状態空間の、与えられた状態を開始点とする全状態遷移群から部分状態遷移群を構成するステップと、
部分状態空間構成手段が、前記部分状態遷移群構成手段により構成された部分状態遷移群に対応する部分状態空間を構成するステップと、
部分検証手段が、前記部分状態空間構成手段により構成された部分状態空間を使用して検証するステップと、
を含む検証方法。
【請求項５】
コンピュータにおいて、請求項４記載の検証方法を実現させるためのプログラム。
【請求項６】
請求項５記載のプログラムを記録する記録媒体。
【発明の詳細な説明】
【技術分野】
【０００１】
本願は、検証装置、検証方法、プログラム、及び、記録媒体に関し、特に、システムの検証を行う検証装置等に関する。
【背景技術】
【０００２】
従来、状態の遷移を検証する場合に、状態空間から冗長な状態を削除する方法として、Partial  Order  Reductionと呼ばれる方法（以下、「ＰＯＲ」という。）が知られている（非特許文献１（特に、Chapter  10参照）、特許文献１等参照）。
【０００３】
ＰＯＲについて、図４を参照して説明する。図４は、ＰＯＲによるシステムの冗長な状態を削除の概要を示す図であり、（Ａ）にはシステムの状態空間が示され、（Ｂ）には検証に使用される簡約した状態空間が示されている。
【０００４】
ＰＯＲは、例えば各プロセスがそれぞれ別の計算機で動作するような、非同期プロセスからなるシステムを対象とする。非同期プロセスからなるシステムでは、それぞれのプロセスが独立に動作する。図４（Ａ）に示されるシステムの状態空間では、最初の状態１からプロセスＡの状態遷移ａにより状態２に遷移し、さらにプロセスＢの状態遷移ｂにより状態３に遷移し、また、最初の状態１からプロセスＢの状態遷移ｂにより状態４に遷移し、さらにプロセスＡの状態遷移ａにより状態３に遷移する。ここで、状態１、状態２、状態３、状態４での安全な状態遷移は、それぞれａ、ｂ、ｃ、ａとする。ここで、安全な状態遷移は、所定の数学的アルゴリズムにより決定されるものである。
【０００５】
プロセスＡの状態遷移ａとプロセスＢの状態遷移ｂが独立に動作し、ａ，ｂが不可視なとき、列ａ，ｂと列ｂ，ａは検査結果が同じになる。したがって、安全性又は活性があるかどうかについて、図４（Ａ）のように列ａ，ｂと列ｂ，ａというシステムの状態空間で検査を行っても、図４（Ｂ）のように列ａ，ｂという安全な状態遷移のみで簡約した状態空間を作成し、簡約した状態空間だけで検査を行っても、同じ結果を得ることができる。なお、独立及び不可視という概念については、後に説明する。
【０００６】
【非特許文献１】E．M．Clarke，Jr.、外２名著，“Model Checking”，MIT  Pr.，1999
【特許文献１】特開平７−３３４５６６号公報
【発明の開示】
【発明が解決しようとする課題】
【０００７】
しかしながら、プロセスが複数存在し、それらがスケジューリング機構の下で動作するシステムでは、スケジューリングという制約があるため、各プロセスは独立に動作しない。そのため、プロセスが独立であるという性質を利用したＰＯＲをスケジューリング機構の下で動作するシステムに適用しても、簡約した状態空間がシステムの状態空間と比べてあまり小さくならない。
【０００８】
そこで、本願発明の目的は、スケジューリング機構の下で動作するプロセスを含むシステムの検証に適した検証装置等を提供することにある。
【課題を解決するための手段】
【０００９】
請求項１に係る発明は、スケジューリング機構の下で動作するプロセスを含むシステムを検証する検証装置であって、任意の状態遷移に対し、状態が変更されるプロセスを決定し、このプロセスが同じになる状態遷移を束ねる束ね手段と、前記束ね手段による束が１つ以上存在する場合に、１つ以上の束を束ねた太束が与えられた状態を開始点とする全状態遷移群と一致しないとき、任意の太束に含まれる状態遷移αと、与えられた状態（ｓ０）から始まる任意の状態遷移列β０・β１・…・βｎ−１に対し、（１）全てのｘ∈［０…ｎ−１］に対しβｘ≠αならば、状態α（ｓ０）から始まる状態遷移列β０・β１・…・βｎ−１が存在し、（２）あるｘ∈［０…ｎ−１］に対しβｘ＝αならば、任意のβｘ＝αとなるｘに対し、状態α（ｓ０）から始まる状態遷移列β０・β１・…・βｘ−１が存在し、（β０・β１・…・βｘ）（ｓ０）＝（β０・β１・…・βｘ−１）（α（ｓ０））である、という条件（１）及び（２）を満たす太束を構成する太束構成手段と、を有し、静的に利用可能な情報を使用して、前記システムを記述する状態空間の、与えられた状態を開始点とする全状態遷移群から部分状態遷移群を構成する部分状態遷移群構成手段と、前記部分状態遷移群構成手段により構成された部分状態遷移群に対応する部分状態空間を構成する部分状態空間構成手段と、前記部分状態空間構成手段により構成された部分状態空間を使用して検証する部分検証手段を備えるものである。
【００１０】
請求項２に係る発明は、状態遷移系Ｍ＝（Ｓ，Ｔ，Ｓ０，Ｌ）のシステムの検証を行う検証装置であって、下記の簡約関数ｒを用いてＭの部分状態遷移系Ｍ’を構成する部分状態遷移系構成手段と、前記部分状態遷移系構成手段により構成された部分状態遷移系Ｍ’の検証を行う部分検証手段を備えるものである。
【００１１】
【数３】
2008243122.tif 000003
【００１２】
請求項３に係る発明は、状態遷移系Ｍ＝（Ｓ，Ｔ，Ｓ０，Ｌ）のシステムの検証を行う検証装置であって、下記の簡約関数ｒを用いてＭの部分状態遷移系Ｍ’を構成する部分状態遷移系構成手段と、前記部分状態遷移系構成手段により構成された部分状態遷移系Ｍ’の検証を行う部分検証手段を備えるものである。
【００１３】
【数４】
2008243122.tif 000004
【００１４】
請求項４に係る発明は、スケジューリング機構の下で動作するプロセスを含むシステムを検証する検証方法であって、束ね手段が、任意の状態遷移に対し、状態が変更されるプロセスを決定し、このプロセスが同じになる状態遷移を束ねるステップと、太束構成手段が、前記束ねステップによる束が１つ以上存在する場合に、１つ以上の束を束ねた太束が与えられた状態を開始点とする全状態遷移群と一致しないとき、任意の太束に含まれる状態遷移αと、与えられた状態（ｓ０）から始まる任意の状態遷移列β０・β１・…・βｎ−１に対し、（１）全てのｘ∈［０…ｎ−１］に対しβｘ≠αならば、状態α（ｓ０）から始まる状態遷移列β０・β１・…・βｎ−１が存在し、（２）あるｘ∈［０…ｎ−１］に対しβｘ＝αならば、任意のβｘ＝αとなるｘに対し、状態α（ｓ０）から始まる状態遷移列β０・β１・…・βｘ−１が存在し、（β０・β１・…・βｘ）（ｓ０）＝（β０・β１・…・βｘ−１）（α（ｓ０））である、という条件（１）及び（２）を満たす太束を構成する太束ステップと、を含み、部分状態遷移群構成手段が、静的に利用可能な情報を使用して、前記システムを記述する状態空間の、与えられた状態を開始点とする全状態遷移群から部分状態遷移群を構成するステップと、部分状態空間構成手段が、前記部分状態遷移群構成手段により構成された部分状態遷移群に対応する部分状態空間を構成するステップと、部分検証手段が、前記部分状態空間構成手段により構成された部分状態空間を使用して検証するステップと、を含むものである。
【００１５】
請求項５に係る発明は、コンピュータにおいて、請求項４記載の検証方法を実現させるためのプログラムである。
【００１６】
請求項６に係る発明は、請求項５記載のプログラムを記録する記録媒体である。
【００１７】
なお、検証の対象となるシステムは、スケジューリング機構の下で動作するプロセスを含むサブシステムを１つ以上含むものであってもよい。
【００１８】
また、部分検証手段による検証は、例えば、システムの安全性、活性を持つか否かなどである。
【発明の効果】
【００１９】
本願発明によれば、スケジューリング機構の下で動作するプロセスを含むシステムの特徴を利用し、スケジューリング機構の下で動作するプロセスを含むシステムに対し、より簡約した状態空間を作成して、安全性、活性等の検証を行うことが可能となる。
【発明を実施するための最良の形態】
【００２０】
図１は、本願発明の実施の形態に係る検証装置１の概略ブロック図である。以下、検証の対象となるシステムは、同一計算機上にプロセスが複数存在し、それらがスケジューリング機構の支配下で、常に１つだけ動作するシステム（以下、「平行プロセスからなるシステム」という。）であるとする。各プロセスには優先度が与えられており、動作するプロセスは、優先度により決定されるものとする。
【００２１】
図１を参照して、検証装置１は、静的に利用可能な情報（検証実行前に入手できる情報）を使用して検証対象のシステムを記述する状態空間から冗長な状態を除去して部分状態空間を構成する部分状態空間構成部３と、部分状態空間構成部３により構成された部分状態空間を使用して、安全性と活性の少なくとも一方を検証する部分状態空間検証部５を備える。
【００２２】
部分状態空間構成部３は、検証対象のシステムを記述する状態空間の、与えられた状態を開始点とする全状態遷移群から、検証に必要な部分状態遷移群を静的に構成する部分状態遷移群構成部７と、部分状態遷移群構成部７により構成された部分状態遷移群に対応する部分状態空間を構成する状態空間構成部９を有する。
【００２３】
部分状態遷移群構成部７は、任意の状態遷移に対して状態が変更されるプロセスを決定し、このプロセスが同じになる状態遷移を束ねる束ね部１１と、束ね部１１により束ねられた束が１つ以上あるかどうかを決定し、束が１つ以上存在する場合、１つ以上の束を束ねて太束を構成する太束構成部１３を有する。ここで、太束は、システムの安全性又は活性を検証するとき、全状態空間上で検証しても、太束に含まれる状態遷移だけで部分状態空間を構成し、その部分状態空間上で検証しても、結果が同じになることが数学的に証明できるよう構成されるものとする。
【００２４】
続いて、図１の検証装置１の動作について、図２を参照して説明する。図２は、図１の検証装置１の動作を示す処理フロー図である。
【００２５】
まず、束ね部１１は、任意の状態遷移に対し、状態が変更されるプロセスを決定し、このプロセスが同じになる状態遷移を束ねる（図２のステップＳＴ１）。続いて、太束構成部１３は、束ね部１１による束を束ね、太束を構成する（図２のステップＳＴ２）。ここで、太束は、任意の太束に含まれる状態遷移αと、与えられた状態（ｓ０）から始まる任意の状態遷移列β０・β１・…・βｎ−１に対し、（１）全てのｘ∈［０…ｎ−１］に対しβｘ≠αならば、状態α（ｓ０）から始まる状態遷移列β０・β１・…・βｎ−１が存在し、（２）あるｘ∈［０…ｎ−１］に対しβｘ＝αならば、任意のβｘ＝αとなるｘに対し、状態α（ｓ０）から始まる状態遷移列β０・β１・…・βｘ−１が存在し、（β０・β１・…・βｘ）（ｓ０）＝（β０・β１・…・βｘ−１）（α（ｓ０））である、という条件を満たすように構成される。
【００２６】
続いて、太束構成部１３は、与えられた状態を開始点とする全状態遷移群と一致しないか否かを判断する（図２のステップＳＴ３）。一致するならば図２のステップＳＴ７の処理に進み、一致しない場合には、さらに図２のステップＳＴ４以下の処理を行う。
【００２７】
図２のステップＳＴ４において、太束構成部１３は、太束の全状態遷移が不可視か否かを判断し、また、図２のステップＳＴ５において、サイクルに関する条件（後に記載する定義１１の条件３）を満たすように太束群が構成されているか否かを判断する。不可視で、かつ、定義１１の３を満たすように太束群が構成されていれば、図２のステップＳＴ７の処理に進み、不可視でないか、又は、定義１１の３を満たすように太束群が構成されていなければ、図２のステップＳＴ６に進む。なお、不可視及びサイクルについては、後に説明する（不可視は定義４において定義され、サイクルは定義５において定義される。）。
【００２８】
図２のステップＳＴ６において、太束構成部１３は、太束を、与えられた状態を開始点とする全状態遷移群にし、図２のステップＳＴ７の処理に進む。
【００２９】
図２のステップＳＴ７において、状態空間構成部９は、部分状態遷移群構成部７により構成された部分状態遷移群に対応する部分状態空間を構成し、図２のステップＳＴ８において、部分状態空間検証部５は、部分状態空間構成部３により構成された部分状態空間を使用して、安全性や活性を検証する。
【００３０】
続いて、図３を参照して、図１の部分状態空間構成部３により構成される、検証に使用される簡約した状態空間について説明する。図３は、従来技術（ＰＯＲ）の図４に対応する図であり、図１の部分状態空間構成部３によるシステムの冗長な状態を削除の概要を示す図であり、（Ａ）にはシステムの状態空間が示され、（Ｂ）には検証に使用される簡約した状態空間が示されている。
【００３１】
平行プロセスからなるシステムには、プロセスＡが動作中に、プロセスＡよりも優先度の高いプロセスＢが割り込み、その後プロセスＢの処理が終わり、プロセスＡに戻ったとき、プロセスＡの状態は、プロセスＢの割り込み前のプロセスＡの状態と変わらないという特徴がある。図３（Ａ）には、プロセスＡの状態遷移ａ（例えば、ローカル変数の値操作（値代入、加算、乗算など）など）、並びに、プロセスＢを起動する割り込みｂ及びプロセスＢの処理列ｃ、ｄ（ｄ実行後にプロセスＢはウェイト状態へ移行）の状態空間が示されている。最初の状態１１からプロセスＡの状態遷移ａにより状態１２へ遷移した後にプロセスＢの状態遷移ｂ、ｃ、ｄにより状態１３、１４、１５へ状態遷移し、また、プロセスＢの状態遷移ｂ、ｃ、ｄにより状態１６、１７、１８へ遷移した後にプロセスＡの状態遷移ａにより状態１５へ遷移している。なお、状態１１、１２、１３、１４、１５、１６、１７、１８における太束に含まれる状態遷移は、それぞれ、ａ、ｂ、ｃ、ｄ、ｅ、ｃ、ｄ、ａであるとする。ここで、太束に含まれる状態遷移は、所定の数学的アルゴリズムに基づいて決定されるものとする。
【００３２】
図３（Ａ）において、プロセスＢの優先度はプロセスＡの優先度よりも高い。そのため、状態１６においてプロセスＡの状態遷移ａはなく、図４（Ａ）にあるような独立の関係にない。そのため、従来技術であるＰＯＲによっては状態空間を簡約できない。
【００３３】
しかしながら、本実施例の検証装置１によれば、プロセスＡの状態遷移ａが不可視などの制約が少し加えられることとなるが、プロセスＡの状態遷移ａと、プロセスＡより優先度の高いプロセスＢを起動する割り込みｂ、プロセスＢの処理列ｃ，ｄに対し、列ａ，ｂ，ｃ，ｄと列ｂ，ｃ，ｄ，ａは検査結果が同じになる。したがって、図３（Ａ）にあるようなシステムの状態空間で検査を行っても、図３（Ｂ）にあるように、安全な状態遷移のみで簡約した状態空間を作成し、列ａ，ｂ，ｃ，ｄのみからなる簡約した状態空間だけで検査を行っても、安全性や活性があるかどうかに対して、同じ結果を得ることができる。
【００３４】
続いて、本発明の手法について、数学的な証明について説明する。まず、以下で用いる用語・概念等の定義を述べる。
【００３５】
【数５】
2008243122.tif 000005
【００３６】
ここで、安全性、活性の大部分は、LTL-X  formulaを用いて記述できることは知られている（例えば、特許文献１の第００３９段落参照）。
【００３７】
【数６】
2008243122.tif 000006
【００３８】
続いて、組込み向け簡約関数ｒを以下のように定義する。
【００３９】
【数７】
2008243122.tif 000007
【００４０】
非特許文献１のｐ．１４７に記載されているように、状態遷移系M=(S,T,S0,L)、M'=(S',T',S'0,L')がstuttering等価なとき、任意のLTL-X  formula  Af、任意の初期状態s∈S0=S'0に対し、（１）式が成り立つ。
【００４１】
【数８】
2008243122.tif 000008
【００４２】
状態遷移系Ｍ、LTL-X  formula  Af（状態遷移が不可視かどうかに関係）が与えられたとき、組込み向け簡約関数ｒを用いて構成されたＭの部分状態遷移系をＭ’とする。ＭとＭ’がstuttering等価であることを示せば、（１）式が成立し、LTL-X  formula  Afを検証する際、Ｍの代わりにＭ’上で検証すればよいこととなる。すなわち、下記の定理１が成立することを示せばよい。
【００４３】
【数９】
2008243122.tif 000009
【００４４】
従来技術（非特許文献１、特許文献１など）では、定義１１の条件１を下記定義１２の条件１に代えた簡約関数ｒ０を用いてＭの部分状態遷移系Ｍ’を構成している。従来技術の証明の流れ（非特許文献１のｐ．１６０−ｐ．１６４）に沿って、以下説明する。
【００４５】
【数１０】
2008243122.tif 000010
【００４６】
従来技術の証明の流れは、まず、無限パスの列π０＝σ，π１，・・・を構成し、π０，π１，・・・（η０，η１，・・・）の極限としてηを構成し、ηがＭ’に属することを示し、最後に、σとηがstuttering等価なことを示している。
【００４７】
従来技術の証明の流れを詳細に検討すると、最初に、簡約関数ｒ０の条件１を用いてπi+1の構成方法のθi+1とηi+1の存在を示し、証明の残りの部分では、条件１を使うことはなく、θi+1とηi+1が存在することを使うのみである。
【００４８】
そこで、定理１の証明では、まず、任意のＭの初期状態から始まる無限パスσに対し、以下のように、無限パスの列π０，π１，・・・を構成する。
【００４９】
【数１１】
2008243122.tif 000011
【００５０】
無限パスπ０，π１，・・・の構成において、定義１１の条件１を用いて、πi+1の構成方法の2(a)、2(b)のθi+1とηi+1の存在を示した。証明の残りの部分については、従来の証明と同様である。
【００５１】
よって、定理１が成り立つことが証明された。
【００５２】
続いて、表１を用いて、本発明の状態空間縮小方法の有効性について説明する。表１では、状態数が２６、状態遷移数が４６の状態空間の一部を対象としている。一般向けのＰＯＲによる縮小では、状態数が２３、状態遷移数が３４であり、組込み向けＰＯＲでは、状態数が１８、状態遷移数が２２である。これに対し、本発明の組込み向け状態空間縮小方法では、状態数が１３、状態遷移数が１５まで縮小されている。
【００５３】
【表１】
2008243122.tif 000012
【００５４】
なお、定義１１により定義される組込み向け簡約関数以外に、例えば、定義１３により定義される組込み向け簡約関数を用いて部分状態遷移系を構成し、安全性を解析するようにしてもよい。定義１３は定義１１の条件３を緩和するものである。定義１３による組込み向け簡約関数を用いた場合、システムの安全性を検証することができる。
【００５５】
【数１２】
2008243122.tif 000013
【００５６】
ここで、witnessは、D.Bosnacki、外１名著，“Improving  Spin's  Partial-Order  Reduction  for  Breadth-First  Search”，LNCS3639，pp.91-105で導入された概念であり、定義１４のように定義されるものである。
【００５７】
【数１３】
2008243122.tif 000014
【図面の簡単な説明】
【００５８】
【図１】本願発明の実施の形態に係る検証装置１の概略ブロック図である。
【図２】図１の検証装置１の動作を示す処理フロー図である。
【図３】従来技術（ＰＯＲ）の図４に対応する図であり、図１の部分状態空間構成部３によるシステムの冗長な状態を削除の概要を示す図であり、（Ａ）にはシステムの状態空間が示され、（Ｂ）には検証に使用される簡約した状態空間が示されている。
【図４】ＰＯＲによるシステムの冗長な状態を削除の概要を示す図であり、（Ａ）にはシステムの状態空間が示され、（Ｂ）には検証に使用される簡約した状態空間が示されている。
【符号の説明】
【００５９】
１  検証装置、３  部分状態空間構成部、５  部分状態空間検証部、７  部分状態遷移群構成部、９  状態空間構成部、１１  束ね部、１３  太束構成部
【図１】
2008243122.tif 000017
【図２】
2008243122.tif 000018
【図３】
2008243122.tif 000019
【図４】
2008243122.tif 000020