(57)【要約】【課題】プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の検証を簡便ならしめることができる回路記述の抽象化装置及び検証装置、回路記述の抽象化プログラム及び検証プログラム、並びに回路記述の抽象化方法及び検証方法を提供する。【解決手段】回路記述の仕様データ２４が示す論理モデル内に含まれる複数の状態及び各状態間の状態遷移により規定される複数のパスに対して、該パスが検証対象とされるか否かを判別する際の判別条件を入力装置１２からの入力操作に基づき制御装置１１が設定する。そして、複数のパスについて、判別条件に基づきパス毎における状態遷移を検査することにより、検証プログラム２２による検証対象から除外される非検証用パスと検証対象とされる検証用パスとを判別し、その判別結果に基づき、複数のパスを非検証用パスと検証用パスとが識別可能な状態で保存する。【選択図】図１
2010079432.tif 000002
【特許請求の範囲】
【請求項１】
プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の仕様データを記憶可能な記憶手段と、前記仕様データで表される論理モデルの抽象化の処理手順を制御する制御手段とを備えた回路記述の抽象化装置であって、
前記制御手段は、
前記論理モデル内に含まれる複数の状態及び各状態間の状態遷移により規定される複数のパスに対して該パスが検証対象とされるか否かを判別する際の判別条件を設定する判別条件設定手段と、
前記複数のパスについて、前記判別条件の設定態様に基づきパス毎における状態遷移の諾否を検査することにより、検証対象から除外される非検証用パスと検証対象とされる検証用パスとを判別するパス判別手段と、
該判別手段の判別結果に基づき、前記回路記述が検証される際には前記複数のパスのうち前記非検証用パスは検証が回避されると共に前記検証用パスは検証が行われるように、前記複数のパスを前記非検証用パスと前記検証用パスとを識別可能な状態にて保存するパス保存手段と
を備えたことを特徴とする回路記述の抽象化装置。
【請求項２】
前記判別条件は、前記パスを構成する複数の状態のうち該状態を経由する状態遷移を禁止する禁止フラグを含んで構成されており、
前記パス判別手段は、前記パス毎の状態遷移の検査段階において前記判別条件として前記禁止フラグが設定された状態を含むパスを検査した場合に、該パスを前記非検証用パスと判別することを特徴とする請求項１に記載の回路記述の抽象化装置。
【請求項３】
前記判別条件は、前記パスを構成する複数の状態のうち状態遷移での始点となる状態から終点となる状態に至るまでの途中で通過すべき状態であることを示す通過フラグを含んで構成されており、
前記パス判別手段は、前記パス毎の状態遷移の検査段階において前記判別条件として前記通過フラグが設定された状態を経由して前記終点となる状態に至ったパスを検査した場合に、該パスを前記検証用パスと判別することを特徴とする請求項１又は請求項２に記載の回路記述の抽象化装置。
【請求項４】
前記パス判別手段によるパス毎の状態遷移の検査が開始されてからの経過時間が予め設定された閾値時間を越えたか否かを判定する時間判定手段を更に備え、
前記パス判別手段は、前記時間判定手段が前記経過時間は前記閾値時間を超えたと判定した時点で、前記パス毎の状態遷移の検査を終了することを特徴とする請求項１〜請求項３のうち何れか一項に記載の回路記述の抽象化装置。
【請求項５】
前記パス判別手段は、その時点で検査している状態からの更なる遷移先の状態を各状態の検査段階毎に順次抽出し、該抽出された遷移先の各状態からの更なる状態遷移を並行的に検査することを特徴とする請求項１〜請求項４のうち何れか一項に記載の回路記述の抽象化装置。
【請求項６】
プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の仕様データを記憶可能な記憶手段と、前記仕様データで表される論理モデルの検証の処理手順を制御する制御手段とを備えた回路記述の検証装置であって、
前記制御手段は、
前記論理モデル内に含まれる複数の状態及び各状態間の状態遷移により規定される複数のパスに対して該パスが検証対象とされるか否かを判別する際の判別条件を設定する判別条件設定手段と、
前記複数のパスについて、前記判別条件の設定態様に基づきパス毎における状態遷移の諾否を検査することにより、検証対象から除外される非検証用パスと検証対象とされる検証用パスとを判別するパス判別手段と、
該判別手段の判別結果に基づき、前記回路記述が検証される際には前記複数のパスのうち前記非検証用パスは検証が回避されると共に前記検証用パスは検証が行われるように、前記複数のパスを前記非検証用パスと前記検証用パスとを識別可能な状態にて保存するパス保存手段と
該パス保存手段により検証用パスとして識別可能に保存されたパスを検証対象にした検証作業を実行する検証手段と
を備えたことを特徴とする回路記述の検証装置。
【請求項７】
前記判別条件は、前記パスを構成する複数の状態のうち該状態を経由する状態遷移を禁止する禁止フラグを含んで構成されており、
前記パス判別手段は、前記パス毎の状態遷移の検査段階において前記判別条件として前記禁止フラグが設定された状態を含むパスを検査した場合に、該パスを前記非検証用パスと判別することを特徴とする請求項６に記載の回路記述の検証装置。
【請求項８】
前記判別条件は、前記パスを構成する複数の状態のうち状態遷移での始点となる状態から終点となる状態に至るまでの途中で通過すべき状態であることを示す通過フラグを含んで構成されており、
前記パス判別手段は、前記パス毎の状態遷移の検査段階において前記判別条件として前記通過フラグが設定された状態を経由して前記終点となる状態に至ったパスを検査した場合に、該パスを前記検証用パスと判別することを特徴とする請求項６又は請求項７に記載の回路記述の検証装置。
【請求項９】
前記パス判別手段によるパス毎の状態遷移の検査が開始されてからの経過時間が予め設定された閾値時間を越えたか否かを判定する時間判定手段を更に備え、
前記パス判別手段は、前記時間判定手段が前記経過時間は前記閾値時間を超えたと判定した時点で、前記パス毎の状態遷移の検査を終了することを特徴とする請求項６〜請求項８のうち何れか一項に記載の回路記述の検証装置。
【請求項１０】
前記パス判別手段は、その時点で検査している状態からの更なる遷移先の状態を各状態の検査段階毎に順次抽出し、該抽出された遷移先の各状態からの更なる状態遷移を並行的に検査することを特徴とする請求項６〜請求項９のうち何れか一項に記載の回路記述の検証装置。
【請求項１１】
プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の仕様データを記憶可能な記憶手段と、前記仕様データで表される論理モデルの抽象化の処理手順を制御する制御手段とを備えた回路記述の抽象化装置を稼動させるために用いられる回路記述の抽象化プログラムであって、
前記制御手段を、
前記論理モデル内に含まれる複数の状態及び各状態間の状態遷移により規定される複数のパスに対して該パスが検証対象とされるか否かを判別する際の判別条件を設定する判別条件設定手段、
前記複数のパスについて、前記判別条件の設定態様に基づきパス毎における状態遷移の諾否を検査することにより、検証対象から除外される非検証用パスと検証対象とされる検証用パスとを判別するパス判別手段、及び、
該判別手段の判別結果に基づき、前記回路記述が検証される際には前記複数のパスのうち前記非検証用パスは検証が回避されると共に前記検証用パスは検証が行われるように、前記複数のパスを前記非検証用パスと前記検証用パスとを識別可能な状態にて保存するパス保存手段
として機能させることを特徴とする回路記述の抽象化プログラム。
【請求項１２】
前記判別条件は、前記パスを構成する複数の状態のうち該状態を経由する状態遷移を禁止する禁止フラグを含んで構成されており、
前記パス判別手段が前記パス毎の状態遷移の検査段階において前記判別条件として前記禁止フラグが設定された状態を含むパスを検査する場合には、該パスを前記パス判別手段に前記非検証用パスと判別させることを特徴とする請求項１１に記載の回路記述の抽象化プログラム。
【請求項１３】
前記判別条件は、前記パスを構成する複数の状態のうち状態遷移の始点となる状態から終点となる状態に至るまでの途中で通過すべき状態であることを示す通過フラグを含んで構成されており、
前記パス判別手段が前記パス毎の状態遷移の検査段階において前記判別条件として前記通過フラグが設定された状態を経由して前記終点となる状態に至ったパスを検査した場合には、該パスを前記パス判別手段に前記検証用パスと判別させることを特徴とする請求項１１又は請求項１２に記載の回路記述の抽象化プログラム。
【請求項１４】
前記制御手段を、
前記パス判別手段によるパス毎の状態遷移の検査が開始されてからの経過時間が予め設定された閾値時間を越えたか否かを判定する時間判定手段として更に機能させ、
前記時間判定手段が前記経過時間は前記閾値時間を超えたと判定した時点で、前記パス判別手段に前記パス毎の状態遷移の検査を終了させることを特徴とする請求項１１〜請求項１３のうち何れか一項に記載の回路記述の抽象化プログラム。
【請求項１５】
前記パス判別手段に、その時点で検査している状態からの更なる遷移先の状態を各状態の検査段階毎に順次抽出させ、抽出した遷移先の各状態からの更なる状態遷移を並行的に検査させることを特徴とする請求項１１〜請求項１４のうち何れか一項に記載の回路記述の抽象化プログラム。
【請求項１６】
プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の仕様データを記憶可能な記憶手段と、前記仕様データで表される論理モデルの検証の処理手順を制御する制御手段とを備えた回路記述の検証装置を稼動させるために用いられる回路記述の検証プログラムであって、
前記制御手段を、
前記論理モデル内に含まれる複数の状態及び各状態間の状態遷移により規定される複数のパスに対して該パスが検証対象とされるか否かを判別する際の判別条件を設定する判別条件設定手段、
前記複数のパスについて、前記判別条件の設定態様に基づきパス毎における状態遷移の諾否を検査することにより、検証対象から除外される非検証用パスと検証対象とされる検証用パスとを判別するパス判別手段、
該判別手段の判別結果に基づき、前記回路記述が検証される際には前記複数のパスのうち前記非検証用パスは検証が回避されると共に前記検証用パスは検証が行われるように、前記複数のパスを前記非検証用パスと前記検証用パスとを識別可能な状態にて保存するパス保存手段、及び、
該パス保存手段により検証用パスとして識別可能に保存されたパスを検証対象にした検証作業を実行する検証手段
として機能させることを特徴とする回路記述の検証プログラム。
【請求項１７】
前記判別条件は、前記パスを構成する複数の状態のうち該状態を経由する状態遷移を禁止する禁止フラグを含んで構成されており、
前記パス判別手段が前記パス毎の状態遷移の検査段階において前記判別条件として前記禁止フラグが設定された状態を含むパスを検査する場合には、該パスを前記パス判別手段に前記非検証用パスと判別させることを特徴とする請求項１６に記載の回路記述の検証プログラム。
【請求項１８】
前記判別条件は、前記パスを構成する複数の状態のうち状態遷移の始点となる状態から終点となる状態に至るまでの途中で通過すべき状態であることを示す通過フラグを含んで構成されており、
前記パス判別手段が前記パス毎の状態遷移の検査段階において前記判別条件として前記通過フラグが設定された状態を経由して前記終点となる状態に至ったパスを検査した場合には、該パスを前記パス判別手段に前記検証用パスと判別させることを特徴とする請求項１６又は請求項１７に記載の回路記述の検証プログラム。
【請求項１９】
前記制御手段を、
前記パス判別手段によるパス毎の状態遷移の検査が開始されてからの経過時間が予め設定された閾値時間を越えたか否かを判定する時間判定手段として更に機能させ、
前記時間判定手段が前記経過時間は前記閾値時間を超えたと判定した時点で、前記パス判別手段に前記パス毎の状態遷移の検査を終了させることを特徴とする請求項１６〜請求項１８のうち何れか一項に記載の回路記述の検証プログラム。
【請求項２０】
前記パス判別手段に、その時点で検査している状態からの更なる遷移先の状態を各状態の検査段階毎に順次抽出させ、抽出した遷移先の各状態からの更なる状態遷移を並行的に検査させることを特徴とする請求項１６〜請求項１９のうち何れか一項に記載の回路記述の検証プログラム。
【請求項２１】
プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の抽象化方法であって、
前記回路記述が示す論理モデル内に含まれる複数の状態及び各状態間の状態遷移により規定される複数のパスに対して該パスが検証対象とされるか否かを判別する際の判別条件を設定する判別条件設定段階と、
前記複数のパスについて、前記判別条件の設定態様に基づきパス毎における状態遷移の諾否を検査することにより、検証対象から除外される非検証用パスと検証対象とされる検証用パスとを判別するパス判別段階と、
該パス判別段階での判別結果に基づき、前記回路記述が検証される際には前記複数のパスのうち前記非検証用パスは検証が回避されると共に前記検証用パスは検証が行われるように、前記複数のパスを前記非検証用パスと前記検証用パスとを識別可能な状態にて保存するパス保存段階と
を備えたことを特徴とする回路記述の抽象化方法。
【請求項２２】
前記判別条件は、前記パスを構成する複数の状態のうち該状態を経由する状態遷移を禁止する禁止フラグを含んで構成されており、
前記パス判別段階では、前記パス毎の状態遷移の検査段階において前記判別条件として前記禁止フラグが設定された状態を含むパスを検査した場合に、該パスを前記非検証用パスと判別することを特徴とする請求項２１に記載の回路記述の抽象化方法。
【請求項２３】
前記判別条件は、前記パスを構成する複数の状態のうち始点となる状態から終点となる状態に至るまでの状態遷移の途中で通過すべき状態であることを示す通過フラグを含んで構成されており、前記パス判別段階では、前記パス毎の状態遷移の検査段階において前記判別条件として前記通過フラグが設定された状態を経由して前記終点となる状態に至ったパスを検査した場合に、該パスを前記検証用パスと判別することを特徴とする請求項２１又は請求項２２に記載の回路記述の抽象化方法。
【請求項２４】
前記パス判別段階にてパス毎の状態遷移の検査が開始されてからの経過時間が予め設定された閾値時間を越えたか否かを判定する時間判定段階を更に備え、
前記パス判別段階では、前記時間判定段階にて前記経過時間は前記閾値時間を超えたと判定した時点で、前記パス毎の状態遷移の検査を終了することを特徴とする請求項２１〜請求項２３のうち何れか一項に記載の回路記述の抽象化方法。
【請求項２５】
前記パス判別段階では、その時点で検査している状態からの更なる遷移先の状態を各状態の検査段階毎に順次抽出し、該抽出された遷移先の各状態からの更なる状態遷移を並行的に検査することを特徴とする請求項２１〜請求項２４のうち何れか一項に記載の回路記述の抽象化方法。
【請求項２６】
プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の検証方法であって、
前記回路記述が示す論理モデル内に含まれる複数の状態及び各状態間の状態遷移により規定される複数のパスに対して該パスが検証対象とされるか否かを判別する際の判別条件を設定する判別条件設定段階と、
前記複数のパスについて、前記判別条件の設定態様に基づきパス毎における状態遷移の諾否を検査することにより、検証対象から除外される非検証用パスと検証対象とされる検証用パスとを判別するパス判別段階と、
該パス判別段階での判別結果に基づき、前記回路記述が検証される際には前記複数のパスのうち前記非検証用パスは検証が回避されると共に前記検証用パスは検証が行われるように、前記複数のパスを前記非検証用パスと前記検証用パスとを識別可能な状態にて保存するパス保存段階と、
該パス保存段階において検証用パスとして識別可能に保存されたパスを検証対象にした検証作業を実行する検証段階と
を備えたことを特徴とする回路記述の検証方法。
【請求項２７】
前記判別条件は、前記パスを構成する複数の状態のうち該状態を経由する状態遷移を禁止する禁止フラグを含んで構成されており、
前記パス判別段階では、前記パス毎の状態遷移の検査段階において前記判別条件として前記禁止フラグが設定された状態を含むパスを検査した場合に、該パスを前記非検証用パスと判別することを特徴とする請求項２６に記載の回路記述の検証方法。
【請求項２８】
前記判別条件は、前記パスを構成する複数の状態のうち始点となる状態から終点となる状態に至るまでの状態遷移の途中で通過すべき状態であることを示す通過フラグを含んで構成されており、前記パス判別段階では、前記パス毎の状態遷移の検査段階において前記判別条件として前記通過フラグが設定された状態を経由して前記終点となる状態に至ったパスを検査した場合に、該パスを前記検証用パスと判別することを特徴とする請求項２６又は請求項２７に記載の回路記述の検証方法。
【請求項２９】
前記パス判別段階にてパス毎の状態遷移の検査が開始されてからの経過時間が予め設定された閾値時間を越えたか否かを判定する時間判定段階を更に備え、
前記パス判別段階では、前記時間判定段階にて前記経過時間は前記閾値時間を超えたと判定した時点で、前記パス毎の状態遷移の検査を終了することを特徴とする請求項２６〜請求項２８のうち何れか一項に記載の回路記述の検証方法。
【請求項３０】
前記パス判別段階では、その時点で検査している状態からの更なる遷移先の状態を各状態の検査段階毎に順次抽出し、該抽出された遷移先の各状態からの更なる状態遷移を並行的に検査することを特徴とする請求項２６〜請求項２９のうち何れか一項に記載の回路記述の検証方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、コンピュータプログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の抽象化装置及び検証装置、回路記述の抽象化プログラム及び検証プログラム、並びに回路記述の抽象化方法及び検証方法に関する。
【背景技術】
【０００２】
従来、設計したコンピュータプログラムが設計者の意図した設計思想どおりのふるまいをするか否かを検証するための技術として、形式的手法を用いた検証装置が広く知られている（例えば、特許文献１）。この検証装置では、例えばＣ、Ｃ＋＋、ＦＯＲＴＲＡＮ等のプログラム言語を用いて記述されたプログラムの記述内容を先ず既存のモデリング変換ソフト（Ｓｉｍｕｌｉｎｋ、Ｓｃａｄｅ等）を用いて形式的仕様記述言語による回路記述に変換するようにしている。そして、同回路記述で示される論理モデル内の全状態及び全遷移について検証ソフトを使用して数学的に検証を行うことで、形式的仕様の回路記述に変換されたプログラム内容の設計の正しさを証明することが可能となっている。
【特許文献１】特許第３６６００９７号公報
【発明の開示】
【発明が解決しようとする課題】
【０００３】
ところで、近年、コンピュータ処理の高度化・複雑化の要請に伴い、コンピュータプログラムは記述内容の規模が拡大化の傾向にあり、そのプログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述から導出されるモデル内の全状態及び全遷移の数も指数的に増大している。そこで、従来の検証装置では、回路記述の一部を削除して検証対象となる回路の規模を縮小させることにより、回路記述の検証に要する処理負荷を低減するようにしていた。
【０００４】
しかしながら、従来の検証装置では、検証者が、回路記述内から削除しようとする領域を任意に選択すると共に、その任意に選択した領域を回路記述内から削除した検証用モデルを手作業で作成し、かかる検証用モデルについて形式的手法に基づき検証する構成であったため、その検証作業には多大な労力と時間を要していた。また、新たに検証作業をやり直す際には、一旦削除した領域を復元させた上で、新たな検証用モデルを作成することになるため、その手間が煩わしかった。
【０００５】
本発明は、このような事情に鑑みてなされたものであり、その目的は、プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の検証を簡便ならしめることができる回路記述の抽象化装置及び検証装置、回路記述の抽象化プログラム及び検証プログラム、並びに回路記述の抽象化方法及び検証方法を提供することにある。
【課題を解決するための手段】
【０００６】
上記目的を達成するために、請求項１に記載の回路記述の抽象化装置は、プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述仕様データを記憶可能な記憶手段と、前記回路記述仕様データで表される論理モデルの抽象化の処理手順を制御する制御手段とを備えた回路記述の抽象化装置であって、前記制御手段は、前記論理モデル内に含まれる複数の状態及び各状態間の状態遷移により規定される複数のパスに対して該パスが検証対象とされるか否かを判別する際の判別条件を設定する判別条件設定手段と、前記複数のパスについて、前記判別条件の設定態様に基づきパス毎における状態遷移を検査することにより、検証対象から除外される非検証用パスと検証対象とされる検証用パスとを判別するパス判別手段と、該判別手段の判別結果に基づき、前記回路記述が検証される際には前記複数のパスのうち前記非検証用パスは検証が回避されると共に前記検証用パスは検証が行われるように、前記複数のパスを前記非検証用パスと前記検証用パスとを識別可能な状態にて保存するパス保存手段とを備えたことを要旨とする。
【０００７】
上記構成によれば、検証装置を用いて回路記述を検証する際、パス保存手段により検証用パスとして識別可能な状態に保存されているパスについては検証対象とする一方で、非検証用パスとして識別可能な状態に保存されているパスについては検証対象から除外した検証作業を実行することが可能であるため、検証作業が迅速且つ簡単になる。また、検証対象から除外するパスについても回路記述内から削除することなく、非検証用パスとして識別可能な状態で検証対象とされる検証用パスと共に元の回路記述内に保存されているので、新たに検証作業をやり直すために判別条件の設定を変更する際にも、一旦削除したパスを復元させるような作業が不要となり、迅速且つ容易に再検証を行うことができる。したがって、プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の検証を簡便ならしめることができる。
【０００８】
請求項２に記載の回路記述の抽象化装置は、請求項１に記載の回路記述の抽象化装置において、前記判別条件は、前記パスを構成する複数の状態のうち該状態を経由する状態遷移を禁止する禁止フラグを含んで構成されており、前記パス判別手段は、前記パス毎の状態遷移の検査段階において前記判別条件として前記禁止フラグが設定された状態を含むパスを検査した場合に、該パスを前記非検証用パスと判別することを要旨とする。
【０００９】
上記構成によれば、パス判別手段はパス毎の状態遷移の検査段階において禁止フラグが判別条件として設定された状態を経由する時点で、その状態を含むパスを検証対象から除外される非検証用パスとして判別できるので、回路記述の抽象化を容易に行うことができる。
【００１０】
請求項３に記載の回路記述の抽象化装置は、請求項１又は請求項２に記載の回路記述の抽象化装置において、前記判別条件は、前記パスを構成する複数の状態のうち始点となる状態から終点となる状態に至るまでの状態遷移の途中で通過すべき状態であることを示す通過フラグを含んで構成されており、前記パス判別手段は、前記パス毎の状態遷移の検査段階において前記判別条件として前記通過フラグが設定された状態を経由して前記終点となる状態に至ったパスを検査した場合に、該パスを前記検証用パスと判別することを要旨とする。
【００１１】
上記構成によれば、始点となる状態から終点となる状態に至るパスが複数存在する場合でも、検証用パスとされるパスを絞り込んで保存できるので、この点でも回路記述の抽象化を容易に行うことができる。
【００１２】
請求項４に記載の回路記述の抽象化装置は、請求項１〜請求項３のうち何れか一項に記載の回路記述の抽象化装置において、前記パス判別手段によるパス毎の状態遷移の検査が開始されてからの経過時間が予め設定された閾値時間を越えたか否かを判定する時間判定手段を更に備え、前記パス判別手段は、前記時間判定手段が前記経過時間は前記閾値時間を超えたと判定した時点で、前記パス毎の状態遷移の検査を終了することを要旨とする。
【００１３】
上記構成によれば、状態遷移の検査段階で終点となる状態に至っても更なる遷移先となる状態が新たに抽出されて無限に継続するような検査を適正に終了させることができ、この点でも回路記述の抽象化を容易に行うことができる。
【００１４】
請求項５に記載の回路記述の抽象化装置は、請求項１〜請求項４のうち何れか一項に記載の回路記述の抽象化装置において、前記パス判別手段は、その時点で検査している状態からの更なる遷移先の状態を各状態の検査段階毎に順次抽出し、該抽出された遷移先の各状態からの更なる状態遷移を並行的に検査することを要旨とする。
【００１５】
上記構成によれば、複数のパスにおける状態遷移を並行して網羅的に検査できるので、この点でも回路記述の抽象化を容易に行うことができる。
請求項６に記載の回路記述の検証装置は、プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の仕様データを記憶可能な記憶手段と、前記仕様データで表される論理モデルの検証の処理手順を制御する制御手段とを備えた回路記述の検証装置であって、前記制御手段は、前記論理モデル内に含まれる複数の状態及び各状態間の状態遷移により規定される複数のパスに対して該パスが検証対象とされるか否かを判別する際の判別条件を設定する判別条件設定手段と、前記複数のパスについて、前記判別条件の設定態様に基づきパス毎における状態遷移の諾否を検査することにより、検証対象から除外される非検証用パスと検証対象とされる検証用パスとを判別するパス判別手段と、該判別手段の判別結果に基づき、前記回路記述が検証される際には前記複数のパスのうち前記非検証用パスは検証が回避されると共に前記検証用パスは検証が行われるように、前記複数のパスを前記非検証用パスと前記検証用パスとを識別可能な状態にて保存するパス保存手段と該パス保存手段により検証用パスとして識別可能に保存されたパスを検証対象にした検証作業を実行する検証手段とを備えたことを要旨とする。
【００１６】
上記構成によれば、回路記述が示すモデルの規模を縮小することで、同モデルの検証に要する処理負荷を低減することができる。
請求項７に記載の回路記述の検証装置は、請求項６に記載の回路記述の検証装置において、前記判別条件は、前記パスを構成する複数の状態のうち該状態を経由する状態遷移を禁止する禁止フラグを含んで構成されており、前記パス判別手段は、前記パス毎の状態遷移の検査段階において前記判別条件として前記禁止フラグが設定された状態を含むパスを検査した場合に、該パスを前記非検証用パスと判別することを要旨とする。上記構成によれば、請求項２に記載の発明と同様の効果が得られる。
【００１７】
請求項８に記載の回路記述の検証装置は、請求項６又は請求項７に記載の回路記述の検証装置において、前記判別条件は、前記パスを構成する複数の状態のうち状態遷移での始点となる状態から終点となる状態に至るまでの途中で通過すべき状態であることを示す通過フラグを含んで構成されており、前記パス判別手段は、前記パス毎の状態遷移の検査段階において前記判別条件として前記通過フラグが設定された状態を経由して前記終点となる状態に至ったパスを検査した場合に、該パスを前記検証用パスと判別することを要旨とする。上記構成によれば、請求項３に記載の発明と同様の効果が得られる。
【００１８】
請求項９に記載の回路記述の検証装置は、請求項６〜請求項８のうち何れか一項に記載の回路記述の検証装置において、前記パス判別手段によるパス毎の状態遷移の検査が開始されてからの経過時間が予め設定された閾値時間を越えたか否かを判定する時間判定手段を更に備え、前記パス判別手段は、前記時間判定手段が前記経過時間は前記閾値時間を超えたと判定した時点で、前記パス毎の状態遷移の検査を終了することを要旨とする。上記構成によれば、請求項４に記載の発明と同様の効果が得られる。
【００１９】
請求項１０に記載の回路記述の検証装置は、請求項６〜請求項９のうち何れか一項に記載の回路記述の検証装置において、前記パス判別手段は、その時点で検査している状態からの更なる遷移先の状態を各状態の検査段階毎に順次抽出し、該抽出された遷移先の各状態からの更なる状態遷移を並行的に検査することを要旨とする。上記構成によれば、請求項５に記載の発明と同様の効果が得られる。
【００２０】
請求項１１に記載の回路記述の抽象化プログラムは、プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の仕様データを記憶可能な記憶手段と、前記仕様データで表される論理モデルの抽象化の処理手順を制御する制御手段とを備えた回路記述の抽象化装置を稼動させるために用いられる回路記述の抽象化プログラムであって、前記制御手段を、前記論理モデル内に含まれる複数の状態及び各状態間の状態遷移により規定される複数のパスに対して該パスが検証対象とされるか否かを判別する際の判別条件を設定する判別条件設定手段、前記複数のパスについて、前記判別条件の設定態様に基づきパス毎における状態遷移の諾否を検査することにより、検証対象から除外される非検証用パスと検証対象とされる検証用パスとを判別するパス判別手段、及び、該判別手段の判別結果に基づき、前記回路記述が検証される際には前記複数のパスのうち前記非検証用パスは検証が回避されると共に前記検証用パスは検証が行われるように、前記複数のパスを前記非検証用パスと前記検証用パスとを識別可能な状態にて保存するパス保存手段として機能させることを要旨とする。上記構成によれば、請求項１に記載の発明と同様の効果が得られる。
【００２１】
請求項１２に記載の回路記述の抽象化プログラムは、請求項１１に記載の回路記述の抽象化プログラムにおいて、前記判別条件は、前記パスを構成する複数の状態のうち該状態を経由する状態遷移を禁止する禁止フラグを含んで構成されており、前記パス判別手段が前記パス毎の状態遷移の検査段階において前記判別条件として前記禁止フラグが設定された状態を含むパスを検査する場合には、該パスを前記パス判別手段に前記非検証用パスと判別させることを要旨とする。上記構成によれば、請求項２に記載の発明と同様の効果が得られる。
【００２２】
請求項１３に記載の回路記述の抽象化プログラムは、請求項１１又は請求項１２に記載の回路記述の抽象化プログラムにおいて、前記判別条件は、前記パスを構成する複数の状態のうち状態遷移の始点となる状態から終点となる状態に至るまでの途中で通過すべき状態であることを示す通過フラグを含んで構成されており、前記パス判別手段が前記パス毎の状態遷移の検査段階において前記判別条件として前記通過フラグが設定された状態を経由して前記終点となる状態に至ったパスを検査した場合には、該パスを前記パス判別手段に前記検証用パスと判別させることを要旨とする。上記構成によれば、請求項３に記載の発明と同様の効果が得られる。
【００２３】
請求項１４に記載の回路記述の抽象化プログラムは、請求項１１〜請求項１３のうち何れか一項に記載の回路記述の抽象化プログラムにおいて、前記制御手段を、前記パス判別手段によるパス毎の状態遷移の検査が開始されてからの経過時間が予め設定された閾値時間を越えたか否かを判定する時間判定手段として更に機能させ、前記パス判別手段が前記時間判定手段が前記経過時間は前記閾値時間を超えたと判定した時点で、前記パス判別手段に前記パス毎の状態遷移の検査を終了させることを要旨とする。上記構成によれば、請求項４に記載の発明と同様の効果が得られる。
【００２４】
請求項１５に記載の回路記述の抽象化プログラムは、請求項１１〜請求項１４のうち何れか一項に記載の回路記述の抽象化プログラムにおいて、前記パス判別手段に、その時点で検査している状態からの更なる遷移先の状態を各状態の検査段階毎に順次抽出させ、抽出した遷移先の各状態からの更なる状態遷移を並行的に検査させることを要旨とする。上記構成によれば、請求項５に記載の発明と同様の効果が得られる。
【００２５】
請求項１６に記載の回路記述の検証プログラムは、プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の仕様データを記憶可能な記憶手段と、前記仕様データで表される論理モデルの検証の処理手順を制御する制御手段とを備えた回路記述の検証装置を稼動させるために用いられる回路記述の検証プログラムであって、前記制御手段を、前記論理モデル内に含まれる複数の状態及び各状態間の状態遷移により規定される複数のパスに対して該パスが検証対象とされるか否かを判別する際の判別条件を設定する判別条件設定手段、前記複数のパスについて、前記判別条件の設定態様に基づきパス毎における状態遷移の諾否を検査することにより、検証対象から除外される非検証用パスと検証対象とされる検証用パスとを判別するパス判別手段、該判別手段の判別結果に基づき、前記回路記述が検証される際には前記複数のパスのうち前記非検証用パスは検証が回避されると共に前記検証用パスは検証が行われるように、前記複数のパスを前記非検証用パスと前記検証用パスとを識別可能な状態にて保存するパス保存手段、及び、該パス保存手段により検証用パスとして識別可能に保存されたパスを検証対象にした検証作業を実行する検証手段として機能させることを要旨とする。上記構成によれば、請求項６に記載の発明と同様の効果が得られる。
【００２６】
請求項１７に記載の回路記述の検証プログラムは、請求項１６に記載の回路記述の検証プログラムにおいて、前記判別条件は、前記パスを構成する複数の状態のうち該状態を経由する状態遷移を禁止する禁止フラグを含んで構成されており、前記パス判別手段が前記パス毎の状態遷移の検査段階において前記判別条件として前記禁止フラグが設定された状態を含むパスを検査する場合には、該パスを前記パス判別手段に前記非検証用パスと判別させることを要旨とする。上記構成によれば、請求項７に記載の発明と同様の効果が得られる。
【００２７】
請求項１８に記載の回路記述の検証プログラムは、請求項１６又は請求項１７に記載の回路記述の検証プログラムにおいて、前記判別条件は、前記パスを構成する複数の状態のうち状態遷移の始点となる状態から終点となる状態に至るまでの途中で通過すべき状態であることを示す通過フラグを含んで構成されており、前記パス判別手段が前記パス毎の状態遷移の検査段階において前記判別条件として前記通過フラグが設定された状態を経由して前記終点となる状態に至ったパスを検査した場合には、該パスを前記パス判別手段に前記検証用パスと判別させることを要旨とする。上記構成によれば、請求項８に記載の発明と同様の効果が得られる。
【００２８】
請求項１９に記載の回路記述の検証プログラムは、請求項１６〜請求項１８のうち何れか一項に記載の回路記述の検証プログラムにおいて、前記制御手段を、前記パス判別手段によるパス毎の状態遷移の検査が開始されてからの経過時間が予め設定された閾値時間を越えたか否かを判定する時間判定手段として更に機能させ、前記時間判定手段が前記経過時間は前記閾値時間を超えたと判定した時点で、前記パス判別手段に前記パス毎の状態遷移の検査を終了させることを要旨とする。上記構成によれば、請求項９に記載の発明と同様の効果が得られる。
【００２９】
請求項２０に記載の回路記述の検証プログラムは、請求項１６〜請求項１９のうち何れか一項に記載の回路記述の検証プログラムにおいて、前記パス判別手段に、その時点で検査している状態からの更なる遷移先の状態を各状態の検査段階毎に順次抽出させ、抽出した遷移先の各状態からの更なる状態遷移を並行的に検査させることを要旨とする。上記構成によれば、請求項１０に記載の発明と同様の効果が得られる。
【００３０】
請求項２１に記載の回路記述の抽象化方法は、プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の抽象化方法であって、前記回路記述が示す論理モデル内に含まれる複数の状態及び各状態間の状態遷移により規定される複数のパスに対して該パスが検証対象とされるか否かを判別する際の判別条件を設定する判別条件設定段階と、前記複数のパスについて、前記判別条件の設定態様に基づきパス毎における状態遷移の諾否を検査することにより、検証対象から除外される非検証用パスと検証対象とされる検証用パスとを判別するパス判別段階と、該パス判別段階での判別結果に基づき、前記回路記述が検証される際には前記複数のパスのうち前記非検証用パスは検証が回避されると共に前記検証用パスは検証が行われるように、前記複数のパスを前記非検証用パスと前記検証用パスとを識別可能な状態にて保存するパス保存段階とを備えたことを要旨とする。上記構成によれば、請求項１に記載の発明と同様の効果が得られる。
【００３１】
請求項２２に記載の回路記述の抽象化方法は、請求項２１に記載の回路記述の抽象化方法において、前記判別条件は、前記パスを構成する複数の状態のうち該状態を経由する状態遷移を禁止する禁止フラグを含んで構成されており、前記パス判別段階では、前記パス毎の状態遷移の検査段階において前記判別条件として前記禁止フラグが設定された状態を含むパスを検査した場合に、該パスを前記非検証用パスと判別することを要旨とする。上記構成によれば、請求項２に記載の発明と同様の効果が得られる。
【００３２】
請求項２３に記載の回路記述の抽象化方法は、請求項２１又は請求項２２に記載の回路記述の抽象化方法において、前記判別条件は、前記パスを構成する複数の状態のうち始点となる状態から終点となる状態に至るまでの状態遷移の途中で通過すべき状態であることを示す通過フラグを含んで構成されており、前記パス判別段階では、前記パス毎の状態遷移の検査段階において前記判別条件として前記通過フラグが設定された状態を経由して前記終点となる状態に至ったパスを検査した場合に、該パスを前記検証用パスと判別することを要旨とする。上記構成によれば、請求項３に記載の発明と同様の効果が得られる。
【００３３】
請求項２４に記載の回路記述の抽象化方法は、請求項２１〜請求項２３のうち何れか一項に記載の回路記述の抽象化方法において、前記パス判別段階にてパス毎の状態遷移の検査が開始されてからの経過時間が予め設定された閾値時間を越えたか否かを判定する時間判定段階を更に備え、前記パス判別段階では、前記時間判定段階にて前記経過時間は前記閾値時間を超えたと判定した時点で、前記パス毎の状態遷移の検査を終了することを要旨とする。上記構成によれば、請求項４に記載の発明と同様の効果が得られる。
【００３４】
請求項２５に記載の回路記述の抽象化方法は、請求項２１〜請求項２４のうち何れか一項に記載の回路記述の抽象化方法において、前記パス判別段階では、その時点で検査している状態からの更なる遷移先の状態を各状態の検査段階毎に順次抽出し、該抽出された遷移先の各状態からの更なる状態遷移を並行的に検査することを要旨とする。上記構成によれば、請求項５に記載の発明と同様の効果が得られる。
【００３５】
請求項２６に記載の回路記述の検証方法は、プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の検証方法であって、前記回路記述が示す論理モデル内に含まれる複数の状態及び各状態間の状態遷移により規定される複数のパスに対して該パスが検証対象とされるか否かを判別する際の判別条件を設定する判別条件設定段階と、前記複数のパスについて、前記判別条件の設定態様に基づきパス毎における状態遷移の諾否を検査することにより、検証対象から除外される非検証用パスと検証対象とされる検証用パスとを判別するパス判別段階と、該パス判別段階での判別結果に基づき、前記回路記述が検証される際には前記複数のパスのうち前記非検証用パスは検証が回避されると共に前記検証用パスは検証が行われるように、前記複数のパスを前記非検証用パスと前記検証用パスとを識別可能な状態にて保存するパス保存段階と、該パス保存段階において検証用パスとして識別可能に保存されたパスを検証対象にした検証作業を実行する検証段階とを備えたことを要旨とする。上記構成によれば、請求項６に記載の発明と同様の効果が得られる。
【００３６】
請求項２７に記載の回路記述の検証方法は、請求項２６に記載の回路記述の検証方法において、前記判別条件は、前記パスを構成する複数の状態のうち該状態を経由する状態遷移を禁止する禁止フラグを含んで構成されており、前記パス判別段階では、前記パス毎の状態遷移の検査段階において前記判別条件として前記禁止フラグが設定された状態を含むパスを検査した場合に、該パスを前記非検証用パスと判別することを要旨とする。上記構成によれば、請求項７に記載の発明と同様の効果が得られる。
【００３７】
請求項２８に記載の回路記述の検証方法は、請求項２６又は請求項２７に記載の回路記述の検証方法において、前記判別条件は、前記パスを構成する複数の状態のうち始点となる状態から終点となる状態に至るまでの状態遷移の途中で通過すべき状態であることを示す通過フラグを含んで構成されており、前記パス判別段階では、前記パス毎の状態遷移の検査段階において前記判別条件として前記通過フラグが設定された状態を経由して前記終点となる状態に至ったパスを検査した場合に、該パスを前記検証用パスと判別することを要旨とする。上記構成によれば、請求項８に記載の発明と同様の効果が得られる。
【００３８】
請求項２９に記載の回路記述の検証方法は、請求項２６〜請求項２８のうち何れか一項に記載の回路記述の検証方法において、前記パス判別段階にてパス毎の状態遷移の検査が開始されてからの経過時間が予め設定された閾値時間を越えたか否かを判定する時間判定段階を更に備え、前記パス判別段階では、前記時間判定段階にて前記経過時間は前記閾値時間を超えたと判定した時点で、前記パス毎の状態遷移の検査を終了することを要旨とする。上記構成によれば、請求項９に記載の発明と同様の効果が得られる。
【００３９】
請求項３０に記載の回路記述の検証方法は、請求項２６〜請求項２９のうち何れか一項に記載の回路記述の検証方法において、前記パス判別段階では、その時点で検査している状態からの更なる遷移先の状態を各状態の検査段階毎に順次抽出し、該抽出された遷移先の各状態からの更なる状態遷移を並行的に検査することを要旨とする。上記構成によれば、請求項１０に記載の発明と同様の効果が得られる。
【発明を実施するための最良の形態】
【００４０】
以下、本発明を具体化した一実施形態を図１〜図４に従って説明する。
図１に示すように、本実施形態におけるコンピュータシステム１０は、制御装置１１、入力装置１２、出力装置１３、読み込み装置１４、及びディスク装置１５を備えている。そして、コンピュータシステム１０は、これらの各装置１１〜１５がバス１６を介して相互に情報を伝達可能に接続されることにより、回路記述の抽象化装置及び検証装置として各種の情報処理を行い得るように構成されている。なお、読み込み装置１４には、ＣＤ（Ｃｏｍｐａｃｔ  Ｄｉｓｃ）などの記録媒体１７が挿脱可能とされている。そして、本実施形態では、この読み込み装置１４に対して、プログラム言語を用いて記述された検証対象となるプログラムデータを記録した記録媒体１７及びこのプログラム言語を用いて記述されたプログラムデータの記述内容を形式的仕様記述言語による回路記述に変換する際に使用するモデリング変換ソフト（Ｓｉｍｕｌｉｎｋ、Ｓｃａｄｅ等）を記録した記録媒体１７が選択的に挿脱されるようになっている。
【００４１】
制御装置１１は、コンピュータシステム１０の稼動状態を制御するための制御手段として機能するものであり、その具体的構成については後述する。入力装置１２は、キーボードやマウス等を備えてなり、各種情報を手入力する場合に使用される。出力装置１３は、入力装置１２を介して入力された各種情報の内容を出力して表示可能なＣＲＴディスプレイ等を備えている。読み込み装置１４は、ＣＤ等の記録媒体１７を挿入された場合に該記録媒体１７に記録されているプログラムデータ等の各種データを読み込む。そして、ディスク装置１５は、読み込み装置１４により読み込まれた各種データを保存可能な記憶手段として機能する。
【００４２】
図１に示すように、制御装置１１は、外部装置との間の情報のやり取りを仲介するインターフェース（図示略）、中央処理装置としてのＣＰＵ１８、所定の情報を読み出し可能に記憶するＲＯＭ１９、及び各種の情報を書き込み／読み出し可能に記憶するＲＡＭ２０を備えたデジタルコンピュータとして構成されている。そして、こうした制御装置１１がデジタルコンピュータとして機能するように、ＣＰＵ１８は、インターフェースを介して各種の情報が入力された場合に、回路記述の抽象化及び抽象化された回路記述の検証のために必要とされる各種の論理演算を行うと共に、その論理演算において使用される各種情報の読み出し及び書き込みを行う。また、ＲＯＭ１９には、回路記述の抽象化処理、及び、抽象化された回路記述の検証処理に際して、ＣＰＵ１８がコンピュータシステム１０全体の稼動状態を制御するために用いる抽象化プログラム２１及び検証プログラム２２が記憶されている。また、ＲＡＭ２０には、コンピュータシステム１０の稼動中にＣＰＵ１８による論理演算において使用されると共に書き換えられる各種の情報内容が適宜記憶されるようになっている。
【００４３】
モデリング変換ソフト（例えば、Ｓｉｍｕｌｉｎｋ）を記録した記録媒体１７が読み込み装置１４に挿入された場合、ＣＰＵ１８は、その記録媒体１７に記録されたモデリング変換ソフトのデータ内容を読み込み装置１４により読み込ませ、その読み込みデータ内容をディスク装置１５にモデリングツール２３として記憶させる。また、プログラム言語を用いて記述された検証対象となるプログラムデータを記録した記録媒体１７が読み込み装置１４に挿入された場合、ＣＰＵ１８は、その記録媒体１７に記録されたプログラムデータをＲＡＭ２０に一旦記憶させる。そして次に、ディスク装置１５に記憶させたモデリングツール２３を起動させることにより、ＲＡＭ２０に一旦記憶させたプログラムデータを形式的仕様記述言語による回路記述の仕様データ２４に変換し、その変換した回路記述の仕様データ２４をディスク装置１５に記憶させる。
【００４４】
また、ＣＰＵ１８は、ＲＯＭ１９に記憶した抽象化プログラム２１を起動した場合に、ディスク装置１５に記憶させた回路記述の仕様データ２４が表す論理モデルに含まれる複数の状態及び各状態間の状態遷移により規定される複数のパスについて、図２に示す状態遷移図の表示態様で出力装置１３のディスプレイに表示させる。そして、ＣＰＵ１８は、その出力装置１３のディスプレイに表示された状態遷移図上の各パスについて、検証プログラム２２による検証処理に際して検証対象とするか否かを判別する際の判別条件を入力装置１２から入力可能とさせる。この点で、ＣＰＵ１８は、ユーザから入力装置１２を介して入力された判別条件を抽象化処理に際して適用可能に設定する判別条件設定手段としての判別条件設定部２５を備えているといえる。
【００４５】
また、ＣＰＵ１８は、論理モデル内の各パスに対して、判別条件設定部２５にて設定された判別条件を満たすか否かをそれぞれ検査して、その検査結果に基づき各パスについて検証対象となるか否かを判別する。この点で、ＣＰＵ１８は、判別条件を満たすパスに対して検証処理に際して検証対象であることを判別すると共に、判別条件を満たさないパスに対して検証処理に際して検証対象ではないことを判別するパス判別手段としてのパス判別部２６を備えているといえる。
【００４６】
また、ＣＰＵ１８は、論理モデル内の各パスについて、パス判別部２６にて、検証処理に際して検証対象であると判別されたパスであるか、或いは、検証処理に際して検証対象ではないと判別されたパスであるかを識別可能な状態にして保存する。そして、そのように識別可能な状態で各パスが保存された論理モデルで表される回路記述の仕様データ２４をディスク装置１５に既に記憶されている仕様データ２４に上書きして保存する。この点で、ＣＰＵ１８は、パス保存手段としてのパス保存部２７を備えているといえる。
【００４７】
また、ＣＰＵ１８は、タイマ機能を有しており、パス判別部２６が各パスの検査を開始してからの経過時間が予め設定された閾値時間を越えたか否かを判定して、そのパスの検査を終了するか否かを判断する。この点で、ＣＰＵ１８は、時間判定手段としての時間判定部２８を備えているといえる。
【００４８】
また、ＣＰＵ１８は、ＲＯＭ１９に記憶した検証プログラム２２を起動した場合に、パス保存部２７にて保存された各パスに付与された識別子をそれぞれ解析し、検証対象であることを示す識別子が付与されたパスをＲＡＭ２０から読み出して、読み出した各パスに対して検証作業を実行する。この点で、ＣＰＵ１８は、検証手段としての検証部２９を備えているといえる。
【００４９】
図２は、本実施形態のコンピュータシステム１０が適用される自動変速機の変速ギヤの変速段の状態遷移を模式的に示したものである。具体的には、「６ｔｈ」に示す状態は、変速ギヤが６速ギヤに設定されていることを示している。また、「６→２」に示す状態は、変速ギヤが６速ギヤから２速ギヤに移行する途中の遷移状態を示している。そして、ユーザは、変速ギヤの状態遷移の軌跡となるパスを判別して抽象化する判別条件として、種々のマークを入力装置１２からの入力操作に基づき設定可能となっている。
【００５０】
すなわち、パスの始点となる状態を示すＳ（Ｓｔａｒｔ）マーク３０、パスの終点となる状態を示すＥ（Ｅｎｄ）マーク３１、パスを構成する複数の状態のうち該状態を経由する状態遷移を禁止する禁止フラグとしての×マーク３２、パスを構成する複数の状態のうち状態遷移の始点となる状態から終点となる状態に至るまでの途中で通過すべき状態であることを示す通過フラグとしてのＰ１マーク３３を設定することが可能となっている。
【００５１】
ちなみに、本実施形態では、Ｓマーク３０を「６ｔｈ」、Ｅマーク３１を「３ｒｄ」、禁止フラグとしての×マーク３２を「１ｔｈ」「４ｔｈ」「５ｔｈ」、通過フラグとしてのＰ１マーク３３を「２ｔｈ」に対して各々設定している。そして、こうした入力装置１２を用いた判定条件となるＳマーク３０、Ｅマーク３１、×マーク３２、及びＰ１マーク３３の設定段階が判別条件設定段階に相当する。
【００５２】
次に、本実施形態のＣＰＵ１８が抽象化プログラム２１の起動に伴い実行する制御処理ルーチンについて、図３及び図４に基づき説明する。なお、本制御処理ルーチンは、図３に示すメインルーチンと図４に示すサブルーチンとからなる。
【００５３】
まず、図３に示すメインルーチンが開始すると、ＣＰＵ１８は、時間計測を開始すると共に、ディスク装置１５から回路記述の仕様データ２４を読み出し、その仕様データ２４が表す論理モデルに含まれる状態遷移図において、パスの始点となる状態を決定する（ステップＳ１１）。本実施形態の場合、図２に示す状態遷移図では「６ｔｈ」の状態にＳマーク３０が設定されていることから、ＣＰＵ１８は、この「６ｔｈ」の状態を検査すべき状態遷移の始状態と決定する。
【００５４】
続いて、ＣＰＵ１８は、ステップＳ１１にて決定された始点となる状態から遷移可能な全状態を抽出する（ステップＳ１２）。具体的には、始点として設定された「６ｔｈ」から遷移可能な遷移先の状態として、「６→１」「６→２」「６→３」「６→４」「６→５」の各遷移状態を抽出する。
【００５５】
続いて、パス判別段階として、ＣＰＵ１８は、ステップＳ１２にて抽出した全ての状態毎に、予め設定した判別条件を満たすか否かの検査を実行する（ステップＳ１３）。すなわち、このステップＳ１３において、ＣＰＵ１８は、図４に示すサブルーチンを図３のメインルーチンにおけるステップＳ１２において抽出される少なくとも一つの状態について、予め設定した判別条件を満たすか否かの検査を並行的に実行する。
【００５６】
ここで、ステップＳ１３におけるパス判別処理に関するサブルーチンについて、図４に基づき説明する。
まず、このサブルーチンが開始すると、ＣＰＵ１８は、ステップＳ１２にて抽出した検査対象となる各状態（「６→１」「６→２」「６→３」「６→４」「６→５」）に禁止フラグとしての×マーク３２が設定されていないか否かを判定する（ステップＳ２１）。そして、このステップＳ２１の判定結果が否定判定（×マークあり）である場合、ＣＰＵ１８は、その時点で検査対象としている状態（例えば「６→５」の遷移状態）を含むパスが予め設定した判別条件を満たしていないと判断し、そのパスを検証プログラム２２による回路記述の検証対象から除外される非検証用パスとして識別するための識別子を付与した状態でＲＡＭ２０に一時記憶して保存した後、そのパスに関する検査をＥＮＤ条件フラグの設定により終了する。一方、ステップＳ２１の判定結果が肯定判定（×マークなし）である場合、ＣＰＵ１８は、その時点で検査対象としている状態を含むパスが予め設定した判別条件を満たしていると判断し、その処理をステップＳ２２に移行する。
【００５７】
そして次に、ＣＰＵ１８は、その時点で検査対象としている状態にＥマーク３１が設定されていないか否かを判定する（ステップＳ２２）。そして、このステップＳ２２の判定結果が肯定判定（Ｅマークなし）である場合、ＣＰＵ１８は、その時点で検査対象としている状態を含むパスが判別条件を満たしていないと判断し、その処理を次のステップＳ２３に移行する。
【００５８】
続いて、時間判定段階として、ＣＰＵ１８は、その時点で検査対象としている状態を含むパスが状態遷移の始状態から現状態に至るまでの間で、検査に要した時間が予め設定した判別処理の閾値時間を越えたか否かを判断する（ステップＳ２３）。そして、このステップＳ２３の判定結果が肯定判定（時間オーバー）である場合、ＣＰＵ１８は、その時点で検査対象としている状態を含むパスの検査を既に十分に行っており、更なる検査は不要であると判断し、その検査のための処理（すなわち、図４に示すサブルーチン）を途中段階で強制的に終了する。なお、その際にも、ＣＰＵ１８は、その検査が途中段階で強制終了されたパスを検証プログラム２２による回路記述の検証対象から除外される非検証用パスとして識別するための識別子を付与した状態でＲＡＭ２０に一時記憶して保存した後、そのパスに関する検査をＥＮＤ条件フラグの設定により終了する。
【００５９】
一方、ステップＳ２３の判定結果が否定判定（閾値時間未満）である場合、ＣＰＵ１８は、その時点で検査対象としている状態を含むパスの検査が不十分であり、更なる検査が必要であると判断し、その処理を図３に示すメインルーチンのステップＳ１２に戻して再び現状態から遷移可能な全ての状態を抽出し、再度、抽出した状態毎に、予め設定した判別条件を満たすか否かの検査を実行する。その結果、ＣＰＵ１８は、再び、図４に示すサブルーチンの処理を繰り返すことになる。そして、こうしたサブルーチンの繰り返し処理において、ステップＳ２２の判定結果が否定判定（Ｅマークあり）である場合、ＣＰＵ１８は、その時点で検査対象としている状態を含むパスが判別条件を満たしていると判断し、その処理をステップＳ２４に移行する。
【００６０】
例えば、いま仮にステップＳ２２の処理時点で検査対象としている状態が図２においてＥマーク３１が設定された「３ｔｈ」の状態であり、且つ、その検査対象となるパスは始状態の「６ｔｈ」の状態から「６→２」の遷移状態、「２ｔｈ」の状態、「２→３」の遷移状態を経由して終状態の「３ｔｈ」の状態に至るパスである場合、ステップＳ２４での処理内容は次のようになる。
【００６１】
すなわち、ＣＰＵ１８は、そのパスが始点となる状態（「６ｔｈ」）から終点となる状態（「３ｔｈ」）に至るまでの間に、通過フラグとしてのＰ１マーク３３が設定された状態を含むか否かを判断する（ステップＳ２４）。そして、このステップＳ２４の判定結果が否定判定（Ｐ１マークなし）である場合、ＣＰＵ１８は、そのパスが予め設定した判別条件を満たしていないと判断し、その処理を前述したステップＳ２３に移行する。
【００６２】
その一方、ステップＳ２４の判定結果が肯定判定（Ｐ１マークあり）である場合、パス保存段階として、ＣＰＵ１８は、そのパスが始点となる状態から通過フラグとしてのＰ１マーク３３の設定された状態（この場合、「２ｔｈ」の状態）を経由して終点となる状態に至ったものであり、予め設定した判別条件を満たしていると判断する。そして、その時点で検査対象としている状態を含むパスを検証プログラム２２により検証対象とされる検証用パスとして識別するための識別子を付与した状態でＲＡＭ２０に一時記憶して保存した後、そのパスの検査をＥＮＤ条件フラグの設定により終了する（ステップＳ２５）。
【００６３】
以上のようにして図３におけるメインルーチンのステップＳ１３（すなわち、図４に示すサブルーチン）がＥＮＤ条件フラグの設定により終了すると、ＣＰＵ１８は、ステップＳ１３での判別条件に関する検査が全てのパスにおいて完了したか否かを判断する（ステップＳ１４）。そして、ステップＳ１４の判定結果が否定判定（すなわち、未だＥＮＤ条件フラグの設定されていないパスが存在するとの判定結果）である場合、ＣＰＵ１８は、その処理をステップＳ１３に戻して、再度、ステップＳ１２にて抽出した各状態のうち判別条件に関する検査が未実施の残っている状態についてステップＳ１３の処理を行う。
【００６４】
一方、ステップＳ１４の判定結果が肯定判定である場合、ＣＰＵ１８は、ＲＡＭ２０に各パスを非検証パスと検証用パスとに識別可能な状態にして一時記憶して保存したデータ内容をディスク装置１５に記憶されている回路記述の仕様データ２４に上書きして保存した後、抽象化プログラム２１の起動に基づいた本制御処理のメインルーチンを終了する。
【００６５】
その後、ディスク装置１５に記憶されている回路記述の仕様データ２４に基づき検証対象とされるプログラム内容を検証する場合、ＣＰＵ１８は、検証段階として、ＲＯＭ１９に記憶している検証プログラム２２を起動して、ディスク装置１５に記憶されている回路記述の仕様データ２４を読み出す。そして、ＣＰＵ１８は、その仕様データ２４により表される論理モデルに含まれる複数のパスのうち、検証用パスを示す識別子が付与されたパスを読み出して、そのパスを検証対象にした自動変速機に関する各種デバッグ用の検証を実行する。
【００６６】
以上説明したように、変速ギヤの変速段の状態及び各状態間の遷移を検証する場合、各状態から遷移可能な全ての状態の抽出を再帰的に実行することでパスの数が指数的に増大し、それらの検証に要するＣＰＵ１８の処理負荷も急激に増大するという問題があるところ、本実施形態のコンピュータシステム１０によれば、各状態から遷移可能な状態を抽出した後、判別条件を満たさないパスが非検証用パスとしてモデルから除外される。そのため、各状態から遷移可能な状態を無作為に抽出して得られた全てのパスを構成要素としてモデルを構築した場合と比較して、検証対象となるパスの数を削減することでモデルの規模を縮小させることが可能となる。したがって、回路記述の仕様データ２４の規模が増大したとしても、ＣＰＵ１８の処理負荷の増大を抑制しつつ、同モデルの検証を実行することが可能となる。
【００６７】
また、回路記述の仕様データ２４で表されるモデルの規模を縮小させる方法として、回路記述の仕様データ２４の一部を削除することなく、同モデル内に含まれる複数のパスを検証プログラム２２による検証対象となる検証用パスと検証対象から除外される非検証用パスとに識別可能な状態で全て残すようにしている。すなわち、モデル内の状態又は各状態間の遷移に対して禁止フラグとしての×マーク３２を設定した場合であっても、それらの状態がモデル内から消去されることはない。そのため、判別条件を設定することにより、自動変速機の変速ギヤに関する他のシミュレーションの各種設定に影響を及ぼすことはない。
【００６８】
本実施形態によれば、以下の効果を得ることができる。
（１）上記実施形態における検証プログラム２２を用いた回路記述の検証方法によれば、コンピュータシステム１０が回路記述の仕様データ２４で表される論理モデルを検証する際、その論理モデルにおいて検証用パスとして識別可能な状態で保存されているパスについては検証対象とする一方で、非検証用パスとして識別可能な状態で保存されているパスについては検証対象から除外した検証作業を実行することが可能であるため、検証作業が迅速且つ簡単になる。また、検証対象から除外するパスについても回路記述の仕様データ２４から削除することなく、非検証用パスとして識別可能な状態で検証対象とされる検証用パスと共に元の回路記述の仕様データ２４内に保存されているので、新たに検証作業をやり直すために判別条件の設定を変更する際にも、一旦削除したパスを復元させるような作業が不要となり、迅速且つ容易に再検証を行うことができる。したがって、プログラムの記述内容を形式的手法による検証が可能な形式的仕様に変換した回路記述の仕様データ２４の検証を簡便ならしめることができる。
【００６９】
（２）上記実施形態における抽象化プログラム２１を用いた回路記述の抽象化方法によれば、パス毎の状態遷移の検査段階において禁止フラグとしての×マーク３２が判別条件として設定された状態を経由する時点で、その状態を含むパスを検証対象から除外する非検証用パスとして判別できるので、回路記述の仕様データ２４で表される論理モデルの抽象化を容易に行うことができる。
【００７０】
（３）上記実施形態における抽象化プログラム２１を用いた回路記述の抽象化方法によれば、パス毎の状態遷移の検査段階において、始点となる状態から終点となる状態に至るまでの状態遷移の途中で通過フラグとしてのＰ１マーク３３が判別条件として設定された状態を経由する時点で、その状態を含むパスを検証対象とする検証用パスとして判別できるので、回路記述の仕様データ２４で表される論理モデルの抽象化を容易に行うことができる。
【００７１】
（４）上記実施形態における抽象化プログラム２１を用いた回路記述の抽象化方法によれば、パス毎の状態遷移の検査が開始されてからの経過時間が予め設定された判別処理の閾値時間を越えたと判定した時点でその検査を強制的に終了するようになっている。そのため、状態遷移の検査段階で終点となる状態に至っても更なる遷移先となる状態が新たに抽出されて無限に継続するような検査を適正に終了させることができ、回路記述の仕様データ２４で表されるモデルの抽象化を容易に行うことができる。
【００７２】
（５）上記実施形態における抽象化プログラム２１を用いた回路記述の抽象化方法によれば、その時点で検査している状態からの更なる遷移先の状態を各状態の検査段階毎に順次抽出し、該抽出された遷移先の各状態からの更なる状態遷移を並行的に検査するようになっている。そのため、複数のパスにおける状態遷移を並行して網羅的に検査できるので、回路記述の仕様データ２４で表されるモデルの抽象化を容易に行うことができる。
【００７３】
なお、上記実施形態は以下のような別の実施形態に変更してもよい。
・上記実施形態において、抽象化プログラム２１は、各パスにおける終点となる状態を起点として検査を開始した後、その時点で検査している状態の遷移前の状態を各状態の検査段階毎に順次抽出し、該抽出された遷移前の状態からの更なる遷移前の状態を始点となる状態に向けて並行的に検査するようにしてもよい。
【００７４】
・上記実施形態において、抽象化プログラム２１は、始点となる状態から遷移可能な状態を抽出した後、抽出した状態のうち一つの状態を選択する操作と、その選択した状態から遷移可能な全ての状態を検査する操作とを交互に実行するようにしてもよい。
【００７５】
・上記実施形態において、抽象化プログラム２１は、判別条件に関する検査を実行した状態数をカウントし、その値が予め設定した閾値を越えたと判定した時点で検査を終了するようにしてもよい。
【００７６】
・上記実施形態において、抽象化プログラム２１は、判別条件としての禁止フラグを×マーク３２以外のマークで表示設定するようにしてもよい。
・上記実施形態において、判別条件としての通過フラグをＰ１マーク３３以外のマークで表示設定するようにしてもよい。
【００７７】
・上記実施形態において、抽象化プログラム２１は、検証プログラム２２に含まれるプログラム構成であってもよい。
【図面の簡単な説明】
【００７８】
【図１】本実施形態のコンピュータシステムを示すブロック図。
【図２】変速ギヤの変速段の状態遷移を模式的に示す状態遷移図。
【図３】抽象化プログラムのメインルーチンを示すフローチャート。
【図４】抽象化プログラムのサブルーチンを示すフローチャート。
【符号の説明】
【００７９】
１０…抽象化装置及び検証装置としてのコンピュータシステム、１１…制御手段としての制御装置、１５…記憶手段としてのディスク装置、１８…判別条件設定手段、パス判別手段、パス保存手段、時間判定手段、及び検証手段としてのＣＰＵ、２１…抽象化プログラム、２２…検証プログラム、２４…回路記述の仕様データ、３０…判別条件を構成するＳマーク、３１…判別条件を構成するＥマーク、３２…判別条件を構成する禁止フラグとしての×マーク、３３…判別条件を構成する通過フラグとしてのＰ１マーク。
【図１】
2010079432.tif 000003
【図２】
2010079432.tif 000004
【図３】
2010079432.tif 000005
【図４】
2010079432.tif 000006