(57)【要約】【課題】時相論理式の中に記載されるオブジェクト記述を生成する。【解決手段】オブジェクト数算出部１２０は、クラス毎にステレオタイプと多重度とを含むクラス図情報データを用いて、ステレオタイプ毎に多重度の合計をオブジェクト数として算出する。オブジェクト記述生成部１３０は、ステレオタイプ毎に、時相論理式パターンから記述ルールを取得し、取得された記述ルールを用いてオブジェクト数と同じ数のオブジェクト名を含んだオブジェクト記述を生成する。【選択図】図１
2018147187.tif 000002
【特許請求の範囲】
【請求項１】
クラス間の関係を示すクラス図に含まれる情報としてクラス毎にステレオタイプと多重度とを含むクラス図情報データを用いて、ステレオタイプ毎に多重度の合計をオブジェクト数として算出するオブジェクト数算出部と、
ステレオタイプ毎に、時相論理式の中に記載されるオブジェクト名に対応するオペランド毎に同じオペランドに対応する複数のオブジェクト名を記述するための記述ルールを含む時相論理式パターンから記述ルールを取得し、取得された記述ルールを用いてオブジェクト数と同じ数のオブジェクト名を含んだオブジェクト記述を生成するオブジェクト記述生成部と
を備える時相論理式生成装置。
【請求項２】
前記オブジェクト記述生成部は、オペランド名とステレオタイプとを互いに対応付けるメタモデルから前記クラス図に含まれるステレオタイプ毎にオペランド名を取得し、取得されたオペランド名に対応する記述ルールを前記時相論理式パターンから取得し、取得された記述ルールを用いて前記オブジェクト記述を生成する
請求項１に記載の時相論理式生成装置。
【請求項３】
前記時相論理式パターンは、時相論理式の書式をオペランド名を用いて示す時相論理式テンプレートと前記時相論理式テンプレートに含まれるオペランド名毎の記述ルールとを含み、
前記時相論理式生成装置は、前記時相論理式テンプレートと前記オブジェクト記述とを表示する表示部を備える
請求項１または請求項２に記載の時相論理式生成装置。
【請求項４】
前記クラス図を示すクラス図データを用いて前記クラス図情報データを生成するクラス図変換部を備える
請求項１から請求項３のいずれか１項に記載の時相論理式生成装置。
【請求項５】
前記時相論理式生成装置は、時相論理式パターンを受け付ける受付部を備え、
前記オブジェクト記述生成部は、受け付けられた時相論理式パターンを用いて前記オブジェクト記述を生成する
請求項１から請求項４のいずれか１項に記載の時相論理式生成装置。
【請求項６】
前記時相論理式パターンは、前記時相論理式の書式をオペランド名を用いて示す時相論理式テンプレートと前記時相論理式テンプレートに含まれるオペランド名毎の記述ルールとを含み、
前記時相論理式生成装置は、前記時相論理式テンプレートに含まれるオペランド名を前記オブジェクト記述に置き換えることによって前記時相論理式を生成する時相論理式生成部を備える
請求項１から請求項５のいずれか１項に記載の時相論理式生成装置。
【請求項７】
クラス間の関係を示すクラス図に含まれる情報としてクラス毎にステレオタイプと多重度とを含むクラス図情報データを用いて、ステレオタイプ毎に多重度の合計をオブジェクト数として算出するオブジェクト数算出部と、
ステレオタイプ毎に、時相論理式の中に記載されるオブジェクト名に対応するオペランド毎に同じオペランドに対応する複数のオブジェクト名を記述するための記述ルールを含む時相論理式パターンから記述ルールを取得し、取得された記述ルールを用いてオブジェクト数と同じ数のオブジェクト名を含んだオブジェクト記述を生成するオブジェクト記述生成部
としてコンピュータを機能させるための時相論理式生成プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、時相論理式を生成するための技術に関するものである。
【背景技術】
【０００２】
モデル検査は、起きうる全てのシナリオを仮想的に検証する技術である。
モデル検査では、検査対象に対する検証項目が時相論理式で記述される。
時相論理式は、順序関係を表現することが可能な論理式である。例えば、時相論理式によって「事象ｐが真ならば、いつか必ず事象ｑは真になる」といった文を表現できる。
【０００３】
モデル検査において検査対象が変更された場合、時相論理式を修正する必要がある。しかし、時相論理式の修正は手間がかかる作業である。
【０００４】
特許文献１は、モデル検査においてシーケンス記述に基づいて時相論理式を生成する技術を開示している。具体的には、データ送受信のシーケンスが記述されているシーケンス記述と時相論理式テンプレートとを用いて時相論理式が生成される。
【０００５】
特許文献２は、複数のシーケンス図を用いて時相論理式を生成する技術を開示している。具体的には、複数のシーケンス図からオブジェクト間のやりとりの順序関係が抽出され、抽出された順序関係に基づいて時相論理式が生成される。
【先行技術文献】
【特許文献】
【０００６】
【特許文献１】特開２０１３−２２８７８０号公報
【特許文献２】国際公開２００８／１２３０２１号公報
【発明の概要】
【発明が解決しようとする課題】
【０００７】
従来の技術では、検証対象が変更された場合に時相論理式を自動的に修正することはできない。
つまり、特許文献１または特許文献２に開示された技術では、検査対象の変更に合わせて時相論理式を生成することはできない。
【０００８】
本発明は、時相論理式の中に記載されるオブジェクト記述を生成できるようにすることを目的とする。
【課題を解決するための手段】
【０００９】
本発明の時相論理式生成装置は、
クラス間の関係を示すクラス図に含まれる情報としてクラス毎にステレオタイプと多重度とを含むクラス図情報データを用いて、ステレオタイプ毎に多重度の合計をオブジェクト数として算出するオブジェクト数算出部と、
ステレオタイプ毎に、時相論理式の中に記載されるオブジェクト名に対応するオペランド毎に同じオペランドに対応する複数のオブジェクト名を記述するための記述ルールを含む時相論理式パターンから記述ルールを取得し、取得された記述ルールを用いてオブジェクト数と同じ数のオブジェクト名を含んだオブジェクト記述を生成するオブジェクト記述生成部とを備える。
【発明の効果】
【００１０】
本発明によれば、時相論理式の中に記載されるオブジェクト記述を生成することができる。その結果、生成されるオブジェクト記述を用いることによって、検査対象が変更された場合の時相論理式を生成することが可能となる。
【図面の簡単な説明】
【００１１】
【図１】実施の形態１における時相論理式生成装置１００の構成図。
【図２】実施の形態１における時相論理式生成方法のフローチャート。
【図３】実施の形態１におけるクラス図２００を示す図。
【図４】実施の形態１におけるクラス図変換処理（Ｓ１１０）のフローチャート。
【図５】実施の形態１におけるクラス図情報データ２１０を示す図。
【図６】実施の形態１におけるオブジェクト数算出処理（Ｓ１２０）のフローチャート。
【図７】実施の形態１におけるクラス情報データ生成（Ｓ１２１）のフローチャート。
【図８】実施の形態１におけるクラス情報データ２２１を示す図。
【図９】実施の形態１におけるオブジェクト数データ生成（Ｓ１２２）のフローチャート。
【図１０】実施の形態１におけるオブジェクト数データ２２２を示す図。
【図１１】実施の形態１におけるオブジェクト記述生成処理（Ｓ１３０）のフローチャート。
【図１２】実施の形態１におけるオブジェクトデータ生成（Ｓ１３１）のフローチャート。
【図１３】実施の形態１におけるメタモデル２３１を示す図。
【図１４】実施の形態１におけるオブジェクトデータ２３２を示す図。
【図１５】実施の形態１における時相論理式データ生成（Ｓ１３２）のフローチャート。
【図１６】実施の形態１における時相論理式パターン２３３を示す図。
【図１７】実施の形態１における時相論理式データ２３４を示す図。
【図１８】実施の形態２における時相論理式生成方法のフローチャート。
【図１９】実施の形態３における時相論理式生成装置１００の構成図。
【図２０】実施の形態３における時相論理式生成方法のフローチャート。
【図２１】実施の形態３におけるオブジェクト記述生成処理（Ｓ１５０）のフローチャート。
【図２２】実施の形態における時相論理式生成装置１００のハードウェア構成図。
【発明を実施するための形態】
【００１２】
実施の形態および図面において、同じ要素および対応する要素には同じ符号を付している。同じ符号が付された要素の説明は適宜に省略または簡略化する。図中の矢印はデータの流れ又は処理の流れを主に示している。
【００１３】
実施の形態１．
時相論理式の中に記載される記述を生成する形態について、図１から図１７に基づいて説明する。
【００１４】
＊＊＊構成の説明＊＊＊
図１に基づいて、時相論理式生成装置１００の構成を説明する。
時相論理式生成装置１００は、プロセッサ９０１とメモリ９０２と補助記憶装置９０３と入出力インタフェース９０４といったハードウェアを備えるコンピュータである。これらのハードウェアは、信号線を介して互いに接続されている。
【００１５】
プロセッサ９０１は、演算処理を行うＩＣ（Ｉｎｔｅｇｒａｔｅｄ  Ｃｉｒｃｕｉｔ）であり、他のハードウェアを制御する。例えば、プロセッサ９０１は、ＣＰＵ（Ｃｅｎｔｒａｌ  Ｐｒｏｃｅｓｓｉｎｇ  Ｕｎｉｔ）、ＤＳＰ（Ｄｉｇｉｔａｌ  Ｓｉｇｎａｌ  Ｐｒｏｃｅｓｓｏｒ）、またはＧＰＵ（Ｇｒａｐｈｉｃｓ  Ｐｒｏｃｅｓｓｉｎｇ  Ｕｎｉｔ）である。
メモリ９０２は揮発性の記憶装置である。メモリ９０２は、主記憶装置またはメインメモリとも呼ばれる。例えば、メモリ９０２はＲＡＭ（Ｒａｎｄｏｍ  Ａｃｃｅｓｓ  Ｍｅｍｏｒｙ）である。メモリ９０２に記憶されたデータは必要に応じて補助記憶装置９０３に保存される。
補助記憶装置９０３は不揮発性の記憶装置である。例えば、補助記憶装置９０３は、ＲＯＭ（Ｒｅａｄ  Ｏｎｌｙ  Ｍｅｍｏｒｙ）、ＨＤＤ（Ｈａｒｄ  Ｄｉｓｋ  Ｄｒｉｖｅ）、またはフラッシュメモリである。補助記憶装置９０３に記憶されたデータは必要に応じてメモリ９０２にロードされる。
【００１６】
入出力インタフェース９０４は入力装置および出力装置が接続されるポートである。例えば、入出力インタフェース９０４はＵＳＢ端子であり、入力装置はキーボードおよびマウスであり、出力装置はディスプレイである。ＵＳＢはＵｎｉｖｅｒｓａｌ  Ｓｅｒｉａｌ  Ｂｕｓの略称である。
【００１７】
時相論理式生成装置１００は、クラス図変換部１１０とオブジェクト数算出部１２０とオブジェクト記述生成部１３０といったソフトウェア要素を備える。ソフトウェア要素はソフトウェアで実現される要素である。
【００１８】
補助記憶装置９０３には、クラス図変換部１１０とオブジェクト数算出部１２０とオブジェクト記述生成部１３０としてコンピュータを機能させるための時相論理式生成プログラムが記憶されている。時相論理式生成プログラムは、メモリ９０２にロードされて、プロセッサ９０１によって実行される。
さらに、補助記憶装置９０３にはＯＳ（Ｏｐｅｒａｔｉｎｇ  Ｓｙｓｔｅｍ）が記憶されている。ＯＳの少なくとも一部は、メモリ９０２にロードされて、プロセッサ９０１によって実行される。
つまり、プロセッサ９０１は、ＯＳを実行しながら、時相論理式生成プログラムを実行する。
時相論理式生成プログラムを実行して得られるデータは、メモリ９０２、補助記憶装置９０３、プロセッサ９０１内のレジスタまたはプロセッサ９０１内のキャッシュメモリといった記憶装置に記憶される。
【００１９】
メモリ９０２はデータを記憶する記憶部１９１として機能する。但し、他の記憶装置が、メモリ９０２の代わりに、又は、メモリ９０２と共に、記憶部１９１として機能してもよい。
入出力インタフェース９０４は、入力を受け付ける受付部１９２として機能する。さらに、入出力インタフェース９０４は、ディスプレイに画像などを表示する表示部１９３として機能する。
【００２０】
時相論理式生成装置１００は、プロセッサ９０１を代替する複数のプロセッサを備えてもよい。複数のプロセッサは、プロセッサ９０１の役割を分担する。
【００２１】
時相論理式生成プログラムは、磁気ディスク、光ディスクまたはフラッシュメモリ等の不揮発性の記憶媒体にコンピュータ読み取り可能に記憶することができる。不揮発性の記憶媒体は、一時的でない有形の媒体である。
【００２２】
＊＊＊動作の説明＊＊＊
時相論理式生成装置１００の動作は時相論理式生成方法に相当する。また、時相論理式生成方法の手順は時相論理式生成プログラムの手順に相当する。
【００２３】
図２に基づいて、時相論理式生成方法を説明する。
ステップＳ１０１において、利用者は、入力装置を操作して、時相論理式生成装置１００にクラス図データを入力する。
受付部１９２は入力されたクラス図データを受け付け、記憶部１９１は受け付けられたクラス図データを記憶する。
【００２４】
クラス図データは、クラス図を示すデータである。
クラス図は、オブジェクト指向におけるクラス間の関係を示す図である。
【００２５】
具体的には、クラス図は、互いに関連する複数のクラスを含み、クラス毎にクラス名とステレオタイプとを含み、クラス間の関連毎に関連付けられている各々のクラスの多重度を含む。
クラス名は、クラスの名称である。
ステレオタイプは、クラスの役割を識別する識別子である。
多重度は、クラスに対応するオブジェクトの数を表す値である。
【００２６】
ステップＳ１１０において、クラス図変換部１１０は、ステップＳ１０１で受け付けられたクラス図データを用いて、クラス図情報データを生成する。記憶部１９１は、生成されたクラス図情報データを記憶する。
クラス図情報データは、クラス図に含まれる情報としてクラス毎にステレオタイプと多重度とを含むデータである。
【００２７】
ステップＳ１２０において、オブジェクト数算出部１２０は、ステップＳ１１０で生成されたクラス図情報データを用いて、クラス図に含まれるステレオタイプ毎に多重度の合計を算出する。算出される合計をオブジェクト数という。
オブジェクト数算出処理（Ｓ１２０）の詳細については後述する。
【００２８】
ステップＳ１３０において、オブジェクト記述生成部１３０は、時相論理式パターンを用いて、ステレオタイプ毎にオブジェクト記述を生成する。記憶部１９１は、生成されたオブジェクト記述を記憶する。
時相論理式パターンは、時相論理式テンプレートと時相論理式テンプレートに含まれるオペランド名毎の記述ルールとを含むデータであり、記憶部１９１に記憶されている。
時相論理式テンプレートは、時相論理式の書式をオペランド名を用いて示す。オペランド名はオペランドの名称である。オペランドは真または偽の値が入る変数である。
記述ルールは、同じオペランド名に対応する複数のオブジェクト名を記述するためのルールである。
オブジェクト記述は、オブジェクト数と同じ数のオブジェクト名を含んだ文字列である。
オブジェクト記述生成処理（Ｓ１３０）の詳細については後述する。
【００２９】
ステップＳ１４０において、表示部１９３は、ステップＳ１３０で生成されたステレオタイプ毎のオブジェクト記述を表示する。
具体的には、表示部１９３は、時相論理式テンプレートとステレオタイプ毎のオブジェクト記述とをディスプレイに表示する。
【００３０】
図３に、クラス図２００を示す。クラス図２００はクラス図の具体例である。
クラス図２００は４つのクラスを含んでいる。角丸四角形がクラスを表している。
それぞれのクラスはクラス名とステレオタイプとを含んでいる。下段に記載されたＣｌａｓｓＸ（Ｘは１、２、３または６）がクラス名である。上段において二重括弧の中に記載された文字列がステレオタイプである。
クラス同士を繋ぐ線はクラス間の関連を表している。
クラス同士を繋ぐ線に付された値が多重度である。
【００３１】
図４に基づいて、クラス図変換処理（Ｓ１１０）の詳細を説明する。
ステップＳ１１１において、クラス図変換部１１０は、クラス図データから関連を抽出する。
ステップＳ１１２において、クラス図変換部１１０は、未選択の関連を１つ選択する。
ステップＳ１１３において、クラス図変換部１１０は、選択された関連の第１クラス情報をクラス図データから取得する。第１クラス情報は第１クラスのクラス情報である。第１クラスは、互いに関連付けられた２つのクラスのうちの一方のクラスである。クラス情報はクラス名、ステレオタイプおよび多重度である。
ステップＳ１１４において、クラス図変換部１１０は、選択された関連の第２クラス情報をクラス図データから取得する。第２クラス情報は第２クラスのクラス情報である。第２クラスは、互いに関連付けられた２つのクラスのうちの他方のクラスである。
ステップＳ１１５において、クラス図変換部１１０は、第１クラス情報と第２クラス情報とを互いに対応付けてクラス図情報データに登録する。
ステップＳ１１６において、クラス図変換部１１０は、未選択の関連が有るか判定する。
未選択の関連が有る場合、処理はステップＳ１１２に進む。
未選択の関連が無い場合、クラス図変換処理（Ｓ１１０）は終了する。
【００３２】
図５に、クラス図情報データ２１０を示す。クラス図情報データ２１０は、図３のクラス図２００に対応するクラス図情報データである。
クラス図情報データ２１０は、表形式のデータであり、クラス図２００に含まれる関連毎にレコード（行）を有する。
レコードは、関連番号と第１クラスと第１ステレオタイプと第１多重度と第２クラスと第２ステレオタイプと第２多重度とのそれぞれの欄を有する。
関連番号の欄は、関連番号を示す。関連番号は、関連を識別する通し番号である。
第１クラスの欄は、第１クラスのクラス名を示す。
第１ステレオタイプの欄は、第１クラスのステレオタイプを示す。
第１多重度の欄は、第１クラスの多重度を示す。
第２クラスの欄は、第２クラスのクラス名を示す。
第２ステレオタイプの欄は、第２クラスのステレオタイプを示す。
第２多重度の欄は、第２クラスの多重度を示す。
【００３３】
図６に基づいて、オブジェクト数算出処理（Ｓ１２０）の詳細を説明する。
ステップＳ１２１において、オブジェクト数算出部１２０は、クラス図情報データを用いてクラス情報データを生成する。記憶部１９１は、生成されたクラス情報データを記憶する。
クラス情報データは、クラス毎にクラス情報を示すデータである。
クラス情報データ生成（Ｓ１２１）の詳細については後述する。
【００３４】
ステップＳ１２２において、オブジェクト数算出部１２０は、クラス情報データを用いてオブジェクト数データを生成する。記憶部１９１は、生成されたオブジェクト数データを記憶する。
オブジェクト数データは、ステレオタイプ毎のオブジェクト数を示すデータである。
オブジェクト数データ生成（ステップＳ１２２）の詳細については後述する。
【００３５】
図７に基づいて、クラス情報データ生成（Ｓ１２１）の手順を説明する。
ステップＳ１２１１において、オブジェクト数算出部１２０は、クラス図情報データからクラス名を抽出する。
ステップＳ１２１２において、オブジェクト数算出部１２０は、未選択のクラス名を１つ選択する。
ステップＳ１２１３において、オブジェクト数算出部１２０は、選択されたクラス名に対応するクラス情報をクラス図情報データから取得する。
ステップＳ１２１４において、オブジェクト数算出部１２０は、取得されたクラス情報をクラス情報データに登録する。
ステップＳ１２１５において、オブジェクト数算出部１２０は、未選択のクラス名が有るか判定する。
未選択のクラス名が有る場合、処理はステップＳ１２１２に進む。
未選択のクラス名が無い場合、クラス情報データ生成（Ｓ１２１）は終了する。
【００３６】
図８に、クラス情報データ２２１を示す。クラス情報データ２２１は、図５のクラス図情報データ２１０に対応するクラス情報データである。
クラス情報データ２２１は、クラス名毎にレコード（行）を有する。
レコードは、クラス名とステレオタイプと多重度とのそれぞれの欄を有する。
クラス名の欄は、クラスの名称を示す。
ステレオタイプの欄は、クラスのステレオタイプを示す。
多重度の欄は、クラスの多重度を示す。
【００３７】
図９に基づいて、オブジェクト数データ生成（Ｓ１２２）の手順を説明する。
ステップＳ１２２１において、オブジェクト数算出部１２０は、クラス情報データからステレオタイプを抽出する。
ステップＳ１２２２において、オブジェクト数算出部１２０は、未選択のステレオタイプを１つ選択する。
ステップＳ１２２３において、オブジェクト数算出部１２０は、選択されたステレオタイプに対応付けられた全ての多重度を取得する。
ステップＳ１２２４において、オブジェクト数算出部１２０は、取得された多重度の合計を算出する。算出される合計をオブジェクト数という。
ステップＳ１２２５において、オブジェクト数算出部１２０は、オブジェクト数をオブジェクト数データに登録する。
【００３８】
図１０に、オブジェクト数データ２２２を示す。オブジェクト数データ２２２は、図８のクラス情報データ２２１に対応するオブジェクト数データである。
オブジェクト数データ２２２は、ステレオタイプ毎にレコード（行）を有する。
レコードは、ステレオタイプとオブジェクト数とのそれぞれの欄を有する。
ステレオタイプの欄は、ステレオタイプを示す。
オブジェクト数の欄は、オブジェクト数を示す。
【００３９】
図１１に基づいて、オブジェクト記述生成処理（Ｓ１３０）の手順を説明する。
ステップＳ１３１において、オブジェクト記述生成部１３０は、メタモデルとオブジェクト数データとを用いて、オブジェクトモデルを生成する。記憶部１９１は、生成されたオブジェクトモデルを記憶する。
メタモデルは、オペランド名とステレオタイプとを互いに対応付けるデータであり、記憶部１９１に記憶されている。
オブジェクトモデルは、メタモデルとオブジェクト数データとを結合して得られるデータである。
オブジェクトデータ生成（Ｓ１３１）の詳細については後述する。
【００４０】
ステップＳ１３２において、オブジェクト記述生成部１３０は、オブジェクトモデルと時相論理式パターンとを用いて、時相論理式データを生成する。記憶部１９１は、生成された時相論理式データを記憶する。
時相論理式データは、時相論理式テンプレートとオブジェクト記述とを含んだデータである。
時相論理式データ生成（Ｓ１３２）の詳細については後述する。
【００４１】
図１２に基づいて、オブジェクトデータ生成（Ｓ１３１）の詳細を説明する。
ステップＳ１３１１において、オブジェクト記述生成部１３０は、オブジェクト数データから、未選択のステレオタイプを１つ選択する。
【００４２】
ステップＳ１３１２において、オブジェクト記述生成部１３０は、選択されたステレオタイプと同じステレオタイプに対応付けられたオペランド名がメタモデルの中に有るか判定する。
該当するオペランドが有る場合、処理はステップＳ１３１３に進む。
該当するオペランドが無い場合、処理はステップＳ１３１５に進む。
【００４３】
ステップＳ１３１３において、オブジェクト記述生成部１３０は、選択されたステレオタイプと同じステレオタイプに対応付けられたオペランド名をメタモデルから取得する。
さらに、オブジェクト記述生成部１３０は、選択されたステレオタイプに対応付けられたオブジェクト数をオブジェクト数データから取得する。
【００４４】
ステップＳ１３１４において、オブジェクト記述生成部１３０は、取得されたオペランド名と選択されたステレオタイプと取得されたオブジェクト数とをオブジェクトデータに登録する。
【００４５】
ステップＳ１３１５において、オブジェクト記述生成部１３０は、未選択のステレオタイプが有るか判定する。
未選択のステレオタイプが有る場合、処理はステップＳ１３１１に進む。
未選択のステレオタイプが無い場合、オブジェクトデータ生成（Ｓ１３１）は終了する。
【００４６】
図１３に、メタモデル２３１を示す。メタモデル２３１はメタモデルの具体例である。
メタモデル２３１は、オペランド名とステレオタイプとの組毎にレコード（行）を有する。
レコードは、オペランド名とステレオタイプとのそれぞれの欄を有する。
オペランド名の欄は、オペランドの名称を示す。
ステレオタイプの欄は、ステレオタイプを示す。
【００４７】
図１４に、オブジェクトデータ２３２を示す。オブジェクトデータ２３２は、図１０のオブジェクト数データ２２２と図１３のメタモデル２３１とに対応するオブジェクトデータである。
オブジェクトデータ２３２は、オペランド名とステレオタイプとオブジェクト数との組毎にレコード（行）を有する。
レコードは、オペランド名とステレオタイプとオブジェクト数とのそれぞれの欄を有する。
オペランド名の欄は、オペランドの名称を示す。
ステレオタイプの欄は、ステレオタイプを示す。
オブジェクト数の欄は、オブジェクト数を示す。
【００４８】
図１５に基づいて、時相論理式データ生成（Ｓ１３２）の手順を説明する。
ステップＳ１３２１において、オブジェクト記述生成部１３０は、オブジェクトモデルから未選択のオペランド名を１つ選択する。
ステップＳ１３２２において、オブジェクト記述生成部１３０は、選択されたオペランド名に対応付けられたオブジェクト数をオブジェクトモデルから取得し、取得されたオブジェクト数を判定する。
オブジェクト数が１である場合、処理はステップＳ１３２３に進む。
オブジェクト数が２以上である場合、処理はステップＳ１３２４に進む。
【００４９】
ステップＳ１３２３において、オブジェクト記述生成部１３０は、選択されたオペランド名を用いてオブジェクト記述を生成する。
具体的には、オブジェクト記述生成部１３０は、選択されたオペランド名に対応する１つのオブジェクト名を生成する。生成される１つのオブジェクト名がオブジェクト記述である。
【００５０】
ステップＳ１３２４において、オブジェクト記述生成部１３０は、選択されたオペランド名に対応する記述ルールを時相論理式パターンから取得する。
そして、オブジェクト記述生成部１３０は、取得された記述ルールに従ってオブジェクト記述を生成する。
【００５１】
具体的には、オブジェクト記述生成部１３０は以下のようにオブジェクト記述を生成する。
まず、オブジェクト記述生成部１３０は、選択されたオペランド名に対応する複数のオブジェクト名を生成する。オブジェクト名の数は、ステップＳ１３２２で取得されたオブジェクト数と同じ数である。
そして、オブジェクト記述生成部１３０は、複数のオブジェクト名を記述ルールが示す論理演算子を用いて接続する。これによって得られる文字列がオブジェクト記述である。
【００５２】
ステップＳ１３２５において、オブジェクト記述生成部１３０は、未選択のオペランド名が有るか判定する。
未選択のオペランド名が有る場合、処理はステップＳ１３２１に進む。
未選択のオペランド名が無い場合、処理はステップＳ１３２６に進む。
【００５３】
ステップＳ１３２６において、オブジェクト記述生成部１３０は、時相論理式パターンから時相論理式テンプレートを取得する。
そして、オブジェクト記述生成部１３０は、取得された時相論理式テンプレートと生成されたオブジェクト記述とを時相論理式データに登録する。
【００５４】
図１６に、時相論理式パターン２３３を示す。時相論理式パターン２３３は時相論理式パターンの具体例である。
時相論理式パターン２３３は、時相論理式テンプレートと記述ルールとのそれぞれの欄を有する。
時相論理式テンプレートの欄は、時相論理式テンプレートを示す。
記述ルールの欄は、時相論理式テンプレートに含まれるオペランド名毎に記述ルールを示す。記述ルールはオペランド名と論理演算子とを示す。記述ルールに示される論理演算子を用いてオペランド名に対応する複数のオブジェクト名を接続することによって得られる文字列がオブジェクト記述である。
【００５５】
図１７に、時相論理式データ２３４を示す。時相論理式データ２３４は、図１４のオブジェクトデータ２３２と図１６の時相論理式パターン２３３とに対応する時相論理式データである。
時相論理式データ２３４は、時相論理式テンプレートとＳｅｎｄオペランドとＲｅｃｅｉｖオペランドとのそれぞれの欄を有する。
時相論理式テンプレートの欄は、時相論理式パターン２３３に含まれる時相論理式テンプレートを示す。
Ｓｅｎｄオペランドの欄は、時相論理式テンプレートに含まれるＳｅｎｄオペランドに対応するオブジェクト記述を示す。オブジェクト記述において、Ｓｅｎｄ１とＳｅｎｄ２との２つのオブジェクト名が論理和演算子（｜｜）で接続されている。
Ｒｅｃｅｉｖｅオペランドの欄は、時相論理式テンプレートに含まれるＲｅｃｅｉｖｅオペランドに対応するオブジェクト記述を示す。オブジェクト記述において、Ｒｅｃｅｉｖｅ１とＲｅｃｅｉｖｅ２とＲｅｃｅｉｖｅ３とＲｅｃｅｉｖｅ４との４つのオブジェクト名が論理和演算子（｜｜）で接続されている。
【００５６】
＊＊＊実施の形態１の効果＊＊＊
時相論理式生成装置１００は、時相論理式の中に記載されるオブジェクト記述を生成することができる。例えば、時相論理式生成装置１００は、検査対象が変更されたときにオブジェクト記述を生成することができる。
そして、利用者は、生成されるオブジェクト記述を用いることによって、検査対象が変更された場合の時相論理式を生成することができる。
これにより、検査対象が変更されたときに時相論理式を生成するための工数が削減される。
【００５７】
実施の形態２．
任意の時相論理式パターンを使用するための形態について、主に実施の形態１と異なる点を図１８に基づいて説明する。
【００５８】
＊＊＊構成の説明＊＊＊
時相論理式生成装置１００の構成は、実施の形態１で説明した構成（図１参照）と同じである。
【００５９】
＊＊＊動作の説明＊＊＊
図１８に基づいて、時相論理式生成方法を説明する。
図１８に示す時相論理式生成方法は、実施の形態１（図２参照）で説明したステップに加えて、ステップＳ１０２を有する。
【００６０】
ステップＳ１０２において、利用者は、入力装置を操作して、時相論理式生成装置１００に時相論理式パターンを入力する。
受付部１９２は入力された時相論理式パターンを受け付け、記憶部１９１は受け付けられた時相論理式パターンを記憶する。
以降のステップＳ１３０では、ステップＳ１０２で受け付けられた時相論理式パターンが使用される。
【００６１】
＊＊＊実施の形態２の効果＊＊＊
時相論理式生成装置１００は、任意の時相論理式パターンを受け付けて受け付けた時相論理式パターンを使用することができる。例えば、時相論理式生成装置１００は、検査対象が変更されたときに検査対象の変更に合った時相論理式パターンを受け付けて受け付けた時相論理式パターンを使用することができる。
【００６２】
実施の形態３．
時相論理式を自動で生成するための形態について、主に実施の形態１と異なる点を図１９から図２１に基づいて説明する。
【００６３】
＊＊＊構成の説明＊＊＊
図１９に基づいて、時相論理式生成装置１００の構成を説明する。
時相論理式生成装置１００は、クラス図変換部１１０とオブジェクト数算出部１２０とオブジェクト記述生成部１３０との他に、時相論理式生成部１４０をソフトウェア要素として備える。
時相論理式生成プログラムは、クラス図変換部１１０とオブジェクト数算出部１２０とオブジェクト記述生成部１３０と時相論理式生成部１４０としてコンピュータを機能させるためのプログラムである。
【００６４】
＊＊＊動作の説明＊＊＊
図２０に基づいて、時相論理式生成方法を説明する。
ステップＳ１０１からステップＳ１３０は、実施の形態１（図２参照）で説明した通りである。
ステップＳ１３０の後、処理はステップＳ１５０に進む。
【００６５】
ステップＳ１５０において、時相論理式生成部１４０は、ステップＳ１３０で生成されたステレオタイプ毎のオブジェクト記述を用いて、時相論理式を生成する。記憶部１９１は、生成された時相論理式を記憶する。
【００６６】
図２１に基づいて、オブジェクト記述生成処理（Ｓ１５０）を説明する。
ステップＳ１５１において、時相論理式生成部１４０は、時相論理式データから時相論理式テンプレートを取得する。
ステップＳ１５２において、時相論理式生成部１４０は、取得された時相論理式テンプレートから未選択のオペランド名を１つ選択する。
ステップＳ１５３において、時相論理式生成部１４０は、選択されたオペランド名に対応するオブジェクト記述を時相論理式データから取得する。
ステップＳ１５４において、時相論理式生成部１４０は、取得された時相論理式テンプレートの中の選択されたオペランド名を、取得されたオブジェクト記述に置き換える。
ステップＳ１５５において、時相論理式生成部１４０は、未選択のオペランド名が有るか判定する。
未選択のオペランド名が有る場合、処理はステップＳ１５２に進む。
未選択のオペランド名が無い場合、オブジェクト記述生成処理（Ｓ１５０）は終了する。
【００６７】
図１７の時相論理式データ２３４に対応する時相論理式は、［］（Ｓｅｎｄ１  ｜｜  Ｓｅｎｄ２  −＞  ＜＞  Ｒｅｃｅｉｖｅ１  ｜｜  Ｒｅｃｅｉｖｅ２  ｜｜  Ｒｅｃｅｉｖｅ３  ｜｜  Ｒｅｃｅｉｖｅ４）である。
【００６８】
＊＊＊実施の形態３の効果＊＊＊
時相論理式生成装置１００は、時相論理式を自動で生成することができる。
これにより、検査対象が変更されたときに時相論理式を生成するための工数がさらに削減される。
【００６９】
＊＊＊他の構成＊＊＊
時相論理式生成装置１００は、実施の形態２と同じく、任意の時相論理式パターンを受け付けて受け付けた時相論理式パターンを使用してもよい。
【００７０】
＊＊＊実施の形態の補足＊＊＊
実施の形態において、時相論理式生成装置１００の機能はハードウェアで実現してもよい。
図２２に、時相論理式生成装置１００の機能がハードウェアで実現される場合の構成を示す。
時相論理式生成装置１００は処理回路９９０を備える。処理回路９９０はプロセッシングサーキットリともいう。
処理回路９９０は、クラス図変換部１１０とオブジェクト数算出部１２０とオブジェクト記述生成部１３０と時相論理式生成部１４０と記憶部１９１とを実現する専用の電子回路である。
例えば、処理回路９９０は、単一回路、複合回路、プログラム化したプロセッサ、並列プログラム化したプロセッサ、ロジックＩＣ、ＧＡ、ＡＳＩＣ、ＦＰＧＡまたはこれらの組み合わせである。ＧＡはＧａｔｅ  Ａｒｒａｙの略称であり、ＡＳＩＣはＡｐｐｌｉｃａｔｉｏｎ  Ｓｐｅｃｉｆｉｃ  Ｉｎｔｅｇｒａｔｅｄ  Ｃｉｒｃｕｉｔの略称であり、ＦＰＧＡはＦｉｅｌｄ  Ｐｒｏｇｒａｍｍａｂｌｅ  Ｇａｔｅ  Ａｒｒａｙの略称である。
【００７１】
時相論理式生成装置１００は、処理回路９９０を代替する複数の処理回路を備えてもよい。複数の処理回路は、処理回路９９０の役割を分担する。
【００７２】
実施の形態は、好ましい形態の例示であり、本発明の技術的範囲を制限することを意図するものではない。実施の形態は、部分的に実施してもよいし、他の形態と組み合わせて実施してもよい。フローチャート等を用いて説明した手順は、適宜に変更してもよい。
【符号の説明】
【００７３】
１００  時相論理式生成装置、１１０  クラス図変換部、１２０  オブジェクト数算出部、１３０  オブジェクト記述生成部、１４０  時相論理式生成部、１９１  記憶部、１９２  受付部、１９３  表示部、２００  クラス図、２１０  クラス図情報データ、２２１  クラス情報データ、２２２  オブジェクト数データ、２３１  メタモデル、２３２  オブジェクトデータ、２３３  時相論理式パターン、２３４  時相論理式データ、９０１  プロセッサ、９０２  メモリ、９０３  補助記憶装置、９０４  入出力インタフェース、９９０  処理回路。
【図１】
2018147187.tif 000003
【図２】
2018147187.tif 000004
【図３】
2018147187.tif 000005
【図４】
2018147187.tif 000006
【図５】
2018147187.tif 000007
【図６】
2018147187.tif 000008
【図７】
2018147187.tif 000009
【図８】
2018147187.tif 000010
【図９】
2018147187.tif 000011
【図１０】
2018147187.tif 000012
【図１１】
2018147187.tif 000013
【図１２】
2018147187.tif 000014
【図１３】
2018147187.tif 000015
【図１４】
2018147187.tif 000016
【図１５】
2018147187.tif 000017
【図１６】
2018147187.tif 000018
【図１７】
2018147187.tif 000019
【図１８】
2018147187.tif 000020
【図１９】
2018147187.tif 000021
【図２０】
2018147187.tif 000022
【図２１】
2018147187.tif 000023
【図２２】
2018147187.tif 000024