(57)【要約】【課題】ＬＴＬ式に不慣れな者であっても、ＬＴＬ式を容易に確認することができるＬＴＬ式確認システム、ＬＴＬ式確認方法及びＬＴＬ式確認プログラムを提供する。【解決手段】ＬＴＬ式確認システム１００に、ＬＴＬ式に含まれる変数が所定の系列長でとりうる値である変数値系列の組み合わせを生成する変数値系列集合生成手段３と、変数値系列集合生成手段３により生成された変数値系列がＬＴＬ式に代入された場合に、ＬＴＬ式が成立するか否かを判定するＬＴＬ式判定手段４と、を備えた。【選択図】図１
2009187416.tif 000002
【特許請求の範囲】
【請求項１】
ＬＴＬ（Linear  Temporal  Logic）式に含まれる変数が所定の系列長でとりうる値である変数値系列の組み合わせを生成する変数値系列集合生成手段と、
前記変数値系列集合生成手段により生成された前記変数値系列が前記ＬＴＬ式に代入された場合に、前記ＬＴＬ式が成立するか否かを判定するＬＴＬ式判定手段と、
を備えるＬＴＬ式確認システム。
【請求項２】
前記ＬＴＬ式判定手段による判定結果が同じであり、且つ、値の違いが１箇所である前記変数値系列同士をマージする変数値系列マージ手段を備える請求項１に記載のＬＴＬ式確認システム。
【請求項３】
前記変数値系列と前記判定結果とを対応付けて表示する結果表示手段を備える請求項１又は２に記載のＬＴＬ式確認システム。
【請求項４】
ＬＴＬ（Linear  Temporal  Logic）式に含まれる変数が所定の系列長でとりうる値である変数値系列の組み合わせを生成し、
生成した前記変数値系列を前記ＬＴＬ式に代入した場合に、前記ＬＴＬ式が成立するか否かを判定するＬＴＬ式確認方法。
【請求項５】
判定結果が同じであり、且つ、値の違いが１箇所である前記変数値系列同士をマージする請求項４に記載のＬＴＬ式確認方法。
【請求項６】
前記変数値系列と前記判定結果とを対応付けて表示する請求項４又は５に記載のＬＴＬ式確認方法。
【請求項７】
ＬＴＬ（Linear  Temporal  Logic）式に含まれる変数が所定の系列長でとりうる値である変数値系列の組み合わせを生成する変数値系列集合生成処理と、
前記変数値系列集合生成処理により生成された前記変数値系列が前記ＬＴＬ式に代入された場合に、前記ＬＴＬ式が成立するか否かを判定するＬＴＬ式判定処理と、
をコンピュータに実行させるＬＴＬ式確認プログラム。
【請求項８】
前記ＬＴＬ式判定処理による判定結果が同じであり、且つ、値の違いが１箇所である前記変数値系列同士をマージする変数値系列マージ処理をコンピュータに実行させる請求項７に記載のＬＴＬ式確認プログラム。
【請求項９】
前記変数値系列と前記判定結果とを対応付けて表示する結果表示処理をコンピュータに実行させる請求項７又は８に記載のＬＴＬ式確認プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ＬＴＬ式確認システム、ＬＴＬ式確認方法及びＬＴＬ式確認プログラムに関する。
【背景技術】
【０００２】
従来から、ソフトウェアやハードウェアの動作仕様を検査する方法として、モデル検査法が知られている。モデル検査法とは、状態遷移と検証項目を入力し、状態遷移が検証項目に違反しないか否かにより、動作仕様を検査する方法である。
【０００３】
モデル検査法では、通常、状態遷移が、モデル記述言語により記述される。そこで、特許文献１では、モデル記述言語を用いた状態遷移の作成を支援する技術が記載されている。
【特許文献１】特開２００７−０１１６０５号公報
【発明の開示】
【発明が解決しようとする課題】
【０００４】
一方、モデル検査法において、検証項目は、通常、ＬＴＬ（Linear  Temporal  Logic：線形時相論理）式などの時相論理式で記述される。そのため、検証項目の作成には、時相論理式の知識が必要となる。従って、ＬＴＬに不慣れな者が検証項目を作成するのは難しい。
具体的には、ＬＴＬ式は抽象的であるため、作成したＬＴＬ式が所望する検証項目を反映しているか否かを確認することが難しい。
【０００５】
本発明は、ＬＴＬ式に不慣れな者であっても、ＬＴＬ式を容易に確認することができるＬＴＬ式確認システム、ＬＴＬ式確認方法及びＬＴＬ式確認プログラムを提供することを目的とする。
【課題を解決するための手段】
【０００６】
本発明の第１の態様にかかるＬＴＬ式確認システムは、ＬＴＬ（Linear  Temporal  Logic）式に含まれる変数が所定の系列長でとりうる値である変数値系列の組み合わせを生成する変数値系列集合生成手段と、前記変数値系列集合生成手段により生成された前記変数値系列が前記ＬＴＬ式に代入された場合に、前記ＬＴＬ式が成立するか否かを判定するＬＴＬ式判定手段と、を備えるものである。
【０００７】
また、本発明の第２の態様にかかるＬＴＬ式確認方法は、ＬＴＬ（Linear  Temporal  Logic）式に含まれる変数が所定の系列長でとりうる値である変数値系列の組み合わせを生成し、生成した前記変数値系列を前記ＬＴＬ式に代入した場合に、前記ＬＴＬ式が成立するか否かを判定するものである。
【０００８】
また、本発明の第３の態様にかかるＬＴＬ式確認プログラムは、ＬＴＬ（Linear  Temporal  Logic）式に含まれる変数が所定の系列長でとりうる値である変数値系列の組み合わせを生成する変数値系列集合生成処理と、前記変数値系列集合生成処理により生成された前記変数値系列が前記ＬＴＬ式に代入された場合に、前記ＬＴＬ式が成立するか否かを判定するＬＴＬ式判定処理と、をコンピュータに実行させるものである。
【発明の効果】
【０００９】
本発明により、ＬＴＬ式に不慣れな者であっても、ＬＴＬ式を容易に確認することができる。
【発明を実施するための最良の形態】
【００１０】
以下に、本発明を適用可能な実施形態を説明する。なお、本発明は、以下の実施形態に限定されるものではない。
【００１１】
実施形態１．
本発明の実施形態１にかかるＬＴＬ式確認システム１００について、図１を参照しながら説明する。ＬＴＬ式確認システム１００は、図１に示すように、変数値系列集合生成手段３、ＬＴＬ式判定手段４を有している。さらに、ＬＴＬ式確認システム１００は、ＬＴＬ式入力手段１、系列長入力手段２、結果表示手段５等を有している。
ＬＴＬ式確認システム１００は、ＣＰＵ（Central  Processing  Unit；図示省略）等を備えるコンピュータ（図示省略）等を有している。そして、ＣＰＵが、ＬＴＬ式確認システム１００の各種機能を実現するためのプログラムを実行することにより、ＬＴＬ式確認システム１００の各種機能が動作する。具体的には、ＣＰＵは、ＬＴＬ式確認プログラムを実行することにより、ＬＴＬ式入力手段１、系列長入力手段２、変数値系列集合生成手段３、ＬＴＬ式判定手段４、結果表示手段５として機能する。
【００１２】
ＬＴＬ式入力手段１は、ユーザにより入力されたＬＴＬ式を読み込み、変数値系列集合生成手段３において処理可能な形式に変換する。そして、ＬＴＬ式入力手段１は、変換したＬＴＬ式を変数値系列集合生成手段３に入力する。
また、ＬＴＬ式入力手段１は、ユーザにより入力されたＬＴＬ式をＬＴＬ式判定手段４０において処理可能な形式に変換する。そして、ＬＴＬ式入力手段１は、変換したＬＴＬ式をＬＴＬ式判定手段４に入力する。
【００１３】
系列長入力手段２は、ユーザにより入力された系列長を読み込み、変数値系列集合生成手段３において処理可能な形式に変換する。そして、系列長入力手段２は、変換した系列長を変数値系列集合生成手段３に入力する。なお、ユーザは、任意の系列長を設定して入力することができる。
【００１４】
変数値系列集合生成手段３は、ＬＴＬ式に含まれる変数が所定の系列長でとりうる値の組み合わせを生成する。以下、当該変数が所定の系列長でとりうる値を変数値系列と称する。また、当該変数が所定の系列長でとりうる値の組み合わせを変数値系列集合と称する。
具体的には、変数値系列集合生成手段３は、まず、ＬＴＬ式に含まれる変数を抽出する。次に、変数値系列集合生成手段３は、系列長入力手段２から入力された系列長の時間において、抽出した変数がとりうる値（変数値系列）の組み合わせ（変数値系列集合）を全て生成する。そして、変数値系列集合生成手段３は、生成した変数値系列集合をＬＴＬ式判定手段４に入力する。
【００１５】
ＬＴＬ式判定手段４は、変数値系列集合生成手段３により生成された変数値系列集合のそれぞれの変数値系列がＬＴＬ式に代入された場合に、当該ＬＴＬ式が成立するか否かを判定する。
具体的には、ＬＴＬ式判定手段４は、ＬＴＬ式の各変数に、変数値系列の値を代入し、当該ＬＴＬ式が成立するか否かを判定する。次に、ＬＴＬ式判定手段４は、当該変数値系列と当該判定結果とを対応付けて結果表示手段５に入力する。
【００１６】
結果表示手段５は、変数値系列と判定結果とを対応付けて表示する。具体的には、結果表示手段５は、ＬＣＤ（liquid  Crystal  Display）等の表示部（図示省略）を備え、ＬＴＬ式判定手段４から入力された変数値系列と判定結果とを対応付けて、当該表示部に表示する。
【００１７】
次に、本発明の実施形態１にかかるＬＴＬ式確認システム１００におけるＬＴＬ式確認方法について、図２に示すフローチャートを参照しながら説明する。
まず、ＬＴＬ式入力手段１が、ユーザにより入力されたＬＴＬ式を読み込む（ステップＳ１）。そして、ＬＴＬ式入力手段１は、読み込んだＬＴＬ式を所定の形式に変換して、変数値系列集合生成手段３及びＬＴＬ式判定手段４に入力する。
【００１８】
次に、系列長入力手段２が、ユーザにより入力された系列長を読み込む（ステップＳ２）。そして、系列長入力手段２は、読み込んだ系列長を所定の形式に変換して、変数値系列集合生成手段３に入力する。
【００１９】
次に、変数値系列集合生成手段３が、ＬＴＬ式に含まれる変数を抽出する（ステップＳ３）。次いで、変数値系列集合生成手段３が、系列長入力手段２により入力された系列長の時間において、当該変数がとりうる値である変数値系列の組み合わせ（変数値系列集合）を全て生成する（ステップＳ４）。そして、変数値系列集合生成手段３は、生成した変数値系列集合をＬＴＬ式判定手段４に入力する。
【００２０】
次に、ＬＴＬ式判定手段４は、変数値系列集合生成手段３から入力された変数値系列集合の中から一つの変数値系列を選択する（ステップＳ５）。
次いで、ＬＴＬ式判定手段４は、ステップＳ５において選択した変数値系列をＬＴＬ式に代入し、当該ＬＴＬ式が成立するか否かを判定する（ステップＳ６）。
【００２１】
次に、ＬＴＬ式判定手段４は、変数値系列集合に含まれる全ての変数値系列について判定処理を行ったか否かについて判断する（ステップＳ７）。
【００２２】
ステップＳ７において、ＬＴＬ式判定手段４が、変数値系列集合に含まれる全ての変数値系列について判定処理を行っていないと判断した場合には（ステップＳ７；Ｎｏ）、ステップＳ５に戻る。
【００２３】
ステップＳ７において、ＬＴＬ式判定手段４が、変数値系列集合に含まれる全ての変数値系列について判定処理を行ったと判断した場合には（ステップＳ７；Ｙｅｓ）、ＬＴＬ式判定手段４は、変数値系列と判定結果とを対応付けて結果表示手段５に入力する。次いで、結果表示手段５は、ＬＴＬ式判定手段４から入力された変数値系列と判定結果とを対応付けて表示する（ステップＳ８）。
【００２４】
実施例１．
次に、本発明の実施形態１の具体的な実施例１について説明する。
実施例１では、ユーザにより、ＬＴＬ式として「□（Ｑ→□（！Ｐ））」が入力され、系列長として「４」が入力された場合を例示して説明する。また、変数Ｐ及びＱは「Ｔ」又は「Ｆ」の何れかの値をとるとする。
【００２５】
ステップＳ３では、ＬＴＬ式「□（Ｑ→□（！Ｐ））」から二つの変数Ｐ及びＱを抽出する。
次に、ステップＳ４では、二つの変数Ｐ及びＱが４単位時間でとりうる変数値系列の組み合わせを全て生成する。生成される変数値系列の組み合わせ（変数値系列集合）を図３に示す。図３に示すように、２５６個の変数値系列が生成される。
【００２６】
次に、ステップＳ５乃至ステップＳ７において、各変数値系列を代入した場合にＬＴＬ式が成立するか否かを判定する。具体的には、ＬＴＬ式判定手段４が、変数値系列から状態遷移を作成し、モデル検査により作成した状態遷移がＬＴＬ式を満たすか否かを判定する。図４を用いて、変数値系列から状態遷移を作成する方法の一例を説明する。図４に示すように、系列位置「１」の時間において変数Ｐの値が「Ｆ」、変数Ｑの値が「Ｔ」、系列位置「２」の時間において変数Ｐの値が「Ｔ」、変数Ｑの値が「Ｆ」、系列位置「３」の時間において変数Ｐの値が「Ｔ」、変数Ｑの値が「Ｔ」、系列位置「４」の時間において変数Ｐの値が「Ｆ」、変数Ｑの値が「Ｆ」である変数値系列を例に挙げて説明する。この場合、系列位置「１」の時間における変数値Ｐ及びＱの値を状態１とし、系列位置「２」の時間における変数値Ｐ及びＱの値を状態２とし、系列位置「３」の時間における変数値Ｐ及びＱの値を状態３とし、系列位置「４」の時間における変数値Ｐ及びＱの値を状態４とし、状態ｎ（ｎは正の整数）と状態ｎ＋１との間に遷移を定義する。即ち、状態１においてＰ＝Ｆ、Ｑ＝Ｔとし、状態２においてＰ＝Ｔ、Ｑ＝Ｆとし、状態３においてＰ＝Ｔ、Ｑ＝Ｔとし、状態４においてＰ＝Ｆ、Ｑ＝Ｆとし、状態１と状態２との間に遷移を定義し、状態２と状態３との間に遷移を定義し、状態３と状態４との間に遷移を定義する。
そして、ステップＳ８において、変数値系列と判定結果とを対応付けて表示する。
【００２７】
以上に説明した本発明の実施形態１にかかるＬＴＬ式確認システム１００、ＬＴＬ式確認方法、及び、ＬＴＬ式確認プログラムによれば、変数値系列集合生成手段３により、ＬＴＬ式に含まれる変数が所定の系列長でとりうる値である変数値系列の組み合わせが生成される。また、ＬＴＬ式判定手段４により、変数値系列集合生成手段３により生成されたそれぞれの変数値系列がＬＴＬ式に代入された場合に、当該ＬＴＬ式が成立するか否かが判定される。
これにより、ユーザは、それぞれの変数値系列においてＬＴＬ式が成立するか否かを確認することができる。従って、ユーザがＬＴＬ式に不慣れな場合でも、ＬＴＬ式を容易に確認することができる。
【００２８】
また、結果表示手段５により、変数値系列と判定結果とを対応付けて表示される。換言すれば、ＬＴＬ式の意味が具体的な値に近い形式で表示される。そのため、ＬＴＬ式がユーザの所望する検証項目を反映しているか否かを確認することができる。
【００２９】
実施形態２．
本発明の実施形態２にかかるＬＴＬ式確認システム２００について、図５を参照しながら説明する。実施形態２にかかるＬＴＬ式確認システム２００では、ＬＴＬ式判定手段４０、変数値系列集合マージ手段６、結果表示手段５０の構成のみが、実施形態１にかかるＬＴＬ式確認システム１００と異なるので、同一の構成については、同一の符号を付すとともにその説明を省略する。
【００３０】
ＬＴＬ式判定手段４０は、実施形態１にかかるＬＴＬ式判定手段４と同様の処理を行って、変数値系列集合のそれぞれの変数値系列がＬＴＬ式に代入された場合に、当該ＬＴＬ式が成立するか否かを判定する。
また、ＬＴＬ式判定手段４０は、変数値系列と判定結果とを対応付けて変数値系列集合マージ手段６に入力する。この点が、ＬＴＬ式判定手段４０は、実施形態１にかかるＬＴＬ式判定手段４と異なる。
【００３１】
変数値系列集合マージ手段６は、ＬＴＬ式判定手段４０による判定結果が同じであり、且つ、値の違いが１箇所である変数値系列同士をマージする。また、変数値系列集合マージ手段６は、マージ処理後の変数値系列と判定結果とを対応付けて結果表示手段５０に入力する。ここで、「値の違いが１箇所である変数値系列同士」とは、「系列長の時間の中の１単位時間における１つの変数の値のみが異なる変数値系列同士」という意味である。
【００３２】
結果表示手段５０は、マージ処理後の変数値系列と判定結果とを対応付けて表示する。具体的には、結果表示手段５０は、ＬＣＤ等の表示部（図示省略）を備え、マージ処理後の変数値系列と判定結果とを対応付けて、当該表示部に表示する。
【００３３】
次に、本発明の実施形態２にかかるＬＴＬ式確認システム２００におけるＬＴＬ式確認方法について、図６に示すフローチャートを参照しながら説明する。なお、ステップＳ１０１乃至ステップＳ１０７の処理は、図２におけるステップＳ１乃至ステップＳ７の処理と同様であるため、その説明を省略する。
【００３４】
ステップＳ１０７において、ＬＴＬ式判定手段４０が、変数値系列集合に含まれる全ての変数値系列について判定処理を行ったと判断した場合には（ステップＳ７；Ｙｅｓ）、ＬＴＬ式判定手段４０は、変数値系列と判定結果とを対応付けて変数値系列集合マージ手段６に入力する。次いで、変数値系列集合マージ手段６は、マージ可能な変数値系列があるか否かを判断する（ステップＳ１０８）。具体的には、変数値系列集合マージ手段６は、ＬＴＬ式判定手段４０による判定結果が同じであり、且つ、値の違いが１箇所である変数値系列があるか否かを判断する。
【００３５】
ステップＳ１０８において、マージ可能な変数値系列がある場合には（ステップＳ１０８；Ｙｅｓ）、変数値系列集合マージ手段６は、当該変数値系列同士に対してマージ処理を行って（ステップＳ１０９）、ステップＳ１０８に戻る。
ステップＳ１０８において、マージ可能な変数値系列がない場合には（ステップＳ１０８；Ｎｏ）、変数値系列集合マージ手段６は、マージ後の変数値系列と判定結果とを対応付けて結果表示手段５０に入力する。次いで、結果表示手段５０は、マージ後の変数値系列と判定結果とを対応付けて表示する（ステップＳ１１０）。
【００３６】
実施例２．
次に、本発明の実施形態２の具体的な実施例２について説明する。また、実施例２では、実施例１と同様に、ユーザにより、ＬＴＬ式として「□（Ｑ→□（！Ｐ））」が入力され、系列長として「４」が入力された場合を例示して説明する。また、変数Ｐ及びＱは「Ｔ」又は「Ｆ」の何れかの値をとるとする。
また、上述の通り、図６のステップＳ１０１乃至ステップＳ１０７の処理は、図２におけるステップＳ１乃至ステップＳ７の処理と同様である。そのため、ステップＳ１０８乃至ステップＳ１１０の処理について説明する。
【００３７】
ステップＳ１０８、ステップＳ１０９では、変数値系列集合マージ手段６が、判定結果が同じであり、且つ、値の違いが１箇所である変数値系列同士をマージする。
図７を用いてマージ処理を説明する。図７には、二つの変数値系列が示されている。一の変数値系列では、系列位置「１」乃至「４」の時間において、変数Ｐ及びＱの値が全て「Ｆ」であり、判定結果が「Ｆ」である。また、他の変数値系列では、系列位置「１」の時間における変数Ｐの値のみが「Ｔ」であり、他の値が全て「Ｆ」であり、判定結果が「Ｆ」である。
【００３８】
従って、図７に示す二つの変数値系列では、系列位置「１」の時間における変数Ｐの値のみが異なり、判定結果が同じである。その場合、変数値系列集合マージ手段６は、当該二つの変数値系列をマージして一つの変数値系列（マージ後の変数値系列）を生成する。
マージ後の変数値系列において、当該二つの変数値系列において異なる値であった箇所は、マージされたことを表現する特殊な記号で表現する。例えば、図７では、マージ後の変数値系列において、系列位置「１」の時間における変数Ｐの値は「＊」で表現される。
【００３９】
同様にして、変数値系列集合マージ手段６は、マージ可能な変数値系列がなくなるまで、ステップＳ１０８、ステップＳ１０９の処理を繰り返す。そして、マージ可能な変数値系列がなくなった場合、変数値系列集合マージ手段６は、マージ後の変数値系列と判定結果とを対応付けて結果表示手段５０に入力する。
【００４０】
次に、ステップＳ１１０では、結果表示手段５０が、マージ後の変数値系列と判定結果とを対応付けて表示する。図８に、結果表示手段５０による表示の一例を示す。図８に示すように、２５６個あった変数値系列は、マージ処理により１５個の変数値系列にマージされた。
【００４１】
以上に説明した本発明の実施形態２にかかるＬＴＬ式確認システム２００、ＬＴＬ式確認方法、及び、ＬＴＬ式確認プログラムによれば、実施形態１と同様の効果が得られることは勿論である。特に、実施形態２では、変数値系列集合マージ手段６により、判定結果が同じであり、且つ、値の違いが１箇所である変数値系列同士がマージされる。そのため、結果表示手段５０において表示する変数値系列の数が少なくなる。よって、結果表示手段５０における表示をより簡潔にすることができる。
【００４２】
なお、本発明は、ＬＴＬ式に限らず、その他の時相論理式にも適用することが可能である。
【図面の簡単な説明】
【００４３】
【図１】本発明の実施形態１にかかるＬＴＬ式確認システムの一例を示す図である。
【図２】本発明の実施形態１にかかるＬＴＬ式確認システムにおけるＬＴＬ式確認方法の一例を説明するフローチャートである。
【図３】実施例１にかかる変数値系列集合の一例を示す図である。
【図４】実施例１における変数値系列から状態遷移を作成する方法を説明する図である。
【図５】本発明の実施形態２にかかるＬＴＬ式確認システムの一例を示す図である。
【図６】本発明の実施形態２にかかるＬＴＬ式確認システムにおけるＬＴＬ式確認方法の一例を説明するフローチャートである。
【図７】実施例２におけるマージ処理を説明する図である。
【図８】実施例２における結果表示手段による表示の一例を示す図である。
【符号の説明】
【００４４】
３  変数値系列集合生成手段
４、４０  ＬＴＬ式判定手段
１００、２００  ＬＴＬ式確認システム
【図１】
2009187416.tif 000003
【図２】
2009187416.tif 000004
【図３】
2009187416.tif 000005
【図４】
2009187416.tif 000006
【図５】
2009187416.tif 000007
【図６】
2009187416.tif 000008
【図７】
2009187416.tif 000009
【図８】
2009187416.tif 000010