(57)【要約】【課題】表示調停制御の仕様化を意図通りに行えているか否かを適切に評価する。【解決手段】表示調停制御の評価装置１は、表示調停制御をモデル化し、コンテンツを定義するコンテンツ定義と、表示エリアを定義するエリア定義と、コンテンツの表示に関する制約を示す制約式とが含まれるルールベース調停仕様モデルを生成するモデル生成部２と、ルールベース調停仕様モデルから製品に搭載される表示調停制御に関するソフトウェア用のルール定義ファイルを生成するルール定義ファイル生成部５ａと、ルールベース調停仕様モデルから網羅テストパターンを生成する網羅テストパターン生成部５ｂと、コンテンツと表示エリアとの組み合わせが制約式により示される制約を満たしているか否かを、網羅テストパターンを用いて自動でシミュレーションし、そのシミュレーション結果をテスト結果ログとして出力するシミュレーション部６と、を備える。【選択図】図１
2019192001.tif 000002
【特許請求の範囲】
【請求項１】
表示調停制御をモデル化し、コンテンツを定義するコンテンツ定義と、表示エリアを定義するエリア定義と、コンテンツの表示に関する制約を示す制約式とが含まれるルールベース調停仕様モデルを生成するモデル生成部（２）と、
前記ルールベース調停仕様モデルから製品に搭載される表示調停制御に関するソフトウェア用のルール定義ファイルを生成するルール定義ファイル生成部（５ａ）と、
前記ルールベース調停仕様モデルから網羅テストパターンを生成する網羅テストパターン生成部（５ｂ）と、
前記コンテンツ定義で定義されているコンテンツと前記エリア定義で定義されている表示エリアとの組み合わせが制約式により示される制約を満たしているか否かを、前記網羅テストパターンを用いて自動でシミュレーションし、そのシミュレーション結果をテスト結果ログとして出力するシミュレーション部（６）と、を備える表示調停制御の評価装置。
【請求項２】
前記シミュレーション部は、評価対象のモデルが新規モデルであれば、前記網羅テストパターンを新たに生成し、その新たに生成した前記網羅テストパターンを用いて自動でシミュレーションし、評価対象のモデルが新規モデルでなく仕様変更であれば、前記網羅テストパターンを新たに生成せずに、過去に生成した前記網羅テストパターンを用いて自動でシミュレーションする請求項１に記載した表示調停制御の評価装置。
【請求項３】
前記ルールベース調停仕様モデルにおける矛盾の有無を検証するモデル検証部（４）を備える請求項１又は２に記載した表示調停制御の評価装置。
【請求項４】
前記ルールベース調停仕様モデルから表示調停制御に関する仕様書を生成する仕様書生成部（３）を備える請求項１から３の何れか一項に記載した表示調停制御の評価装置。
【請求項５】
表示調停制御をモデル化し、コンテンツを定義するコンテンツ定義と、表示エリアを定義するエリア定義と、コンテンツの表示に関する制約を示す制約式とが含まれるルールベース調停仕様モデルを生成するモデル生成手順と、
前記ルールベース調停仕様モデルから製品に搭載される表示調停制御に関するソフトウェア用のルール定義ファイルを生成するルール定義ファイル生成手順と、
前記ルールベース調停仕様モデルから網羅テストパターンを生成する網羅テストパターン生成手順と、
前記コンテンツ定義で定義されているコンテンツと前記エリア定義で定義されている表示エリアとの組み合わせが制約式により示される制約を満たしているか否かを、前記網羅テストパターンを用いて自動でシミュレーションし、そのシミュレーション結果をテスト結果ログとして出力するシミュレーション手順と、を実行する表示調停制御の評価方法。
【請求項６】
前記シミュレーション手順は、評価対象のモデルが新規モデルであれば、前記網羅テストパターンを新たに生成し、その新たに生成した前記網羅テストパターンを用いて自動でシミュレーションし、評価対象のモデルが新規モデルでなく仕様変更であれば、前記網羅テストパターンを新たに生成せずに、過去に生成した前記網羅テストパターンを用いて自動でシミュレーションする請求項５に記載した表示調停制御の評価方法。
【請求項７】
前記ルールベース調停仕様モデルにおける矛盾の有無を検証するモデル検証手順を実行した後に、前記シミュレーション手順を実行する請求項５又は６に記載した表示調停制御の評価方法。
【請求項８】
表示調停制御をモデル化し、コンテンツを定義するコンテンツ定義と、表示エリアを定義するエリア定義と、コンテンツの表示に関する制約を示す制約式とが含まれるルールベース調停仕様モデルを生成するモデル生成部（２）と、
前記ルールベース調停仕様モデルから製品に搭載される表示調停制御に関するソフトウェア用のルール定義ファイルを生成するルール定義ファイル生成部（５ａ）と、を備えるルール定義ファイルの生成装置。
【請求項９】
表示調停制御をモデル化し、コンテンツを定義するコンテンツ定義と、表示エリアを定義するエリア定義と、コンテンツの表示に関する制約を示す制約式とが含まれるルールベース調停仕様モデルを生成するモデル生成手順と、
前記ルールベース調停仕様モデルから製品に搭載される表示調停制御に関するソフトウェア用のルール定義ファイルを生成するルール定義ファイル生成手順と、を実行するルール定義ファイルの生成方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、表示調停制御の評価装置、その評価方法、ルール定義ファイルの生成装置、その生成方法に関する。
【背景技術】
【０００２】
車両の室内で表示されるコンテンツは多岐にわたっている。この種のコンテンツとしては、例えば車速、エンジン回転数、シフトポジション、燃料の残量等の車両走行に直接的に関係する走行系のコンテンツや、ナビゲーション用の地図情報、エアコンの設定情報、オーディオ情報等の車両走行に直接的に関係しない非走行系のコンテンツが挙げられる。又、このように表示されるコンテンツの多様化に伴い、コンテンツを表示する表示装置も種々な種類が搭載される。この種の表示装置としては、例えばセンターコンソールに配置されているセンターディスプレイ、ヘッドアップディスプレイ、グラフィックメータ等が挙げられる。又、表示装置によっては異なる複数のコンテンツを複数の表示エリアに同時に表示可能である。このような事情から、どのコンテンツをどの表示装置のどの表示エリアに表示させるのかを調停する表示調停制御が重要となっている。
【０００３】
従来の手法では、表示調停制御の仕様をマトリックスや状態遷移を用いて定義し、表示調停制御の仕様化を意図通りに行えているか否かを評価していた。しかしながら、マトリックスや状態遷移を用いて定義する手法では、コンテンツの数が増加すると、その数の２乗に比例して仕様の複雑度が増加する。そのため、コンテンツの数が増加傾向にある近年では、そのコンテンツの数の増加に対応することが困難となり、表示調停制御の仕様化を意図通りに行えているか否かを適切に評価することが困難となる。その結果、コンテンツの表示調停制御を適切に行えなくなることが懸念される。
【０００４】
この点に対し、例えば特許文献１には、コンテンツと、そのコンテンツが有する情報価値とを対応付けてコンテンツ情報として管理すると共に、表示エリアの属性をエリア情報として管理し、コンテンツ情報とエリア情報とを用いてコンテンツと表示エリアとの最適な組み合わせを決定する手法が開示されている。
【先行技術文献】
【特許文献】
【０００５】
【特許文献１】特許第５７４２７９９号公報
【発明の概要】
【発明が解決しようとする課題】
【０００６】
特許文献１に開示されている手法では、表示調停制御のルールベースの仕様を定義することで、仕様の複雑度が増加することなくコンテンツの数の増加に対応した表示調停制御を行える。しかしながら、特許文献１に開示されている手法では、仕様の記述を簡略化することができる反面、具体的な表示調停制御の挙動を理解し難いという問題がある。又、ルール間に矛盾が有る仕様でも定義し得るので、その矛盾に気付き難いという問題もある。更に、仕様化を意図通りに行えているか否かを評価するには、実際に実機で動かして動作を確認するしかないので、仕様に不具合があったとしても当該不具合を修正するのはソフトウェア開発の終盤になってしまい、作業工数が増大するという問題もある。
【０００７】
本発明は、上記した事情に鑑みてなされたものであり、その目的は、上記した様々な問題を解決し、表示調停制御の仕様化を意図通りに行えているか否かを適切に評価することができる表示調停制御の評価装置、その評価方法、ルール定義ファイルの生成装置、その生成方法を提供することにある。
【課題を解決するための手段】
【０００８】
請求項１に記載した発明によれば、モデル生成部（２）は、表示調停制御をモデル化し、コンテンツを定義するコンテンツ定義と、表示エリアを定義するエリア定義と、コンテンツの表示に関する制約を示す制約式とが含まれるルールベース調停仕様モデルを生成する。ルール定義ファイル生成部（５ａ）は、ルールベース調停仕様モデルから製品に搭載される表示調停制御に関するソフトウェア用のルール定義ファイルを生成する。網羅テストパターン生成部（５ｂ）は、ルールベース調停仕様モデルから網羅テストパターンを生成する。シミュレーション部（６）は、コンテンツ定義で定義されているコンテンツとエリア定義で定義されている表示エリアとの組み合わせが制約式により示される制約を満たしているか否かを、網羅テストパターンを用いて自動でシミュレーションし、そのシミュレーション結果をテスト結果ログとして出力する。
【０００９】
即ち、表示調停制御をモデル化し、ルールベース調停仕様モデルを生成し、コンテンツと表示エリアとの組み合わせが制約式により示される制約を満たしているか否かを、網羅テストパターンを用いて自動でシミュレーションし、そのシミュレーション結果をテスト結果ログとして出力する。シミュレーションによるテスト結果ログを解析することで、具体的な表示調停制御の挙動を理解し易くなる。又、調停結果が満たすべき条件を制約式で記述することで、ルール間に矛盾が無い仕様だけを定義することができ、ルール間に矛盾が有る仕様を除外することができる。更に、テスト結果ログによる評価を、表示調停制御に関するソフトウェアが製品に搭載される前に実施することで、仮に仕様に不具合があったとしても当該不具合をソフトウェア開発の初期の段階で修正することができ、作業工数の増大を未然に回避することができる。これにより、表示調停制御の仕様化を意図通りに行えているか否かを適切に評価することができる。
【図面の簡単な説明】
【００１０】
【図１】一実施形態のツール構成を示す図
【図２】サンプルモデルを示す図
【図３】フローチャート
【図４】モデル検証を示す図
【発明を実施するための形態】
【００１１】
以下、本発明の一実施形態について図面を参照して説明する。図１に示すように、表示調停制御の評価装置１は、製品に搭載されるソフトウェアを開発する環境の一部であり、モデルエディタ２（モデル生成部に相当する）と、仕様書生成ツール３（仕様書生成部に相当する）と、モデル検証ツール４（モデル検証部に相当する）と、コード生成ツール５と、ＰＣシミュレータ６（シミュレーション部に相当する）とを有する。表示調停制御の評価装置１は、ＣＰＵ（Central Processing Unit）、ＲＯＭ（Read Only Memory）、ＲＡＭ（Random Access Memory）、Ｉ／Ｏ（Input／Output）等を含むマイクロコンピュータを有し、非遷移的実体的記憶媒体に格納されているプログラムを実行することで、ルールベース調停（以下、ＲＢＡ：Rule Based Arbitration）仕様モデルの生成、仕様書の生成、検証結果の出力、ルール定義ファイル及び網羅テストパターンの生成等を行う。エディタ２、各ツール３〜５、ＰＣシミュレータ６は、プログラムのモジュールにより構成される。
【００１２】
モデルエディタ２は、ＲＢＡメタモデル（ＥＭＦ（Eclipse Modeling Framework）モデル）を用いて表示調停制御をモデル化し、ＲＢＡ仕様モデルを生成する。表示調停制御の評価装置１は、モデルエディタ２により生成したＲＢＡ仕様モデルを中心とし、仕様書の生成、モデルの検証、コードの生成を行う。
【００１３】
仕様書生成ツール３は、ＲＢＡ仕様モデルを用いて仕様書を生成する。ＲＢＡ仕様モデルは機械が解読するためのものであり、仕様書は作業者が解読するためのものである。
【００１４】
モデル検証ツール４は、ＲＢＡ仕様モデルのルール間の矛盾の有無を検証し、その検証結果を出力する。モデル検証ツール４は、ＲＢＡ仕様モデルのルール間に矛盾が無いと判定すると、表示調停制御を適切に行える旨を検証結果として出力し、ＲＢＡ仕様モデルのルール間に矛盾が有ると判定すると、表示調停制御を適切に行えない旨を検証結果として出力する。
【００１５】
コード生成ツール５は、ルール定義ファイル生成部５ａと、網羅テストパターン生成部５ｂとを有する。ルール定義ファイル生成部５ａは、ＲＢＡ仕様モデルを用いて製品に搭載されるソフトウェア用のルール定義ファイルを生成し、その生成したルール定義ファイルを出力する。ルール定義ファイルは、製品に搭載されているＲＢＡフレームワーク７に実装される。即ち、製品は、ルール定義ファイルがＲＢＡフレームワーク７に実装されることで、ルール定義ファイルを調停ロジックにしたがって実行し、表示調停制御を行う。網羅テストパターン生成部５ｂは、ＲＢＡ仕様モデルを用いてシミュレータ用の網羅テストパターンを生成し、その生成したシミュレータ用の網羅テストパターンを出力する。
【００１６】
ＰＣシミュレータ６は、網羅テストパターンの実行機能を有する。ＰＣシミュレータ６は、コード生成ツール５からルール定義ファイル及びシミュレータ用の網羅テストパターンを入力し、その入力したルール定義ファイルを調停ロジックにしたがって網羅テストパターンを用いて実行し、自動でシミュレーションする。網羅テストパターンはコンテンツの組み合わせから生成され、調停は同じ表示エリアに対して表示可能なコンテンツが同時に発生した場合に行われる。コンテンツがｎ（ｎは自然数）個であり、同じ表示エリアに対してｍ（ｍは自然数、ｎ≧ｍ）個の調停を行う場合には、以下の個数の網羅テストパターンが生成される。
nＰm＝ｎ！／（ｎ−ｍ）！
（「！」は階乗を示す）
即ち、ＰＣシミュレータ６は、網羅テストパターンの実行機能により、コンテンツの組み合わせを自動でシミュレーションし、ＲＢＡ仕様モデルで定義されたルールの挙動を自動でシミュレーションする。コンテンツの個数である「ｎ」及び調停を行う個数である「ｍ」は、それぞれ作業者により指定される。ＰＣシミュレータ６は、シミュレーションを終了すると、その評価結果をテスト結果ログとして出力する。
【００１７】
ここで、モデル検証ツール４によるモデル検証とＰＣシミュレータ６によるシミュレーション評価との相違について説明する。
モデル検証は、後述するＳＭＴソルバを使ってエリア定義、コンテンツ定義、制約式の間に矛盾が無いか（充足可能か）をチェックする検証であり、実際の調停ロジックを使わずにモデル情報だけを使って検証する手法である。モデル検証では、起こり得る全ての組み合わせに対して制約式を満たすことが可能であるか否を検証することができ、完全網羅が可能であるが、調停結果までは出力することができない。即ち、モデル検証では、問題が解けるかどうかは判るが、解は判らない。
【００１８】
シミュレーション評価は、実際の調停ロジックを使って評価する手法である。シミュレーション評価では、調停結果を出力することができ、表示調停制御の挙動が判る。シミュレーション評価は、手動でも自動でも実行可能であるが、起こり得る全ての組み合わせに対して制約式を満たすことが可能であるか否を検証することはできず、完全網羅が不可能である。シミュレーション評価では、組み合わせの数（Ｎ）を増やしながら実行時カバレッジを計測し、一定の基準を満たすまで評価を続ける。
【００１９】
実行時カバレッジの例を以下に示す。
・各エリアに表示可能なコンテンツが少なくとも１回は表示される。
・各エリアで任意の２つのコンテンツ間の調停が少なくとも１回ずつ実行される。
・制約式の各ノードの条件評価が網羅される（条件網羅）。
例えばＡ且つＢならば！Ｃ（Ａ  ＡＮＤ  Ｂ  −＞  ！Ｃ）という制約式があった場合であれば、
Ａが真の場合、偽の場合、
Ｂが真の場合、偽の場合、
（Ａ  ＡＮＤ  Ｂ）が真の場合、偽の場合、
Ｃが真の場合、偽の場合、
！Ｃが真の場合、偽の場合、
（Ａ  ＡＮＤ  Ｂ  −＞  ！Ｃ）が真の場合、偽の場合、
これらの全てが網羅されるまで評価を続ける。
【００２０】
次に、ＲＢＡ仕様モデルの構成及び調停ロジックについて順次説明する。
（１）ＲＢＡ仕様モデルの構成
ＲＢＡ仕様モデルは、エリア定義と、コンテンツ定義と、制約式とを含む。エリア定義では、表示場所として、表示エリアの位置、表示エリアの重ね合わせの順序、表示エリアのサイズが定義される。又、エリア定義では、表示場所の価値として、優先度、視認性が定義される。更に、エリア定義では、調停ポリシーとして、優先度調停、後勝ち調停、価値ベース調停が定義される。優先度調停は、表示エリア単位の調停ポリシーであり、その表示エリアに表示可能なコンテンツの中で最も価値が高いコンテンツを表示する調停である。後勝ち調停は、表示エリア単位の調停ポリシーであり、その表示エリアで最後に要求が発生したコンテンツを表示し、そのコンテンツの表示が終了した場合は残っている中で最後に要求が発生したコンテンツを表示する調停である。価値ベース調停は、表示エリア全体での調停ポリシーであり、コンテンツの価値を数値化した数値と表示エリアの価値を数値化した数値とを乗じた演算値が最大となるようにコンテンツを表示する調停である。
【００２１】
コンテンツ定義では、表示内容の状態として、例えば通常表示、警告表示が定義される。又、コンテンツ定義では、表示内容の価値として、優先度が定義される。更に、コンテンツ定義では、表示可能表示エリアとして、複数の表示エリアが定義される。制約式では、調停結果が満たすべき条件、表示エリア抑制やコンテンツ抑制の条件（ランタイム制約）、モデル検証の制約、シミュレータ評価の制約が定義される。
【００２２】
コンテンツには「GoodLoser」という属性がある。「GoodLoser」は、調停負けしたときに要求を取り下げるか残したままにするかの属性であり、「GoodLoser=true」の場合、調停負けしたときに要求を取り下げる。「GoodLoser」を使用する例を以下に示す。
エリア定義は、通常画面の表示エリア（Ａ）、割込みの表示エリア（Ｂ）、何れも後勝ちの調停ポリシーである。
コンテンツ定義は、表示エリア（Ａ）に表示可能なコンテンツは、例えばナビ、オーディオ、走行支援等であり、表示エリア（Ｂ）に表示可能なコンテンツは、例えばＴＢＴ通知等である。
制約式は、
B.isDisplayed() -> A.isHidden() //割込みエリアは通常画面を隠す。
(pre)ナビ.isVisible() -> !TbT通知.isVisible() //ナビを表示していたらTbT割込み通知しない。
【００２３】
上記したモデルの問題点は、
１．モデルをシミュレーション実行し、ナビを表示しているときにＴｂＴ通知の表示要求を出しても制約式によってＴｂＴ通知は表示されない（意図通り）
２．続けて、オーディオの表示要求を出すと、表示エリア（Ａ）は後勝ちなのでオーディオが表示される（意図通り）
３．更に続けて、走行支援の表示要求を出すと、ＴｂＴ通知が表示されてしまう（意図しない振る舞い、ＴｂＴ通知が表示されるのは前の状態がナビ表示でないことに因る）
ＴｂＴ通知は調停負けしたら要求を取り下げないといけないので、これを「GoodLoser」にすることで実現する。
【００２４】
制約式で扱える論理式は、コンテンツの状態、表示エリアの状態、表示エリアに表示中のコンテンツ、表示エリア、コンテンツの集合、論理演算、量化記号である。コンテンツの状態は、アクティブであるか非アクティブであるか、表示中であるか非表示中であるかである。表示エリアの状態は、表示中であるか非表示中であるかである。論理演算は、ＮＯＴ（！）、ＡＮＤ、ＯＲ、含意（−＞）、等号（＝）である。量化記号は、∀（Ｆｏｒ  Ａｌｌ：集合の要素全てに対して条件が成立する）、∃（Ｅｘｉｓｔｓ：集合に条件を満たす要素が少なくとも一つ存在する）である。
【００２５】
制約式では、調停前の状態を条件に使用できるようにしたこと、「isHidden」というエリアが隠されているかどうかを定義している。「isHidden」を使用する例を以下に示す。
For-All ALL#CONTENTS[x |
(!(pre)x.isVisible() AND x.isVisible())
-> (!(pre)x.isActive() OR
Exists ALL#AREAS[ a |
a.displayingContent() == x AND (
((pre)a.isVisible() AND !(pre)a.displayingContent().isActive())
OR(pre)a.isHidden()
)
]
)
]
上記した意味は、「今回新しく表示されたコンテンツは、今回表示要求を出したコンテンツか、そのコンテンツが表示されたエリアで、前のコンテンツの表示要求がなくなった場合、又はそのエリアが前回隠されていたエリアでなければならない」
シミュレーションで網羅的テストパターンを実行しながら、この制約式を評価することで、作業者の意図しない振る舞いを検出することができる。そして、このように作業者の意図しない振る舞いを検出することで、上記した「GoodLoser」の設定忘れをチェックすることができる。又、このように１つの不具合を検出したときに、評価用の制約式を用い、今回の検出した不具合と同じような不具合の存在を、網羅評価のシミュレーションによりチェックすることができる。
【００２６】
（２）調停ロジック
調停ロジックには、表示エリア毎の調停と表示エリア全体の調停とがある。
表示エリア毎の調停は、優先度調停及び後勝ち調停の表示エリアを、表示エリアの価値の高い順に調停する。各表示エリアについて、最も優先されるコンテンツを仮に割り当て、制約式の評価結果が正であれば、仮に割り当てたコンテンツを確定し、制約式の評価結果が否であれば、次に優先されるコンテンツを再評価する。制約式を満たすコンテンツが無ければ、その表示エリアにはコンテンツを表示しない。
【００２７】
表示エリア全体の調停（価値ベース調停）は、ベストフィットロジック及びワンパスロジックがある。ベストフィットロジックは、制約式を満たすコンテンツと表示エリアとの全ての組み合わせの中から価値の総和が最も高いものを選択する。ワンパスロジックは、価値の高い表示エリアから順に優先度を調停し、価値の高いコンテンツを価値の高い表示エリアに配置する。尚、既に他の表示エリアに割り当てられたコンテンツは対象外にする。
【００２８】
図２は、マルチメディア系の割込みとスイッチ操作系の割込みのサンプルモデルを例示している。コンテンツ抑制は、コンテンツＣの通常表示中は割込み通知しない。「中心.displayingContent（）=コンテンツＣ -> ! コンテンツＣ通知.isVisible（）」は、中心表示エリアにコンテンツＣを表示していれば、コンテンツＣ通知を表示しない、という制約である。又、後勝ち調停と優先度調停が混在する場合では、基本的に後勝ち調停を優先するが、ＭＭ系割込みの中ではＴＥＬを優先する。「TEL.isActive（） -> For All MM系割込み（TEL以外） [ x |!x.isVisible（）]」は、ＴＥＬがアクティブであれば、全てのＭＭ系割込み（ＴＥＬ以外）を表示しない、という制約である。
【００２９】
次に、上記した構成の作用について図３及び図４を参照して説明する。作業者は、表示調停制御の仕様化を意図通りに行えているか否かを以下の手順にしたがって評価する。
最初に、作業者は、モデルの記述式にしたがい、モデルエディタ２を用いてＲＢＡ仕様モデルを生成する（Ｓ１、モデル生成手順に相当する）。次に、作業者は、モデルエディタ２を用いて生成したＲＢＡ仕様モデルの記述を、手動でシミュレーションして具体的な表示調停制御の挙動を検証し、意図通りの動作をしているか否かを確認する（Ｓ３）。作業者は、意図通りの動作をしている旨を確認できなければ（Ｓ３：ＮＯ）、ステップＳ１に戻り、モデルエディタ２を用いてＲＢＡ仕様モデルを生成し直し（Ｓ１）、ステップＳ１以降の手順を繰り返す。
【００３０】
作業者は、意図通りの動作をしている旨を確認できれば（Ｓ３：ＹＥＳ）、モデル検証ツール４を用いてＲＢＡ仕様モデルを検証する（Ｓ４、モデル検証手順に相当する）。作業者は、ＳＭＴソルバ（Ｚ３）を用いた形式手法により検証し、述語論理による命題が充足可能であるか否かをチェックする。ＳＭＴソルバでは、図４に示すように、モデル情報（エリア定義、コンテンツ定義、制約式）を、述語論理を含むＺ３のスクリプトに変換し、Ｚ３でスクリプトを実行し、モデル情報において矛盾の有無（充足可能であるか否かを）をチェックする。
【００３１】
ここで、検証する制約式には、調停ロジックの中に含まれるものに加え、評価用の制約式を手動で追加することができる。後述する網羅テストパターンによる検証は膨大な時間を要するが、ＳＭＴソルバによる検証は短時間（数秒から数分程度）で完了するので、ＳＭＴソルバによる検証では、仕様の論理的な矛盾の有無を短時間で検証することができる。即ち、作業者は、先にＲＢＡ仕様モデルを検証して論理的なエラーを除去し、その後に網羅テストパターンを用いるシミュレーションを実施することで効率良く評価することができる。
【００３２】
作業者は、モデルを検証した検証結果の正否を確認する（Ｓ５）。作業者は、検証結果が正である旨を確認できなければ（Ｓ５：ＮＯ）、この場合も、ステップＳ１に戻り、モデルエディタ２を用いてＲＢＡ仕様モデルを生成し直し（Ｓ１）、ステップＳ１以降の手順を繰り返す。
【００３３】
作業者は、検証結果が正である旨を確認できれば（Ｓ５：ＹＥＳ）、今回の評価対象のモデルが新規モデルであるか否かを確認する（Ｓ６）。作業者は、今回の評価対象のモデルが新規モデルである旨を確認すると（Ｓ６：ＹＥＳ）、コード生成ツール５を用いてルール定義ファイル及び網羅テストパターンを生成し（Ｓ７、ルール定義ファイル生成手順及び網羅テストパターン生成手順に相当する）、ＰＣシミュレータ６を用いて自動でシミュレーションする（Ｓ８、シミュレーション手順に相当する）。作業者は、ＰＣシミュレータ６から出力されたテスト結果ログを評価し、具体的な表示調停制御の挙動を評価し、評価結果の正否を確認する（Ｓ９）。作業者は、評価結果が正である旨を確認できなければ（Ｓ９：ＮＯ）、この場合も、ステップＳ１に戻り、モデルエディタ２を用いてＲＢＡ仕様モデルを生成し直し（Ｓ１）、ステップＳ１以降の手順を繰り返す。
【００３４】
作業者は、評価結果が正である旨を確認できれば（Ｓ９：ＹＥＳ）、製品の環境と類似する実機での評価を行い（Ｓ１０）、意図通りの動作をしているか否かを確認する（Ｓ１１）。作業者は、意図通りの動作をしている旨を確認できなければ（Ｓ１１：ＮＯ）、実機での評価結果が否である旨を確認し、この場合も、ステップＳ１に戻り、モデルエディタ２を用いてＲＢＡ仕様モデルを生成し直し（Ｓ１）、ステップＳ１以降の手順を繰り返す。作業者は、意図通りの動作をしている旨を確認できれば（Ｓ１１：ＹＥＳ）、実機での評価結果が正である旨を確認し、一連の作業を終了する。
【００３５】
又、作業者は、今回の評価対象のモデルが新規モデルでなく前回の評価対象のモデルからの仕様変更である旨を確認すると（Ｓ６：ＮＯ）、コード生成ツール５を用いてルール定義ファイルを生成し（Ｓ１２）、自動でシミュレーションして具体的な表示調停制御の挙動を評価し（Ｓ１３）、評価結果の正否を確認する（Ｓ１４）。作業者は、評価結果が正である旨を確認できなければ（Ｓ１４：ＮＯ）、この場合も、ステップＳ１に戻り、モデルエディタ２を用いてＲＢＡ仕様モデルを生成し直し（Ｓ１）、ステップＳ１以降の手順を繰り返す。
【００３６】
作業者は、評価結果が正である旨を確認できれば（Ｓ１４：ＹＥＳ）、ＰＣシミュレータ６から出力されたテスト結果ログの差分を確認し（Ｓ１５）、意図通りであるか否かを確認する（Ｓ１６）。作業者は、意図通りである旨を確認できなければ（Ｓ１６：ＮＯ）、この場合も、ステップＳ１に戻り、モデルエディタ２を用いてＲＢＡ仕様モデルを生成し直し（Ｓ１）、ステップＳ１以降の手順を繰り返す。作業者は、意図通りである旨を確認できれば（Ｓ１６：ＹＥＳ）、実機での評価を簡易的に行い（Ｓ１７）、意図通りの動作をしているか否かを確認する（Ｓ１８）。
【００３７】
作業者は、意図通りの動作をしている旨を確認できなければ（Ｓ１８：ＮＯ）、実機での簡易的な評価結果が否である旨を確認し、この場合も、ステップＳ１に戻り、モデルエディタ２を用いてＲＢＡ仕様モデルを生成し直し（Ｓ１）、ステップＳ１以降の手順を繰り返す。作業者は、意図通りの動作をしている旨を確認できれば（Ｓ１８：ＹＥＳ）、実機での簡易的な評価結果が正である旨を確認し、一連の作業を終了する。
【００３８】
即ち、作業者は、今回の評価対象のモデルが新規モデルでなく前回の評価対象のモデルからの仕様変更である旨を確認した場合には、コード生成ツール５を用いてルール定義ファイルを生成するが、網羅テストパターンを生成せずに、前回と同じ網羅テストパターンにより自動でシミュレーションして具体的な表示調停制御の挙動を評価し、テスト結果ログを比較することで、仕様変更を意図通りに行えたか否かを確認することができる。
【００３９】
作業者は、以上の一連の手順を行うことでルール定義ファイルの正否を評価することができる。そして、ルール間に矛盾が無い旨を確認した後に、製品搭載のＲＢＡフレームワーク７に実装することで、品質を保証したソフトウェアを製品に実装することができ、製品において適切な表示調停制御を実現することができる。
【００４０】
以上に説明したように本実施形態によれば、次に示す効果を得ることができる。表示調停制御をモデル化し、コンテンツと表示エリアとの組み合わせが制約式により示される制約を満たしているか否かを、網羅テストパターンを用いて自動でシミュレーションし、そのシミュレーション結果をテスト結果ログとして出力するようにした。シミュレーションによるテスト結果ログを解析することで、具体的な表示調停制御の挙動を理解し易くなる。又、調停結果が満たすべき条件を制約式で記述することで、ルール間に矛盾が無い仕様だけを定義することができ、ルール間に矛盾が有る仕様を除外することができる。更に、テスト結果ログによる評価を、表示調停制御に関するソフトウェアが製品に搭載される前に実施することで、仮に仕様に不具合があったとしても当該不具合をソフトウェア開発の初期の段階で修正することができ、作業工数の増大を未然に回避することができる。これにより、表示調停制御の仕様化を意図通りに行えているか否かを適切に評価することができる。加えると、網羅テストパターンをモデルから自動生成することで、網羅テストパターンの作成工数を削減することができる。評価用の制約式によりシミュレーション評価の自動実行が可能になる。モデル検証、シミュレーション評価、実機評価の順で段階を踏むことで、早期に不具合を修正することができる。工数を最も要する実機評価を、仕様変更の際に大幅に簡略化することができる。
【００４１】
又、ルールベース調停仕様モデルにおける矛盾の有無を検証するようにした。先にＲＢＡ仕様モデルを検証して論理的なエラーを除去し、その後に網羅テストパターンを用いるシミュレーションを実施することで、表示調停制御の仕様化を意図通りに行えているか否かを効率良く評価することができる。
【００４２】
又、ルールベース調停仕様モデルから表示調停制御に関する仕様書を生成するようにした。仕様書を容易に生成することができる。
【００４３】
尚、以上は、ＰＣシミュレータ６において、ルール定義ファイルを調停ロジックにしたがって網羅テストパターンを用いて実行し、自動でシミュレーションするが、網羅テストパターンの実行機能を用いず、ルール定義ファイルを手動でシミュレーションするだけで表示調停制御の挙動を評価しても良い。
【００４４】
本開示は、実施例に準拠して記述されたが、当該実施例や構造に限定されるものではないと理解される。本開示は、様々な変形例や均等範囲内の変形をも包含する。加えて、様々な組み合わせや形態、更には、それらに一要素のみ、それ以上、或いはそれ以下を含む他の組み合わせや形態をも、本開示の範疇や思想範囲に入るものである。
仕様書生成ツール３やモデル検証ツール４が省かれている構成でも良い。
【符号の説明】
【００４５】
図面中、１は表示調停制御の評価装置、２はモデル生成部、３は仕様書生成部、４はモデル検証部、５ａはルール定義ファイル生成部、５ｂは網羅テストパターン生成部、６はシミュレーション部である。
【図１】
2019192001.tif 000003
【図２】
2019192001.tif 000004
【図３】
2019192001.tif 000005
【図４】
2019192001.tif 000006