(57)【要約】【課題】容易に適切なモデル検査を行うことができるタイミングチャート生成装置、及びプログラムを提供すること。【解決手段】タイミングチャート生成装置は、モデル検査対象の信号の制約を示す制約定義表を生成する制約定義表生成部と、前記制約定義表生成部によって生成された前記制約定義表と、モデル検査対象の仕様情報とに基づいて、前記仕様情報に示される前記モデル検査対象の信号と、前記制約定義表に含まれる前記制約とを互いに対応付けた信号制約定義表を生成する信号制約定義表生成部と、前記信号制約定義表生成部によって生成された前記信号制約定義表に含まれる前記制約を示す制約タイミングチャートを前記信号毎に生成する制約タイミングチャート生成部と、前記制約タイミングチャート生成部によって生成された前記制約タイミングチャートを表示部に表示させる表示制御部とを備える。【選択図】図１
2020170483.tif 000002
【特許請求の範囲】
【請求項１】
モデル検査対象の信号の制約を示す制約定義表を生成する制約定義表生成部と、
前記制約定義表生成部によって生成された前記制約定義表と、モデル検査対象の仕様情報とに基づいて、前記仕様情報に示される前記モデル検査対象の信号と、前記制約定義表に含まれる前記制約とを互いに対応付けた信号制約定義表を生成する信号制約定義表生成部と、
前記信号制約定義表生成部によって生成された前記信号制約定義表に含まれる前記制約を示す制約タイミングチャートを前記信号毎に生成する制約タイミングチャート生成部と、
前記制約タイミングチャート生成部によって生成された前記制約タイミングチャートを表示部に表示させる表示制御部と、
を備えるタイミングチャート生成装置。
【請求項２】
前記制約タイミングチャート生成部は、更に、前記制約定義表生成部によって生成された前記制約定義表に含まれる制約を示す信号間制約タイミングチャートを生成する、
請求項１に記載のタイミングチャート生成装置。
【請求項３】
ユーザの入力を受け付ける受付部を更に備え、
前記信号制約定義表生成部は、前記受付部によって受け付けられたユーザの入力に基づいて、前記信号と、前記制約とを互いに対応付けて前記信号制約定義表を生成する
請求項１又は請求項２に記載のタイミングチャート生成装置。
【請求項４】
前記モデル検査対象に係る情報と信号制約定義表とに基づいて、前記モデル検査対象のモデルを生成するモデル生成部と、
前記モデル生成部によって生成された前記モデルと、とに基づいて、モデル検査を実行するモデル検査実行部と、
前記モデル検査実行部の実行結果に基づいて、実行結果のタイミングチャートを生成する実行結果タイミングチャート生成部とを更に備え、
前記表示制御部は、前記実行結果タイミングチャート生成部によって生成された前記実行結果のタイミングチャートを表示部に表示させる、
請求項１から請求項３のうちいずれか一項に記載のタイミングチャート生成装置。
【請求項５】
前記実行結果タイミングチャート生成部は、信号種別と、前記実行結果のタイミングチャートにおける信号の表記方と、実行結果における表記とが互いに対応付けられた生成規則情報に基づいて、タイミングチャートの生成対象信号の実行結果と対応する前記表記方を選択することにより、前記実行結果のタイミングチャートを生成する、
請求項４に記載のタイミングチャート生成装置。
【請求項６】
モデル検査対象の信号の制約を示す制約定義表を生成する制約定義表生成ステップと、
前記制約定義表生成ステップによって生成された前記制約定義表と、モデル検査対象の仕様情報とに基づいて、前記仕様情報に示される前記モデル検査対象の信号と、前記制約定義表に含まれる前記制約とを互いに対応付けた信号制約定義表を生成する信号制約定義表生成ステップと、
前記信号制約定義表生成ステップによって生成された前記信号制約定義表に含まれる前記制約を示すタイミングチャートを前記信号毎に生成する制約タイミングチャート生成ステップと、
前記制約タイミングチャート生成ステップによって生成された前記タイミングチャートを表示ステップに表示させる表示制御ステップと、
をコンピュータに実行させるためのプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、タイミングチャート生成装置、及びプログラムに関する。
【背景技術】
【０００２】
従来、モデル検査の対象項目のうち、検査条件に合致する対象項目について、モデル検査を行うことにより、状態爆発の発生を低減する技術が知られている（例えば、特許文献１）。
【先行技術文献】
【特許文献】
【０００３】
【特許文献１】特開２０１０−１４００８４号公報
【発明の概要】
【発明が解決しようとする課題】
【０００４】
しかしながら、従来の技術では、モデル検査の検査用モデルコードを解読することができない習熟度の低いユーザは、検査条件を設定し、適切な対象項目を抽出することが容易ではなかった。
【０００５】
本発明は、このような事情を考慮してなされたものであり、容易に適切なモデル検査を行うことができるタイミングチャート生成装置、及びプログラムを提供することを目的の一つとする。
【課題を解決するための手段】
【０００６】
本発明の一態様は、モデル検査対象の信号の制約を示す制約定義表を生成する制約定義表生成部と、前記制約定義表生成部によって生成された前記制約定義表と、モデル検査対象の仕様情報とに基づいて、前記仕様情報に示される前記モデル検査対象の信号と、前記制約定義表に含まれる前記制約とを互いに対応付けた信号制約定義表を生成する信号制約定義表生成部と、前記信号制約定義表生成部によって生成された前記信号制約定義表に含まれる前記制約を示す制約タイミングチャートを前記信号毎に生成する制約タイミングチャート生成部と、前記制約タイミングチャート生成部によって生成された前記制約タイミングチャートを表示部に表示させる表示制御部とを備えるタイミングチャート生成装置である。
【発明の効果】
【０００７】
本発明によれば、容易に適切なモデル検査を行うことができる。
【図面の簡単な説明】
【０００８】
【図１】本実施形態に係るタイミングチャート生成装置１００の構成の一例を示す図である。
【図２】制約定義表を生成する処理において、表示部ＤＰに表示される画像６０１の一例を示す図である。
【図３】制約Ｎｏ．１〜４ｃのタイミングチャートを示す画像６０２の一例を示す図である。
【図４】制約Ｎｏ．５〜１０のタイミングチャートを示す画像６０３の一例を示す図である。
【図５】信号制約定義表生成部１１６が信号制約定義表を生成する処理において、表示部ＤＰに表示される画像６０４の一例を示す図である。
【図６】信号制約のタイミングチャートを示す画像６０５の一例を示す図である。
【図７】モデル検査の実行結果の一例を示す図である。
【図８】生成規則情報１３８の内容の一例を示す図である。
【図９】実行結果タイミングチャート生成部１１９によって生成されたタイミングチャートを示す画像６０６の一例を示す図である。
【図１０】タイミングチャート生成装置１００の処理の一連の流れを示すフローチャートである。
【発明を実施するための形態】
【０００９】
［実施形態］
以下、図を参照して本発明の実施形態について説明する。
【００１０】
図１は、本実施形態に係るタイミングチャート生成装置１００の構成の一例を示す図である。タイミングチャート生成装置１００は、（工程１）モデル検査の対象である回路、及びソフトウェア（以下、モデル検査対象）の仕様情報から、モデル検査に用いる検査用モデルコードを導出し、（工程２）検査用モデルコードを実行して得られるモデル検査実行結果に基づいて、タイミングチャートを生成する。モデル検査は、システムの網羅的な検査（テスト）を実現する技術である。具体的には、モデル検査は、システムを有限個の状態を持つモデルで表現し、システムが満たすべき性質がモデル上で成り立つかどうかを、モデルが取り得る全ての状態およびパスにおいて、網羅的に検査する技術である。
【００１１】
タイミングチャート生成装置１００には、例えば、操作部ＣＴと、表示部ＤＰとが接続される。操作部ＣＴは、ユーザからの操作入力を受け付けるキーボード、タッチパッド、マウス等の入力装置である。表示部ＤＰは、例えば、液晶ディスプレイパネル、プラズマディスプレイパネル、有機ＥＬ（Electro Luminescence）ディスプレイパネル等の表示装置である。なお、操作部ＣＴと、表示部ＤＰとは、一体に構成されたタッチパネルによって実現されてもよい。
【００１２】
タイミングチャート生成装置１００は、例えば、制御部１１０と、記憶部１３０とを備える。制御部１１０は、例えば、ＣＰＵ（Central Processing Unit）等のハードウェアプロセッサが記憶部１３０に記憶されるプログラム（ソフトウェア）を実行することにより、取得部１１１と、受付部１１２と、表示制御部１１３と、制約定義表生成部１１４と、制約タイミングチャート生成部１１５と、信号制約定義表生成部１１６と、モデル検査記述言語生成部１１７と、モデル検査記述言語生成部１１７と、モデル検査実行部１１８と、実行結果タイミングチャート生成部１１９とを機能部として実現する。また、これらの構成要素のうち一部又は全部は、ＬＳＩ（Large Scale Integration）やＡＳＩＣ（Application Specific Integrated Circuit）、ＦＰＧＡ（Field-Programmable Gate Array）、ＧＰＵ（Graphics Processing Unit）等のハードウェア（回路部；circuitryを含む）によって実現されてもよいし、ソフトウェアとハードウェアの協働によって実現されてもよい。
【００１３】
記憶部１３０は、例えば、ＲＡＭ（Random Access Memory）、ＲＯＭ（Read Only Memory）、ＨＤＤ（Hard Disk Drive）、フラッシュメモリ、又はこれらのうち複数が組み合わされたハイブリッド型記憶装置等により実現される。また、記憶部１３０の一部又は全部は、ＮＡＳ（Network Attached Storage）や外部のストレージサーバ等、タイミングチャート生成装置１００のアクセス可能な外部装置であってもよい。記憶部１３０には、検査式情報１３１と、回路ブロック図情報１３２、ステートチャート情報１３４、フローチャート情報１３６、及び生成規則情報１３８やプログラムが格納される。検査式情報１３１は、モデル検査対象が満たすべき性質を示した検査式の情報である。回路ブロック図情報１３２は、モデル検査対象の回路ブロック図を示す情報である。ステートチャート情報１３４は、モデル検査対象の状態遷移図を示す情報である。フローチャート情報１３６は、モデル検査対象のフローチャートを示す情報である。生成規則情報１３８の詳細については、後述する。
【００１４】
取得部１１１は、例えば、他の装置からネットワークを介して仕様情報を取得する。ネットワークは、例えば、インターネット、セルラー網、Ｗｉ−Ｆｉ網、ＷＡＮ（Wide Area Network）、ＬＡＮ（Local Area Network）等である。仕様情報は、例えば、（工程１）におけるモデル検査対象に係る仕様を示す情報であり、例えば、モデル検査対象において用いられる信号の情報や、処理速度（クロック周波数）等を示す情報である。なお、取得部１１１は、ＳＤカード等の着脱可能な記憶媒体がタイミングチャート生成装置１００のドライブ装置に装着されることに伴い、記憶媒体に格納された仕様情報を取得してもよい。
【００１５】
受付部１１２は、ユーザが操作部ＣＴに行った入力操作を受け付ける。表示制御部１１３は、表示部ＤＰを制御し、表示部ＤＰに各種情報を表示させる。
【００１６】
制約定義表生成部１１４は、受付部１１２によって受け付けられた入力操作に基づいて、制約定義表を生成する。図２は、制約定義表を生成する処理において、表示部ＤＰに表示される画像６０１の一例を示す図である。表示制御部１１３は、例えば、制約定義表を生成する処理において、制約定義表生成部１１４の指示に基づいて、画像６０１を生成し、表示部ＤＰに表示させる。
【００１７】
画像６０１には、例えば、制約定義表を示す領域と、作業ウインドウの領域とが含まれる。制約定義表には、例えば、モデル検査対象の動作の制約を識別可能な情報（以下、制約Ｎｏ．）と、制約に係るモデル検査対象の動作（制御）内容と、当該制約に係る基準信号と、基準信号に対応して変化する従属信号とについて、所定のクロック（図示では、１４クロック）間の当該制約に係る基準信号の状態遷移、又は従属信号の状態遷移を示す情報（以下、タイムスロット）が、制約毎に互いに対応付けられたレコードが含まれる。制約は、モデル検査対象における各種信号に課される条件である。すなわち、制約は、実際の動作における各種信号間の正しい動作を定義したものである。
【００１８】
なお、この一例において、制約定義表のタイムスロットは、１４クロック分であるが、制御内容に示される制約を表現するに際して、１４クロックでは制約を表現できない場合、制約定義表のタイムスロットは、１４クロックより多いクロック数であってもよく、１４クロックよりも少ないクロックによって制約を表現できる場合、制約定義表のタイムスロットは、１４クロックより少ないクロック数であってもよい。
【００１９】
制御内容には、例えば、基準信号の状態遷移と、基準信号の状態遷移に応じた従属信号の状態遷移の制約が含まれる。図２の制約定義表には、制約Ｎｏ．１〜１０の１６個の制約が含まれており、例えば、制約Ｎｏ．１の制御内容は、「基準信号のアサート期間中は、従属信号がアサートでなければならない」ことである。ユーザは、例えば、マウスやキーボード等の操作部ＣＴを操作して、カーソルＣＳを操作し、画像６０１として示される制約定義表の制約Ｎｏ．と制御内容のセルに情報を入力する。
【００２０】
タイムスロットには、所定のクロック間の制約に基づく基準信号の状態遷移、及び従属信号の状態遷移が、「０」、又は「１」の値等で表現される。例えば、制約Ｎｏ．１の基準信号の状態遷移は、１４クロックのうち、１〜２クロックはネゲートであり、３〜５クロックはアサートであり、６〜１４クロックはネゲートである。また、制約Ｎｏ．１の従属信号の状態遷移は、制約内容の通り、基準信号のアサート期間中は、アサートされるため、４クロックのうち、１〜２クロックはネゲートであり、３〜５クロックはアサートであり、６〜１４クロックはネゲートである。ユーザは、例えば、マウスやキーボード等の操作部ＣＴを操作して、画像６０１として示される制約定義表のタイムスロットのセルに情報を入力する。
【００２１】
また、タイムスロットのセルは、当該セルに入力される値が、クロックの立ち上がり、或いは立下りに応じて変化するものである場合、網掛けにされる。ユーザは、例えば、マウス等の操作部ＣＴを操作して、画像６０１として示される制約定義表のタイムスロットのセルをクリックし、セルの網掛けの設定、或いは解除を行う。
【００２２】
作業ウインドウには、モデル検査対象の制約を示す際に用いられる複数のオブジェクト画像ＯＪ（図示するオブジェクト画像ＯＪａ〜ＯＪｃ）が含まれる。オブジェクト画像ＯＪａは、矢印の始点が、基準信号が従属信号に影響を与える状態遷移の遷移期間を示し、矢印の終点が、従属信号が基準信号に影響を与えられた状態遷移の遷移期間を示す。また、オブジェクト画像ＯＪｂは、矢印の始点、及び終点が基準信号のタイムスロットに存在する場合、制約で定められた基準信号のアサート／ネゲート期間の幅を示し、矢印の始点、及び終点が従属信号のタイムスロットに存在する場合、制約で定められた従属信号のアサート／ネゲート期間の幅を示し、矢印の始点が基準信号のタイムスロットに存在し、矢印の終点が従属信号のタイムスロットに存在する場合、矢印の始点が、基準信号が従属信号に与える状態遷移のタイミングを示し、矢印の終点が、従属信号が基準信号に影響を与えられた状態遷移のタイミングを示す。なお、制約で定められた基準信号のアサート／ネゲート期間の幅は、オブジェクト画像ＯＪｃによって示されてもよい。ユーザは、マウス等の操作部ＣＴを操作して、画像６０１として示される制約定義表のタイムスロットのセル上に、オブジェクト画像ＯＪａ〜ＯＪｃを配置する。
【００２３】
制約定義表生成部１１４は、ユーザが画像６０１に示される制約定義表に入力した各種情報と、タイムスロットのセル上に配置したオブジェクト画像ＯＪに基づいて、制約定義表を生成する。なお、上述では、制約定義表生成部１１４がモデル検査対象について制約定義表を生成する場合について説明したが、これに限られない。制約定義表生成部１１４は、特定のモデル検査対象に限らず、一般的な信号の制約条件に係る制約定義表を生成するものであってもよい。
【００２４】
図１に戻り、制約タイミングチャート生成部１１５は、制約定義表生成部１１４によって生成された制約定義表を示す情報に基づいて、制約定義表に示される制約をタイミングチャート（以下、信号間制約タイミングチャートと記載する。）に変換する。図３は、制約Ｎｏ．１〜４ｃのタイミングチャートを示す画像６０２の一例を示す図である。図４は、制約Ｎｏ．５〜１０のタイミングチャートを示す画像６０３の一例を示す図である。制約タイミングチャート生成部１１５は、制約定義表のタイムスロットに示される「０」、又は「１」の値に基づいて、制約を示す波形を生成する。また、制約タイミングチャート生成部１１５は、制約定義表のタイムスロットのセル上に配置されたオブジェクト画像ＯＪａ〜ＯＪｃに基づいて、信号の状態を示す図形（図示する図形ＩＭａ〜ＩＭｆ）を、制約を示す波形に配置する。
【００２５】
図形ＩＭａ１〜ＩＭａ１０は、オブジェクト画像ＯＪｂの矢印の始点によって示されるタイミングであり、基準信号が従属信号に与える状態遷移のタイミングにおける基準信号の状態（「０」、又は「１」）を示す図形である。図形ＩＭｂ１〜ＩＭｂ１５は、オブジェクト画像ＯＪｂと同様に、矢印の始点が、基準信号が従属信号に与える状態遷移のタイミングを示し、矢印の終点が、従属信号が基準信号に影響を与えられた状態遷移のタイミングを示す。図形ＩＭｃ１〜ＩＭｃ３は、オブジェクト画像ＯＪｂの矢印の始点によって示されるタイミングであり、基準信号が従属信号に与える状態遷移のタイミングにおける基準信号の立ち上がり、或いは立下りの状態（「０」、又は「１」）を示す図形である。図形ＩＭｄ１〜ＩＭｄ６は、オブジェクト画像ＯＪｂと同様に、制約で定められた基準信号のアサート／ネゲート期間の幅、又は制約で定められた従属信号のアサート／ネゲート期間の幅を示す図形である。図形ＩＭｅ１〜ＩＭｅ６は、制約で定められたクロック数を示すコメントを示す図形である。図形ＩＭｆ１〜ＩＭｆ４は、基本信号のアサート期間中の期間を示す図形、又は基本信号がアサート期間中であることに応じて、従属信号（２値、或いはデータを示す信号）が有効である期間を示す図形である。
【００２６】
制約タイミングチャート生成部１１５は、例えば、制約定義表に基づいて制約を示す信号間制約タイミングチャートを生成し、表示制御部１１３は、制約タイミングチャート生成部１１５が生成した信号間制約タイミングチャートを示す画像（この一例では、画像６０２、及び画像６０３）を表示部ＤＰに表示させる。これにより、ユーザは、制約を適切に設定することができたか否かを視覚的に確認することができる。
【００２７】
次に、信号制約定義表生成部１１６は、取得部１１１によって取得された仕様情報と、制約定義表生成部１１４によって生成された制約定義表とに基づいて、仕様情報に含まれる各種信号と、制約定義表に示される制約との対応付けを行った信号制約定義表を生成する。図５は、信号制約定義表生成部１１６が信号制約定義表を生成する処理において、表示部ＤＰに表示される画像６０４の一例を示す図である。表示制御部１１３は、例えば、信号制約定義表を生成する処理において、信号制約定義表生成部１１６の指示に基づいて、画像６０４を生成し、表示部ＤＰに表示させる。
【００２８】
画像６０４には、例えば、信号制約定義表が示される。信号制約定義表は、制約Ｎｏ．と、信号名称と、タイムスロットとが、信号セット（基準信号、及び従属信号のセット）毎が互いに対応付けられたレコードが含まれる。信号名称は、仕様情報から取得され、信号制約定義表に転記される情報である。ユーザは、例えば、マウス等の操作部ＣＴを操作して、カーソルＣＳを操作し、画像６０４として示される信号制約定義表の制約Ｎｏ．のセルに、対応付けられた信号名称の制約として適当な制約の制約Ｎｏ．を入力する。信号制約定義表のタイムスロットには、制約Ｎｏ．が入力されることに応じて、制約定義表の対応する制約のタイムスロットの情報が転記される。信号制約定義表生成部１１６は、ユーザが画像６０４に示される信号制約定義表に入力した各種情報に基づいて、信号制約定義表を生成する。
【００２９】
図６は、信号制約のタイミングチャート（以下、制約タイミングチャートと記載する。）を示す画像６０５の一例を示す図である。制約タイミングチャート生成部１１５は、信号制約定義表のタイムスロットに示される「０」、又は「１」の値に基づいて、各信号の制約を示す波形を生成する。また、制約タイミングチャート生成部１１５は、信号制約定義表のタイムスロットのセル上に配置されたオブジェクト画像ＯＪａ〜ＯＪｃに基づいて、信号の状態を示す図形（図示する図形ＩＭａ〜ＩＭｆ）を、制約を示す波形に配置する。制約タイミングチャート生成部１１５が信号制約定義表に基づいて図６に示すようなフローチャートを生成する処理は、制約定義表に基づいて、図３〜４に示すようなフローチャートを生成する処理と同様であるため、説明を省略する。表示制御部１１３は、制約タイミングチャート生成部１１５が生成した制約タイミングチャートを示す画像（この一例では、画像６０５）を表示部ＤＰに表示させる。これにより、ユーザは、信号に制約を適切に設定（対応付け）することができたか否かを視覚的に確認することができる。
【００３０】
モデル検査記述言語生成部１１７は、既知の方法によって回路ブロック図情報１３２に示されるモデル検査対象の回路ブロック図、ステートチャート情報１３４に示されるモデル検査対象のステートチャート、及びフローチャート情報１３６に示されるモデル検査対象のフローチャートを、モデル検査が実施可能な態様にそれぞれ変換（つまり、モデル化）する。モデル検査記述言語生成部１１７は例えば、モデル検査対象を示す各種情報の特徴に応じたモデリングツールをそれぞれ用いてモデル検査対象をモデル化する。また、モデル検査記述言語生成部１１７は、信号制約定義表を用いて、各種モデル検査対象をモデル化する。モデル検査記述言語生成部１１７は、例えば、テキストフォーマットに基づいて、信号制約定義表に示される制約に対応する仕様記述言語パターンを制約毎に選択し、モデル化する。テキストフォーマットは、信号制約定義表に示される制約のうち、タイムスロットの特徴と、仕様記述言語パターンとを、タイムスロットの特徴毎に対応付けた情報である。
【００３１】
モデル検査実行部１１８は、モデル検査記述言語生成部１１７によって変換された各種モデルと、検査式情報１３１に示される検査式とに基づいて、モデル検査を実行する。モデル検査実行部１１８は、モデル検査の実行結果について出力する。図７は、モデル検査の実行結果の一例を示す図である。モデル検査の実行結果は、例えば、モデル検査対象の信号名称と、信号が初期状態から不具合に至るまでのタイムスロットとが互いに対応付けられたレコードが含まれる情報である。
【００３２】
実行結果タイミングチャート生成部１１９は、モデル検査実行部１１８によって出力された実行結果と、生成規則情報１３８とに基づいて、実行結果タイミングチャートを生成する。図８は、生成規則情報１３８の内容の一例を示す図である。生成規則情報１３８は、例えば、信号種別と、実行結果タイミングチャートにおける信号の表記方（図形）と、実行結果における表記とが互いに対応付けられたレコードが含まれる情報である。実行結果タイミングチャート生成部１１９は、例えば、実行結果に含まれるタイミングチャートの生成対象の信号について、当該生成対象の信号の信号名称に基づいて信号種別を特定し、特定した信号種別に対応付けられている図形のうち、当該生成対象の信号の実行結果と対応する実行結果の図形をタイムスロット毎に選択することにより、実行結果タイミングチャートの波形を生成する。図９は、実行結果タイミングチャート生成部１１９によって生成された実行結果タイミングチャートを示す画像６０６の一例を示す図である。実行結果タイミングチャート生成部１１９は、例えば、実行結果に基づいて実行結果タイミングチャートを生成し、表示制御部１１３は、実行結果タイミングチャート生成部１１９が生成した実行結果タイミングチャートを示す画像（この一例では、画像６０６）を表示部ＤＰに表示させる。これにより、ユーザは、モデル検査の実行結果を視覚的に確認することができる。
【００３３】
［動作フロー］
図１０は、タイミングチャート生成装置１００の処理の一連の流れを示すフローチャートである。制約定義表生成部１１４は、受付部１１２によって受け付けられた情報に基づいて、制約定義表を生成する（ステップＳ１００）。ここで、制約定義表生成部１１４は、制約定義表を生成する処理において表示制御部１１３を制御し、制約定義表の生成をユーザに促すような画像（この一例では、画像６０１）を表示部ＤＰに表示させる。取得部１１１は、仕様情報を取得する（ステップＳ１０２）。なお、仕様情報は、予め記憶部１３０に記憶されていてもよい。この場合、タイミングチャート生成装置１００は、取得部１１１を備えていなくてもよい。
【００３４】
信号制約定義表生成部１１６は、取得部１１１によって取得された仕様情報と、制約定義表生成部１１４によって生成された制約定義表とに基づいて、信号制約定義表を生成する（ステップＳ１０４）。ここで、信号制約定義表生成部１１６は、信号制約定義表を生成する処理において表示制御部１１３を制御し、信号制約定義表の生成をユーザに促すような画像（この一例では、画像６０４）を表示部ＤＰに表示させる。信号制約定義表生成部１１６は、ユーザが画像６０４に示される信号制約定義表に入力した各種情報に基づいて、様情報に含まれる各種信号と、制約定義表に示される制約との対応付けを行い、信号制約定義表を生成する。
【００３５】
制約タイミングチャート生成部１１５は、信号制約定義表生成部１１６によって生成された信号制約定義表に基づいて、制約タイミングチャートを生成する（ステップＳ１０６）。表示制御部１１３は、制約タイミングチャート生成部１１５によって生成された制約タイミングチャートを示す画像（この一例では、画像６０５）を表示部ＤＰに表示させ、ユーザは、表示された制約タイミングチャートを確認し、信号制約定義表が適切に生成されているか否かを判定する。受付部１１２は、操作部ＣＴに対してユーザから信号制約定義表が適切に生成されたことを示す操作が行われるまでの間、ステップＳ１０４〜Ｓ１０６の処理を繰り返す（ステップＳ１０８）。表示制御部１１３は、例えば、ステップＳ１０８において、操作部ＣＴに対して信号制約定義表が適切に生成されていないことを示す操作が行われた場合、信号制約定義表の生成をユーザに促すような画像（この一例では、画像６０１）を表示部ＤＰに表示させる。
【００３６】
モデル検査記述言語生成部１１７は、モデル検査対象に係る情報（この一例では、回路ブロック図情報１３２、ステートチャート情報１３４、及びフローチャート情報１３６）と、信号制約定義表を用いてモデルに変換する（ステップＳ１１０）。モデル検査記述言語生成部１１７は、例えば、これらの処理を、モデリングツールを用いて実行する。モデル検査実行部１１８は、モデル検査記述言語生成部１１７によって生成されたモデルと、検査式情報１３１に示される検査式とに基づいて、モデル検査を実行する（ステップＳ１１２）。モデル検査実行部１１８は、モデル検査の実行結果を出力する。
【００３７】
実行結果タイミングチャート生成部１１９は、モデル検査実行部１１８によって出力された実行結果と、生成規則情報１３８とに基づいて、実行結果タイミングチャートを生成する（ステップＳ１１４）。実行結果タイミングチャート生成部１１９は、例えば、実行結果に含まれる実行結果タイミングチャートの生成対象の信号について、当該生成対象の信号の信号名称に基づいて信号種別を特定し、特定した信号種別に対応付けられている図形のうち、当該生成対象の信号の実行結果と対応する実行結果の図形をタイムスロット毎に選択することにより、実行結果タイミングチャートの波形を生成する。表示制御部１１３は、実行結果タイミングチャート生成部１１９によって生成された実行結果タイミングチャートを表示部ＤＰに表示させる。
【００３８】
［実施形態のまとめ］
以上説明したように、本実施形態のタイミングチャート生成装置１００は、信号の動作の制約を示す制約定義表を生成する制約定義表生成部１１４と、制約定義表生成部１１４によって生成された制約定義表と、モデル検査対象の仕様情報とに基づいて、仕様情報に示されるモデル検査対象の信号と、制約定義表に含まれる制約とを互いに対応付けた信号制約定義表を生成する信号制約定義表生成部１１６と、信号制約定義表生成部１１６によって生成された信号制約定義表に含まれる制約を示す制約タイミングチャートを信号毎に生成する制約タイミングチャート生成部１１５によって生成された制約タイミングチャートを表示部に表示させる表示制御部１１３とを備え、モデル検査の検査用モデルコードを解読することなく、容易に制約を信号に対応付けることができるため、容易に適切なモデル検査を行うことができる。
【００３９】
また、本実施形態のタイミングチャート生成装置１００において、制約タイミングチャート生成部１１５は、更に、制約定義表生成部１１４によって生成された制約定義表に含まれる制約を示す制約タイミングチャートを生成する、制約タイミングチャート生成部１１５によって生成された制約タイミングチャートを示す画像（この一例では、画像６０２、画像６０３）を表示部ＤＰに表示することにより、ユーザに制約を適切に設定することができたか否かを視覚的に確認することを促すことができる。
【００４０】
また、本実施形態のタイミングチャート生成装置１００は、ユーザの入力を受け付ける受付部１１２を更に備え、信号制約定義表生成部１１６は、受付部１１２によって受け付けられたユーザの入力に基づいて、信号と、制約とを互いに対応付けて信号制約定義表を生成するため、ユーザが所望する制約を信号に付すことができる。
【００４１】
また、本実施形態のタイミングチャート生成装置１００は、モデル検査対象に係る情報（この一例では、回路ブロック図情報１３２、ステートチャート情報１３４、及びフローチャート情報１３６）に基づいて、モデル検査対象のモデルを生成するモデル生成部（この一例では、モデル検査記述言語生成部１１７）と、モデル検査記述言語生成部１１７によって生成されたモデルと、とに基づいて、モデル検査を実行するモデル検査実行部１１８と、モデル検査実行部１１８の実行結果に基づいて、実行結果タイミングチャートを生成する実行結果タイミングチャート生成部とを更に備え、表示制御部１１３は、実行結果タイミングチャート生成部１１９によって生成された実行結果タイミングチャートを表示部ＤＰに表示させることにより、ユーザにモデル検査の実行結果を視覚的に確認させることができる。
【００４２】
以上、本発明を実施するための形態について実施形態を用いて説明したが、本発明はこうした実施形態に何等限定されるものではなく、本発明の要旨を逸脱しない範囲内において種々の変形及び置換を加えることができる。
【符号の説明】
【００４３】
１００…タイミングチャート生成装置、１０８…ステップ、１１０…制御部、１１１…取得部、１１２…受付部、１１３…表示制御部、１１４…制約定義表生成部、１１５…制約タイミングチャート生成部、１１６…信号制約定義表生成部、１１７…モデル検査記述言語生成部、１１８…モデル検査実行部、１１９…実行結果タイミングチャート生成部、１３０…記憶部、１３１…検査式情報、１３２…回路ブロック図情報、１３４…ステートチャート情報、１３６…フローチャート情報、１３８…生成規則情報
【図１】
2020170483.tif 000003
【図２】
2020170483.tif 000004
【図３】
2020170483.tif 000005
【図４】
2020170483.tif 000006
【図５】
2020170483.tif 000007
【図６】
2020170483.tif 000008
【図７】
2020170483.tif 000009
【図８】
2020170483.tif 000010
【図９】
2020170483.tif 000011
【図１０】
2020170483.tif 000012