ＵＩ設計検証装置及び方法
【課題】 ＵＭＬのような図式表記で表現された製品のＵＩ挙動仕様を自動的に検証できるＵＩ設計検証装置を提供する。
【解決手段】 この発明のＵＩ設計検証装置は、表明変換用公理群を保持する表明変換用公理データベース５と、検証用公理群を保持する検証用公理データベース６と、図式表記のＵＩ設計仕様を代数的表記に変換したその代数表記を入力する代数表記入力部１と、入力された代数表記に対して、表明変換用公理データベースに登録されている表明変換用公理群の内の該当する公理を適用して表明を作成する表明変換用公理適用部２と、表明変換用公理が適用された表明に対して、検証用公理データベースに登録されている検証用公理群の内の該当する公理を適用して表明の検証を行う検証用公理適用部３と、検証用公理適用部にて検証した結果を出力する検証結果出力部４とを備えている。
【解決手段】 この発明のＵＩ設計検証装置は、表明変換用公理群を保持する表明変換用公理データベース５と、検証用公理群を保持する検証用公理データベース６と、図式表記のＵＩ設計仕様を代数的表記に変換したその代数表記を入力する代数表記入力部１と、入力された代数表記に対して、表明変換用公理データベースに登録されている表明変換用公理群の内の該当する公理を適用して表明を作成する表明変換用公理適用部２と、表明変換用公理が適用された表明に対して、検証用公理データベースに登録されている検証用公理群の内の該当する公理を適用して表明の検証を行う検証用公理適用部３と、検証用公理適用部にて検証した結果を出力する検証結果出力部４とを備えている。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ＵＩ挙動を検証するためのＵＩ設計検証装置及び方法に関する。
【背景技術】
【０００２】
本発明は、小型電子機器のユーザインターフェース設計の初期段階を対象としている。携帯電話が典型的な例であるが、その新機種は数ヶ月毎に発売され、開発作業と開発コスト回収も同じ期間でなされなくてはならない。そのため設計初期段階と引き続くファームウェア開発には、密接した連携が必要となる。
【０００３】
設計初期段階では、例えばｅ−ＳＩＭ社製（イスラエル）のＲａｐｉｄＰＬＵＳ（商品名）のようなプロトタイプ作成用のソフトウェアが用いられることがある。これらのソフトウェアはデモ用のアニメーションを生成することに主眼が置かれている。これは、デザイナーの興味がシステムの分析ではなく、製品形状と操作感覚に注がれることが多いためである。しかしながら、開発の視点から見ると、これらのプロトタイプ作成用ソフトウェアには２つの問題点がある。第１の問題点は、初期設計に続く開発作業のためのデータの共有と再利用の観点が欠けていることであり、第２の問題点は、質的な分析に対しての必要性が認識されていないことである。
【０００４】
したがって、ほとんどのプロトタイプ作成用ソフトウェアでは、自身のデータをデータ共有、再利用、質的分析のためのデータをエキスポートすることができない。さらにほとんどの製品仕様は、例えば、Ｍｉｃｒｏｓｏｆｔ Ｗｏｒｄ（商品名）で作成された文書のようなテキスト形式で書かれることが多く、形式的な表現ではないために自動的な検証を行うことはできない。よって設計初期段階においても、検証と再利用のための製品仕様の記述方法が必要であった。
【０００５】
また、プロトタイプ作成用ソフトウェアは、システムの振る舞いをアニメーションとして見せることに主眼が置かれている。しかしながら、そのデータは独自仕様であって公開されておらず、またデータ共有のための中間フォーマットなどは用いられていない。このためにデータの検証と再利用が妨げられている。
【０００６】
例えば、論文「Harel, D.: "Statecharts: A visual formalism for complex systems"; Science of Computer Programming 8 231-274 North-Holland (1987)」に記載されているプロトタイプ作成用ソフトウェアのように、いくつかのプロトタイプ作成用ソフトウェアでは、自身のデータをＳｔａｔｅｃｈａｒｔｓで出力することができる。またＧＵＩデザイン仕様にＳｔａｔｅｃｈａｒｔｓを用いるソフトウェアも幾つかある（例えば、論文「Horrocks, I.: "Constructing the User Interface with Statecharts"; Addison-Wesley, (1999)」）。Ｓｔａｔｅｃｈａｒｔｓは、状態遷移機械を表現するためには非常に有効であり、多くのツールが用意されている。
【０００７】
しかしながら、Ｓｔａｔｅｃｈａｒｔｓは図式表記であり、その形式化された表現については幾つかの提案、例えば、論文「Yacoub, S., Ammar, H.: "A Pattern Language of Statecharts"; PLoP-98 Conference (1998)」（非特許文献１）、論文「Costagliola, G. , Deufemia, V., Ferrucci, F. and Gravino, C.: "Implementing Statecharts using Extended Positional Grammars"; VLFM01, Symposium on Visual Languages and Formal Method, (2001)」（非特許文献２）があるが、矛盾したモデル記述を検証できる形式的な記述言語または数学的な表現形式は確立されていない。またＳｔａｔｅｃｈａｒｔｓには、排他的な状態遷移や、同期したイベント及び状態遷移を表現することはできない。
【０００８】
状態遷移機械の枠に縛られない概念的なモデルも提案されている。ＣＳＣＷ（Ｃｏｍｐｕｔｅｒ−ｓｕｐｐｏｒｔｅｄ Ｃｏｏｐｅｒａｔｉｖｅ Ｗｏｒｋ）の分野では、ＵＭＬに基づいた記述からＣＰＮ（Ｃｏｌｏｒｅｄ Ｐｅｔｒｉ Ｎｅｔ）の形式に変換する方法が提案されている（論文「Garrido, J., Gea, M.: "A Coloured Petri Net Formalisation for a UML-Based Notation Applied to Cooperative System Modeling"; Proceeding of 9th International Workshop, DSV-IS (2002)」（非特許文献３））。またこの領域では、論文「van der Veer, G. C., van Welie, M.:"Task Based Groupware Design: Putting theory into practice"; Proc. of Symposium on Designing Interactive Systems (DIS'2000), pp.326-337, (2000)」（非特許文献４）に記載されているＧＴＡ（Ｇｒｏｕｐ Ｔａｓｋ Ａｎａｌｙｓｉｓ）や、論文「Paterno, F.: "Model-based Design and Evaluation on Interactive Applications"; Springer-Verlag, (2000)」（非特許文献５）に記載されているＣＴＴ（ＣｏｎｃｕｒＴａｓｋＴｒｅｅｓ）なども提案されている。また、これらの表現形式からペトリネットへと変換する方式（ＩＣＯ ｆｏｒｍａｌｉｓｍ）も提案されている（例えば、論文「Palanque, P., Bastide, R.: "Synergistic modeling on task, users and systems using formal specification techniques"; Interacting with Computers 9, pp.129-153, (1997)」（非特許文献６））。
【非特許文献１】Yacoub, S., Ammar, H.: "A Pattern Language of Statecharts"; PLoP-98 Conference (1998)
【非特許文献２】Costagliola, G., Deufemia, V., Ferrucci, F. and Gravino, C. : Implementing Statecharts using Extended Positional Grammars; VLFM01, Symposium on Visual Languages and Formal Method, (2001)
【非特許文献３】Garrido, J., Gea, M.: "A Coloured Petri Net Formalisation for a UML-Based Notation Applied to Cooperative System Modeling"; Proceeding of 9th International Workshop, DSV-IS (2002)
【非特許文献４】van der Veer, G. C., van Welie, M.: "Task Based Groupware Design: Putting theory into practice"; Proc. of Symposium on Designing Interactive Systems (DIS'2000) , pp.326-337, (2000)
【非特許文献５】Paterno, F.: "Model-based Design and Evaluation on Interactive Applications"; Springer-Verlag, (2000).
【非特許文献６】Palanque, P., Bastide, R. : Synergistic modeling on task, users and systems using formal specification techniques; Interactign with Computers 9, pp.129-153, (1997)
【発明の開示】
【発明が解決しようとする課題】
【０００９】
本発明は、上述のような従来技術の問題点に鑑みてなされたものであり、ＵＭＬのような図式表記で表現された製品のＵＩ挙動仕様を自動的に検証できるＵＩ設計検証装置及び方法を提供することを目的とする。
【課題を解決するための手段】
【００１０】
請求項１の発明のＵＩ設計検証装置は、表明変換用公理群を保持する表明変換用公理データベースと、検証用公理群を保持する検証用公理データベースと、図式表記のＵＩ設計仕様を代数的表記に変換したその代数表記を入力する代数表記入力部と、入力された代数表記に対して、前記表明変換用公理データベースに登録されている表明変換用公理群の内の該当する公理を適用して表明を作成する表明変換用公理適用部と、前記表明変換用公理が適用された表明に対して、前記検証用公理データベースに登録されている検証用公理群の内の該当する公理を適用して表明の検証を行う検証用公理適用部と、前記検証用公理適用部にて検証した結果を出力する検証結果出力部とを備えたものである。
【００１１】
請求項２の発明は、請求項１のＵＩ設計検証装置において、前記検証用公理適用部には、完全性、強連結性、状態数の最小性についての公理を適用して検証する第１検証用公理適用部と、階層構造の一貫性についての公理を適用して検証する第２検証用公理適用部と、非決定性仕様の公理を適用して検証する第３検証用公理適用部とを備えたことを特徴とするものである。
【００１２】
請求項３の発明のＵＩ設計検証方法は、コンピュータを用いて、図式表記のＵＩ設計仕様を代数的表記に変換したその代数表記を入力する処理と、入力された代数表記に対して、表明変換用公理データベースに登録されている表明変換用公理群の内の該当する公理を適用して表明を作成する処理と、作成された表明に対して、検証用公理データベースに登録されている検証用公理群の内の該当する公理を適用して表明の検証を行う処理と、検証した結果を出力する処理とを実行するものである。
【００１３】
請求項４の発明は、請求項３のＵＩ設計検証方法において、前記検証用公理群の内の該当する公理を適用して表明の検証を行う処理には、完全性、強連結性、状態数の最小性についての公理を適用して検証する第１の検証と、階層構造の一貫性についての公理を適用して検証する第２の検証と、非決定性仕様の公理を適用して検証する第３の検証とを含むことを特徴とするものである。
【発明の効果】
【００１４】
本発明によれば、図式表記されたＵＩ挙動設計の自動的な検証が可能であり、ＵＩ挙動設計の効率化に寄与できる。
【発明を実施するための最良の形態】
【００１５】
以下、本発明の実施の形態を図に基づいて詳説する。
図１は本発明の１つの実施の形態のＵＩ設計検証装置の機能ブロック図である。本実施の形態のＵＩ設計検証装置は、Ｓｔａｔｅｃｈａｒｔｓ等の図式表記を代数的表記に変換したその代数表記を入力する代数表記入力部１、入力された代数表記に対して、表明変換用公理データベース５に登録されている表明変換用公理群の内の該当する公理を適用して表明を作成する表明変換用公理適用部２、この表明変換用公理が適用された表明に対して、検証用公理データベース６に登録されている検証用公理群の内の該当する公理を適用して表明の検証を行う検証用公理適用部３、この検証用公理適用部３にて検証した結果を表示し、またプリントアウト等を行う検証結果出力部４から構成されている。
【００１６】
検証用公理適用部３には、完全性、強連結性、状態数の最小性についての公理を適用して検証する第１検証用公理適用部３−１、階層構造の一貫性についての公理を適用して検証する第２検証用公理適用部３−２、そして非決定性仕様の公理を適用して検証する第３検証用公理適用部３−３を有している。また検証結果出力部４は、第１〜第３検証用公理適用部３−１〜３−３それぞれに対応して完全性、強連結性、状態数の最小性の検証結果を出力する第１検証結果出力部４−１、階層構造の一貫性の検証結果を出力する第２検証結果出力部４−２、そして非決定性仕様の検証結果を出力する第３検証結果出力部４−３を備えている。
【００１７】
上記実施の形態のＵＩ設計検証装置によるＵＩ設計検証方法のシーケンスは、図２に示す通りである。まず、Ｓｔａｔｅｃｈａｒｔｓ等の図式表記を代数的表記に変換し（ステップＳＱ１１）、ステップＳＱ１１で変換した代数的表記を表明変換用公理データベース５から該当する表明変換用公理を抽出して適用して表明に変換し（ステップＳＱ１２）、ステップＳＱ１２で変換した表明に検証用公理データベース６から該当する検証用公理を抽出して適用し、その検証結果を出力する（ステップＳＱ１３、ＳＱ１４、ＳＱ１５）。ステップＳＱ１３は完全性、強連結性、状態数の最小性についての公理の検証であり、ステップＳＱ１４は階層構造の一貫性についての公理の検証であり、ステップＳＱ１５は非決定性仕様の公理の検証である。
【００１８】
図３は、本実施の形態の代数的記述と評価の流れのシーケンス図である。図３はＩＤＥＦ０（アクティビティ・モデリング手法）形式で表現されている。四角い箱はアクティビティを示し、箱に左から入る矢印がアクティビティへの入力を、右側に出る矢印が出力を示している。他に、上から入る矢印が参照用のデータ、下から入る矢印がアクティビティで使用するメカニズムを示す。
【００１９】
設計者が作成したデザインを入力としてＵＩプロトタイプ／シナリオベースのＳｔａｔｅｃｈａｒｔｓを生成し（アクティビティＡ１１）、作成したＳｔａｔｅｃｈａｒｔｓを入力として公理系からデータを参照して公理を適用し（アクティビティＡ１２）、適用した公理を入力として検証用公理系からデータを参照して検証用公理を適用し、検証結果を出力する（アクティビティＡ１３）。
【００２０】
本発明では仕様の記述と検証に、製品仕様の数学的な記述表現と公理に基づく代数的な検証方法を用いる。これは、Ｃ．Ａ．Ｒ Ｈｏａｒｅによって提唱され計算機言語のＰＡＳＣＡＬの意味的な仕様をエミュレートする際に用いられた方法である。その詳しい方法は、論文「C. A. R. Hoare, N. Wirth: "An axiomatic definition of the programming language Pascal"; Acta Information 2, pp.335-355, (1973)」に記載されている。Ｍａｒｇｒｅｎは、論文「Margren, W.: "Formal Specification of Graphic Data Types"; ACM Transactions on Programming Languages and systems, vol.4, No.4, pp.687-710, (1982)」において、この方法論を２次元グラフィックディスプレイ上の２つの描画画像が等価であるかどうかの証明に用いている。この方法では検証は２つのステージで行われる。始めに代数的に表現された状態遷移機械の仕様から表明が生成される。「表明」とは、内部変数と状態遷移に関する事実の集まりであり、代数式による宣言の集成とも言える。「公理」は論理学的な取り扱いでは「自明の、もしくはあまねく認識されている真実」である。代数仕様と表明の間には１対１の対応関係がある。公理は、代数仕様から表明の変換を定義するルールであり、代数仕様が表明中に残す効果を表現している。全ての代数的仕様を公理によって変換すると、最終的な表明が残される。この作業によって状態遷移機械の数学的な表現が導出される。アクティビティＡ１３では、別の公理の集合が表明に適用されて仕様の検証が行われる。
【００２１】
本実施の形態では、ＵＩ設計の図式的表記であるＳｔａｔｅｃｈａｒｔｓから導出される基本的な有限状態機械を定義し検証するために、以下の情報を代数表現する。図４に状態遷移機械の代数表現の例を挙げる。「宣言開始」、「状態名宣言」、「イベント名宣言」、「アクション名宣言」、「大域的開始状態宣言」、「状態遷移宣言」、「状態遷移の階層構造定義」等である。状態遷移宣言は開始状態、終了状態、遷移を起動するイベント、同時に実行されるアクションの宣言なども行う。状態遷移の階層構造定義は、開始状態、サブ状態、終了状態、ヒストリインディケータの宣言を含む。階層構造の入れ子や並行サブプロセスなども表現する。
【００２２】
また図５に階層構造の代数表現の例を示している。スーパー状態ｓ３については、サブ状態がｓ５，ｓ６である。このＳｔａｔｅｃｈａｒｔｓに対する代数表現は、同図（ｂ）のように表現する。また、図６に並行動作の代数表現を例示している。複数の階層構造を併記して表現している。同図（ａ）のＳｔａｔｅｃｈａｒｔｓに対して同図（ｂ）のように代数表現する。
【００２３】
以下の説明では、ケーススタディとしてＶＷＣ（Ｖｉｓｕａｌ Ｗｉｒｅｌｅｓｓ Ｃｏｍｍｕｎｉｃａｔｏｒ）というデバイスのＵＩ設計検証を例示して説明する。ＶＷＣは無線ＬＡＮを経由して幾つかのリモートカメラを操作し、自身のＬＤＣモニタに映し出す小型の電子機器で、人間が直接行くには危険な作業現場などで有効と考えられる。他には、レジャー用途として非常に見晴らしが良いが一般の観光客が行けないような危険な場所（崖の突端や高層ビルの展望スペースの外側など）にリモートカメラを設置し、観光客がコントロールユニットを制御して自分の記念写真を撮り、撮影した写真を携帯電話に電子メールとして受け取る、といった用途で使われるものである。
【００２４】
図７に代数的仕様記述の例を示す。この記述は、ケーススタディとしたＶＷＣの仕様の一部である。それぞれの記述は、名前と引数の組み合わせで表現される。これは入力部１においてユーザーが行う（アクティビティＡ１１）。
【００２５】
次に図３におけるアクティビティＡ１２にて行う代数的仕様記述から表明への変換について説明する。始めに、表明変換用公理適用部２において、入力された代数的仕様記述から表明への変換を行う。代数的仕様記述を変換する際には、表明中の変数への代入などが行う。この変換が完了すると、最終的に残された表明が仕様全体を表現している。次に検証用公理適用部３にて、表明に対する検証を行う。この検証では、検証対象とするシステム内部の全ての変数を必要とするわけではなく、２つのステージ（アクティビティＡ１２、Ａ１３）で必要とされるものだけを取り扱う。従って表明で表現する変数などは最小限の範囲で取り扱う。
【００２６】
図８は、代数的仕様記述から表明への変換の一部を例示している。Ａｘ１とＡｘ２の式は、表明を生成するための公理の例である。図８では、代数“Ｓｔａｒｔ（ ）”を記述の開始の宣言として用いている。この代数に適用される公理Ａｘ１は、有限状態機械を定義する全ての変数の初期化を行う。Ａｘ１を代数式“Ｓｔａｒｔ（ ）”に適用すると、表明のテンプレートとして全ての変数が初期化された空リストの集合が生成される（アクティビティＡ２１）。他の公理では代数式に従って、このリストへ値を代入する形で表明の変換を定義する。
【００２７】
Ａｘ２は宣言された状態名を表明中の“ｓｔａｔｅＬｉｓｔ”に登録するために用いられる。引数ｓがａｔｏｍの場合（状態名が単独で登録される場合）は、その要素のみを含むリストが生成されて、“ｓｔａｔｅＬｉｓｔ”と結合される。図８では、下線をつけた状態名が“ｓｔａｔｅＬｉｓｔ”に付加されている（アクティビティＡ２２）。ここでは、リスト操作のための一般的な公理が必要なため、２つのステージの両方で利用できるように用意してある。“ＩｓＬｉｓｔ”と“Ｕｎｉｏｎ”などの公理はリスト操作用として予め用意してある。
【００２８】
表明検証用公理適用部３による表明の検証は、表明をそのままの形式で検証することは不可能なので、検証用の公理のグループをデータベース６に用意している。検証用の公理は、表明を入力として特定の状況を満たしているかどうかを判断するための検証結果を出力する。
【００２９】
一般にイベントは自身の名前と引数、以前に実行されたイベントによって累積した結果によりシステムの変数の生成もしくは変更を引き起こす。上記の公理は、イベントに対応して表明を生成するので、全てのイベント系列を表明に変換し、得られた表明をシステムの最終状態の表現とし、本実施の形態ではこれを検証結果として出力する。
【００３０】
図９はＶＷＣデバイスのＳｔａｔｅｃｈａｒｔｓを示している。このチャートは、状態遷移のトップレベルを示している。図１０には並行サブプロセスの部分を示してある。図９のチャートにおいて、“Ｐｏｗｅｒ＿Ｏｆｆ”が初期状態であり、電源が入れられると制御ユニットはリモートカメラをコントロールすることが可能となる。図中のアスタリスク（＊）は、並行サブ状態が存在することを示している。
【００３１】
用意してある公理には以下の３種類がある。（１）“Ｓｔａｒｔ（ ）”で用いる初期化用公理、（２）代数的表現に１対１に対応して表明を生成するための公理、（３）検証に用いるための公理である。このうち、（１）と（２）の公理を参照して表明を生成するが、これについて説明する。本実施の形態では、代数的仕様記述を関数呼び出しとして使用し表明を生成する。代数的仕様記述は“Ｓｔａｒｔ（ ）”から始まり、その内容に従ってシステムの初期化を行う。表明に含まれて検証で用いられる情報のリストを以下に挙げる。「状態名を列挙したリスト」、「イベント名を列挙したリスト」、「アクション名を列挙したリスト」、「全ての状態遷移を列挙したリスト」、「状態の階層構造に関する定義を列挙したリスト」、「遷移する可能性のある状態のリスト、またそれらの直積集合」、「イベントとアクションの直積集合」である。
【００３２】
本実施の形態では、状態遷移機械の検証のために、上記（３）の公理を用いて表明を検証するために、図１１に示すような完全性、強連結性、状態数の最小性を検証する第１の検証（ステップＳＱ１３）、図１２〜図１４に示すような階層構造記述の一貫性と並行状態の記述を検証する第２の検証（ステップＳＱ１４）、そして図１５に示すような非決定性問題を検証する第３の検証（ステップＳＱ１５）を実行する。
【００３３】
図１１に示したように、ステップＳＱ１３の完全性、強連結性、状態数の最小性の検証は次の通りである。
【００３４】
［完全性］完全性の検証では、全ての状態から少なくとも一つの他の状態への遷移が存在するかどうかを検証する。このために、公理中では、各々の状態からの遷移が定義されているかどうかを確認する。
【００３５】
［強連結性］強連結性の検証では、任意の状態ｕ及びｖの間での状態遷移と、その逆の遷移が可能であるかどうかの検証を行う。公理中では、状態名の直積集合を元に、ある状態から他の状態への遷移が可能であるかどうかを探索する。
【００３６】
［状態数の最小性］イベントとアクションの組み合わせから決まる最小限の個数の状態遷移を持つべき、同じイベントとアクションの組み合わせで並行した状態遷移が定義されている場合は、状態遷移の設計が不完全で、後述する非決定性問題を起こす可能性がある。このような場合、並行サブ状態などを用いて、イベントとアクションの組み合わせが単一の状態遷移を持つように、遷移の構造を見直す必要がある。そこで、公理では遷移を起こすイベントとアクションの組み合わせの数で検証する。
【００３７】
ステップＳＱ１４の階層構造の検証では、図１２〜図１４に示し、以下に列挙するように細分化された詳細な項目に関して行う。１つめの項目としては、サブ／スーパーの状態の関係（階層構造の定義）が一貫して、ツリー構造となっているか、２つめの項目としては、サブ状態からスーパー状態へ戻る遷移が少なくとも一つ定義されているかどうか。３つめの項目としては、スーパー状態への遷移が定義されているときに、その中で初期状態が宣言されているか、４つめの項目としては、終了状態への遷移が定義されているときに、終了状態に対応する外部の状態が宣言されているかどうか、５つめの項目としては、初期状態／終了状態への直接の遷移が定義されていないかどうか、６つめの項目としては、サブ状態からの遷移が一定の方式に従っているかどうかを検証する。
【００３８】
図１５に示したように、ステップＳＱ１５の非決定性仕様の検証は、階層構造の中で２つ以上の遷移が、同じイベント／アクションの組み合わせで発生する場合、その仕様は非決定性問題（矛盾した仕様）を含んでいる可能性がある。例えば、同じイベントによって階層構造の外側への遷移と、階層構造の内側での遷移が定義されているような場合である。このような状況を検出するために、本発明では階層構造中での同じイベントによる遷移をチェックし、必要であれば警告を出す。
【００３９】
本実施の形態によれば、特定の言語に依存しない特徴がある。また、静的な仕様と動的なイベント系列を入力とした仕様の検証の両方に適用できる特徴もある。さらに、有限状態機械に適用可能な公理の標準的な集合を定義できる特徴もある。
【実施例１】
【００４０】
次に、本発明の実施例について説明する。ＶＷＣデバイスのＵＩ挙動設計のため図１６、図１７に示したＳｔａｔｅｃｈａｒｔｓを作成し、これに対して、図１８に示す代数表現を作成して入力し、ＵＩ挙動の検証実験を実施した。この検証結果は、図１９〜図２１の検証結果１〜検証結果３に示すものであった。すなわち、図１９の検証結果１に示したように、サブ状態のさらに下で「待機中」という同じ状態名が出てくることを発見した。また、図２０の検証結果２に示したように、システム全体での初期状態の指定が欠けている点を発見した。つまり、“電源ＯＮ”中のどれが初期状態になるかが不明であることを発見した。この場合、四角で囲った「待機中」のサブ状態には開始を示すマークが付加されるべきであるのが、欠落しているのである。さらに、図２１の検証結果３に示したように、開始状態として定義された状態への複数の遷移を発見した。これは、他のサブ状態で同じ状態名「待機中」を使っている場合にも起こるものである。
【実施例２】
【００４１】
図２２、図２４に示すようなＳｔａｔｅｃｈａｒｔｓに対して代数表現を作成し、本実施の形態のＵＩ設計検証装置に入力し、非決定性仕様を検証した。その結果として、図２３、図２５の検証結果を得た。これにより、図２２、図２３よりサブ状態関係の状態ｓ２とｓ１からの同一のイベントによる遷移があるので、これを非決定性遷移として警告を発することができることを確認できた。また図２４、図２５より並行関係中で同一イベントによる外部への遷移がある場合、非決定性遷移として警告を発することが確認できた。
【図面の簡単な説明】
【００４２】
【図１】本発明の一つの実施の形態のＵＩ設計検証装置の機能ブロック図。
【図２】上記実施の形態のＵＩ設計検証装置のＵＩ設計検証動作のフローチャート。
【図３】上記実施の形態のＵＩ設計検証装置が実行するＵＩ設計検証動作のフローチャート（ＩＤＥＦ０形式による）。
【図４】上記実施の形態のＵＩ設計検証装置で入力する状態遷移機械の代数表現例１の説明図。
【図５】上記実施の形態のＵＩ設計検証装置で入力する状態遷移機械の代数表現例２の説明図。
【図６】上記実施の形態のＵＩ設計検証装置で入力する状態遷移機械の代数表現例３の説明図。
【図７】上記実施の形態のＵＩ設計検証装置に入力するＶＷＣデバイスのＵＩ設計仕様の代数表現例の説明図。
【図８】上記実施の形態のＵＩ設計検証装置による具体的なＵＩ設計検証動作のフローチャート（ＩＤＥＦ０形式による）。
【図９】上記実施の形態のＵＩ設計検証装置にて検証対象としたＶＷＣデバイスのＵＩ挙動仕様のトップレベルのＳｔａｔｅｃｈａｒｔｓの図。
【図１０】上記実施の形態のＵＩ設計検証装置にて検証対象としたＶＷＣデバイスのＵＩ挙動仕様の並行サブプロセスのＳｔａｔｅｃｈａｒｔｓの図。
【図１１】上記実施の形態のＵＩ設計検証装置にて検証する第１の検証項目の説明図。
【図１２】上記実施の形態のＵＩ設計検証装置にて検証する第２の検証項目の説明図（その１）。
【図１３】上記実施の形態のＵＩ設計検証装置にて検証する第２の検証項目の説明図（その２）。
【図１４】上記実施の形態のＵＩ設計検証装置にて検証する第２の検証項目の説明図（その３）。
【図１５】上記実施の形態のＵＩ設計検証装置にて検証する第３の検証項目の説明図。
【図１６】上記実施の形態のＵＩ設計検証装置にて検証対象とした実施例１のＶＷＣデバイスのＵＩ挙動仕様のトップレベルのＳｔａｔｅｃｈａｒｔｓの図。
【図１７】上記実施の形態のＵＩ設計検証装置にて検証対象とした実施例１のＶＷＣデバイスのＵＩ挙動仕様の並行サブプロセスのＳｔａｔｅｃｈａｒｔｓの図。
【図１８】上記実施の形態のＵＩ設計検証装置にて検証対象とした実施例１のＶＷＣデバイスのＵＩ挙動仕様の代数表現の一部を示す説明図。
【図１９】上記実施の形態のＵＩ設計検証装置にて検証対象とした実施例１のＶＷＣデバイスのＵＩ挙動仕様に対する検証結果１の説明図。
【図２０】上記実施の形態のＵＩ設計検証装置にて検証対象とした実施例１のＶＷＣデバイスのＵＩ挙動仕様に対する検証結果２の説明図。
【図２１】上記実施の形態のＵＩ設計検証装置にて検証対象とした実施例１のＶＷＣデバイスのＵＩ挙動仕様に対する検証結果３の説明図。
【図２２】上記実施の形態のＵＩ設計検証装置にて検証対象とした実施例２のＵＩ挙動仕様その１のＳｔａｔｅｃｈａｒｔｓの図。
【図２３】上記実施例２のＵＩ挙動仕様その１に対する検証結果の説明図。
【図２４】上記実施の形態のＵＩ設計検証装置にて検証対象とした実施例２のＵＩ挙動仕様その２のＳｔａｔｅｃｈａｒｔｓの図。
【図２５】上記実施例２のＵＩ挙動仕様その２に対する検証結果の説明図。
【符号の説明】
【００４３】
１ 代数表記入力部
２ 表明変換用公理適用部
３ 検証用公理適用部
３−１ 第１検証用公理適用部
３−２ 第２検証用公理適用部
３−３ 第３検証用公理適用部
４ 検証結果出力部
４−１ 第１検証結果出力部
４−２ 第２検証結果出力部
４−３ 第３検証結果出力部
５ 表明変換用公理データベース
６ 検証用公理データベース
【技術分野】
【０００１】
本発明は、ＵＩ挙動を検証するためのＵＩ設計検証装置及び方法に関する。
【背景技術】
【０００２】
本発明は、小型電子機器のユーザインターフェース設計の初期段階を対象としている。携帯電話が典型的な例であるが、その新機種は数ヶ月毎に発売され、開発作業と開発コスト回収も同じ期間でなされなくてはならない。そのため設計初期段階と引き続くファームウェア開発には、密接した連携が必要となる。
【０００３】
設計初期段階では、例えばｅ−ＳＩＭ社製（イスラエル）のＲａｐｉｄＰＬＵＳ（商品名）のようなプロトタイプ作成用のソフトウェアが用いられることがある。これらのソフトウェアはデモ用のアニメーションを生成することに主眼が置かれている。これは、デザイナーの興味がシステムの分析ではなく、製品形状と操作感覚に注がれることが多いためである。しかしながら、開発の視点から見ると、これらのプロトタイプ作成用ソフトウェアには２つの問題点がある。第１の問題点は、初期設計に続く開発作業のためのデータの共有と再利用の観点が欠けていることであり、第２の問題点は、質的な分析に対しての必要性が認識されていないことである。
【０００４】
したがって、ほとんどのプロトタイプ作成用ソフトウェアでは、自身のデータをデータ共有、再利用、質的分析のためのデータをエキスポートすることができない。さらにほとんどの製品仕様は、例えば、Ｍｉｃｒｏｓｏｆｔ Ｗｏｒｄ（商品名）で作成された文書のようなテキスト形式で書かれることが多く、形式的な表現ではないために自動的な検証を行うことはできない。よって設計初期段階においても、検証と再利用のための製品仕様の記述方法が必要であった。
【０００５】
また、プロトタイプ作成用ソフトウェアは、システムの振る舞いをアニメーションとして見せることに主眼が置かれている。しかしながら、そのデータは独自仕様であって公開されておらず、またデータ共有のための中間フォーマットなどは用いられていない。このためにデータの検証と再利用が妨げられている。
【０００６】
例えば、論文「Harel, D.: "Statecharts: A visual formalism for complex systems"; Science of Computer Programming 8 231-274 North-Holland (1987)」に記載されているプロトタイプ作成用ソフトウェアのように、いくつかのプロトタイプ作成用ソフトウェアでは、自身のデータをＳｔａｔｅｃｈａｒｔｓで出力することができる。またＧＵＩデザイン仕様にＳｔａｔｅｃｈａｒｔｓを用いるソフトウェアも幾つかある（例えば、論文「Horrocks, I.: "Constructing the User Interface with Statecharts"; Addison-Wesley, (1999)」）。Ｓｔａｔｅｃｈａｒｔｓは、状態遷移機械を表現するためには非常に有効であり、多くのツールが用意されている。
【０００７】
しかしながら、Ｓｔａｔｅｃｈａｒｔｓは図式表記であり、その形式化された表現については幾つかの提案、例えば、論文「Yacoub, S., Ammar, H.: "A Pattern Language of Statecharts"; PLoP-98 Conference (1998)」（非特許文献１）、論文「Costagliola, G. , Deufemia, V., Ferrucci, F. and Gravino, C.: "Implementing Statecharts using Extended Positional Grammars"; VLFM01, Symposium on Visual Languages and Formal Method, (2001)」（非特許文献２）があるが、矛盾したモデル記述を検証できる形式的な記述言語または数学的な表現形式は確立されていない。またＳｔａｔｅｃｈａｒｔｓには、排他的な状態遷移や、同期したイベント及び状態遷移を表現することはできない。
【０００８】
状態遷移機械の枠に縛られない概念的なモデルも提案されている。ＣＳＣＷ（Ｃｏｍｐｕｔｅｒ−ｓｕｐｐｏｒｔｅｄ Ｃｏｏｐｅｒａｔｉｖｅ Ｗｏｒｋ）の分野では、ＵＭＬに基づいた記述からＣＰＮ（Ｃｏｌｏｒｅｄ Ｐｅｔｒｉ Ｎｅｔ）の形式に変換する方法が提案されている（論文「Garrido, J., Gea, M.: "A Coloured Petri Net Formalisation for a UML-Based Notation Applied to Cooperative System Modeling"; Proceeding of 9th International Workshop, DSV-IS (2002)」（非特許文献３））。またこの領域では、論文「van der Veer, G. C., van Welie, M.:"Task Based Groupware Design: Putting theory into practice"; Proc. of Symposium on Designing Interactive Systems (DIS'2000), pp.326-337, (2000)」（非特許文献４）に記載されているＧＴＡ（Ｇｒｏｕｐ Ｔａｓｋ Ａｎａｌｙｓｉｓ）や、論文「Paterno, F.: "Model-based Design and Evaluation on Interactive Applications"; Springer-Verlag, (2000)」（非特許文献５）に記載されているＣＴＴ（ＣｏｎｃｕｒＴａｓｋＴｒｅｅｓ）なども提案されている。また、これらの表現形式からペトリネットへと変換する方式（ＩＣＯ ｆｏｒｍａｌｉｓｍ）も提案されている（例えば、論文「Palanque, P., Bastide, R.: "Synergistic modeling on task, users and systems using formal specification techniques"; Interacting with Computers 9, pp.129-153, (1997)」（非特許文献６））。
【非特許文献１】Yacoub, S., Ammar, H.: "A Pattern Language of Statecharts"; PLoP-98 Conference (1998)
【非特許文献２】Costagliola, G., Deufemia, V., Ferrucci, F. and Gravino, C. : Implementing Statecharts using Extended Positional Grammars; VLFM01, Symposium on Visual Languages and Formal Method, (2001)
【非特許文献３】Garrido, J., Gea, M.: "A Coloured Petri Net Formalisation for a UML-Based Notation Applied to Cooperative System Modeling"; Proceeding of 9th International Workshop, DSV-IS (2002)
【非特許文献４】van der Veer, G. C., van Welie, M.: "Task Based Groupware Design: Putting theory into practice"; Proc. of Symposium on Designing Interactive Systems (DIS'2000) , pp.326-337, (2000)
【非特許文献５】Paterno, F.: "Model-based Design and Evaluation on Interactive Applications"; Springer-Verlag, (2000).
【非特許文献６】Palanque, P., Bastide, R. : Synergistic modeling on task, users and systems using formal specification techniques; Interactign with Computers 9, pp.129-153, (1997)
【発明の開示】
【発明が解決しようとする課題】
【０００９】
本発明は、上述のような従来技術の問題点に鑑みてなされたものであり、ＵＭＬのような図式表記で表現された製品のＵＩ挙動仕様を自動的に検証できるＵＩ設計検証装置及び方法を提供することを目的とする。
【課題を解決するための手段】
【００１０】
請求項１の発明のＵＩ設計検証装置は、表明変換用公理群を保持する表明変換用公理データベースと、検証用公理群を保持する検証用公理データベースと、図式表記のＵＩ設計仕様を代数的表記に変換したその代数表記を入力する代数表記入力部と、入力された代数表記に対して、前記表明変換用公理データベースに登録されている表明変換用公理群の内の該当する公理を適用して表明を作成する表明変換用公理適用部と、前記表明変換用公理が適用された表明に対して、前記検証用公理データベースに登録されている検証用公理群の内の該当する公理を適用して表明の検証を行う検証用公理適用部と、前記検証用公理適用部にて検証した結果を出力する検証結果出力部とを備えたものである。
【００１１】
請求項２の発明は、請求項１のＵＩ設計検証装置において、前記検証用公理適用部には、完全性、強連結性、状態数の最小性についての公理を適用して検証する第１検証用公理適用部と、階層構造の一貫性についての公理を適用して検証する第２検証用公理適用部と、非決定性仕様の公理を適用して検証する第３検証用公理適用部とを備えたことを特徴とするものである。
【００１２】
請求項３の発明のＵＩ設計検証方法は、コンピュータを用いて、図式表記のＵＩ設計仕様を代数的表記に変換したその代数表記を入力する処理と、入力された代数表記に対して、表明変換用公理データベースに登録されている表明変換用公理群の内の該当する公理を適用して表明を作成する処理と、作成された表明に対して、検証用公理データベースに登録されている検証用公理群の内の該当する公理を適用して表明の検証を行う処理と、検証した結果を出力する処理とを実行するものである。
【００１３】
請求項４の発明は、請求項３のＵＩ設計検証方法において、前記検証用公理群の内の該当する公理を適用して表明の検証を行う処理には、完全性、強連結性、状態数の最小性についての公理を適用して検証する第１の検証と、階層構造の一貫性についての公理を適用して検証する第２の検証と、非決定性仕様の公理を適用して検証する第３の検証とを含むことを特徴とするものである。
【発明の効果】
【００１４】
本発明によれば、図式表記されたＵＩ挙動設計の自動的な検証が可能であり、ＵＩ挙動設計の効率化に寄与できる。
【発明を実施するための最良の形態】
【００１５】
以下、本発明の実施の形態を図に基づいて詳説する。
図１は本発明の１つの実施の形態のＵＩ設計検証装置の機能ブロック図である。本実施の形態のＵＩ設計検証装置は、Ｓｔａｔｅｃｈａｒｔｓ等の図式表記を代数的表記に変換したその代数表記を入力する代数表記入力部１、入力された代数表記に対して、表明変換用公理データベース５に登録されている表明変換用公理群の内の該当する公理を適用して表明を作成する表明変換用公理適用部２、この表明変換用公理が適用された表明に対して、検証用公理データベース６に登録されている検証用公理群の内の該当する公理を適用して表明の検証を行う検証用公理適用部３、この検証用公理適用部３にて検証した結果を表示し、またプリントアウト等を行う検証結果出力部４から構成されている。
【００１６】
検証用公理適用部３には、完全性、強連結性、状態数の最小性についての公理を適用して検証する第１検証用公理適用部３−１、階層構造の一貫性についての公理を適用して検証する第２検証用公理適用部３−２、そして非決定性仕様の公理を適用して検証する第３検証用公理適用部３−３を有している。また検証結果出力部４は、第１〜第３検証用公理適用部３−１〜３−３それぞれに対応して完全性、強連結性、状態数の最小性の検証結果を出力する第１検証結果出力部４−１、階層構造の一貫性の検証結果を出力する第２検証結果出力部４−２、そして非決定性仕様の検証結果を出力する第３検証結果出力部４−３を備えている。
【００１７】
上記実施の形態のＵＩ設計検証装置によるＵＩ設計検証方法のシーケンスは、図２に示す通りである。まず、Ｓｔａｔｅｃｈａｒｔｓ等の図式表記を代数的表記に変換し（ステップＳＱ１１）、ステップＳＱ１１で変換した代数的表記を表明変換用公理データベース５から該当する表明変換用公理を抽出して適用して表明に変換し（ステップＳＱ１２）、ステップＳＱ１２で変換した表明に検証用公理データベース６から該当する検証用公理を抽出して適用し、その検証結果を出力する（ステップＳＱ１３、ＳＱ１４、ＳＱ１５）。ステップＳＱ１３は完全性、強連結性、状態数の最小性についての公理の検証であり、ステップＳＱ１４は階層構造の一貫性についての公理の検証であり、ステップＳＱ１５は非決定性仕様の公理の検証である。
【００１８】
図３は、本実施の形態の代数的記述と評価の流れのシーケンス図である。図３はＩＤＥＦ０（アクティビティ・モデリング手法）形式で表現されている。四角い箱はアクティビティを示し、箱に左から入る矢印がアクティビティへの入力を、右側に出る矢印が出力を示している。他に、上から入る矢印が参照用のデータ、下から入る矢印がアクティビティで使用するメカニズムを示す。
【００１９】
設計者が作成したデザインを入力としてＵＩプロトタイプ／シナリオベースのＳｔａｔｅｃｈａｒｔｓを生成し（アクティビティＡ１１）、作成したＳｔａｔｅｃｈａｒｔｓを入力として公理系からデータを参照して公理を適用し（アクティビティＡ１２）、適用した公理を入力として検証用公理系からデータを参照して検証用公理を適用し、検証結果を出力する（アクティビティＡ１３）。
【００２０】
本発明では仕様の記述と検証に、製品仕様の数学的な記述表現と公理に基づく代数的な検証方法を用いる。これは、Ｃ．Ａ．Ｒ Ｈｏａｒｅによって提唱され計算機言語のＰＡＳＣＡＬの意味的な仕様をエミュレートする際に用いられた方法である。その詳しい方法は、論文「C. A. R. Hoare, N. Wirth: "An axiomatic definition of the programming language Pascal"; Acta Information 2, pp.335-355, (1973)」に記載されている。Ｍａｒｇｒｅｎは、論文「Margren, W.: "Formal Specification of Graphic Data Types"; ACM Transactions on Programming Languages and systems, vol.4, No.4, pp.687-710, (1982)」において、この方法論を２次元グラフィックディスプレイ上の２つの描画画像が等価であるかどうかの証明に用いている。この方法では検証は２つのステージで行われる。始めに代数的に表現された状態遷移機械の仕様から表明が生成される。「表明」とは、内部変数と状態遷移に関する事実の集まりであり、代数式による宣言の集成とも言える。「公理」は論理学的な取り扱いでは「自明の、もしくはあまねく認識されている真実」である。代数仕様と表明の間には１対１の対応関係がある。公理は、代数仕様から表明の変換を定義するルールであり、代数仕様が表明中に残す効果を表現している。全ての代数的仕様を公理によって変換すると、最終的な表明が残される。この作業によって状態遷移機械の数学的な表現が導出される。アクティビティＡ１３では、別の公理の集合が表明に適用されて仕様の検証が行われる。
【００２１】
本実施の形態では、ＵＩ設計の図式的表記であるＳｔａｔｅｃｈａｒｔｓから導出される基本的な有限状態機械を定義し検証するために、以下の情報を代数表現する。図４に状態遷移機械の代数表現の例を挙げる。「宣言開始」、「状態名宣言」、「イベント名宣言」、「アクション名宣言」、「大域的開始状態宣言」、「状態遷移宣言」、「状態遷移の階層構造定義」等である。状態遷移宣言は開始状態、終了状態、遷移を起動するイベント、同時に実行されるアクションの宣言なども行う。状態遷移の階層構造定義は、開始状態、サブ状態、終了状態、ヒストリインディケータの宣言を含む。階層構造の入れ子や並行サブプロセスなども表現する。
【００２２】
また図５に階層構造の代数表現の例を示している。スーパー状態ｓ３については、サブ状態がｓ５，ｓ６である。このＳｔａｔｅｃｈａｒｔｓに対する代数表現は、同図（ｂ）のように表現する。また、図６に並行動作の代数表現を例示している。複数の階層構造を併記して表現している。同図（ａ）のＳｔａｔｅｃｈａｒｔｓに対して同図（ｂ）のように代数表現する。
【００２３】
以下の説明では、ケーススタディとしてＶＷＣ（Ｖｉｓｕａｌ Ｗｉｒｅｌｅｓｓ Ｃｏｍｍｕｎｉｃａｔｏｒ）というデバイスのＵＩ設計検証を例示して説明する。ＶＷＣは無線ＬＡＮを経由して幾つかのリモートカメラを操作し、自身のＬＤＣモニタに映し出す小型の電子機器で、人間が直接行くには危険な作業現場などで有効と考えられる。他には、レジャー用途として非常に見晴らしが良いが一般の観光客が行けないような危険な場所（崖の突端や高層ビルの展望スペースの外側など）にリモートカメラを設置し、観光客がコントロールユニットを制御して自分の記念写真を撮り、撮影した写真を携帯電話に電子メールとして受け取る、といった用途で使われるものである。
【００２４】
図７に代数的仕様記述の例を示す。この記述は、ケーススタディとしたＶＷＣの仕様の一部である。それぞれの記述は、名前と引数の組み合わせで表現される。これは入力部１においてユーザーが行う（アクティビティＡ１１）。
【００２５】
次に図３におけるアクティビティＡ１２にて行う代数的仕様記述から表明への変換について説明する。始めに、表明変換用公理適用部２において、入力された代数的仕様記述から表明への変換を行う。代数的仕様記述を変換する際には、表明中の変数への代入などが行う。この変換が完了すると、最終的に残された表明が仕様全体を表現している。次に検証用公理適用部３にて、表明に対する検証を行う。この検証では、検証対象とするシステム内部の全ての変数を必要とするわけではなく、２つのステージ（アクティビティＡ１２、Ａ１３）で必要とされるものだけを取り扱う。従って表明で表現する変数などは最小限の範囲で取り扱う。
【００２６】
図８は、代数的仕様記述から表明への変換の一部を例示している。Ａｘ１とＡｘ２の式は、表明を生成するための公理の例である。図８では、代数“Ｓｔａｒｔ（ ）”を記述の開始の宣言として用いている。この代数に適用される公理Ａｘ１は、有限状態機械を定義する全ての変数の初期化を行う。Ａｘ１を代数式“Ｓｔａｒｔ（ ）”に適用すると、表明のテンプレートとして全ての変数が初期化された空リストの集合が生成される（アクティビティＡ２１）。他の公理では代数式に従って、このリストへ値を代入する形で表明の変換を定義する。
【００２７】
Ａｘ２は宣言された状態名を表明中の“ｓｔａｔｅＬｉｓｔ”に登録するために用いられる。引数ｓがａｔｏｍの場合（状態名が単独で登録される場合）は、その要素のみを含むリストが生成されて、“ｓｔａｔｅＬｉｓｔ”と結合される。図８では、下線をつけた状態名が“ｓｔａｔｅＬｉｓｔ”に付加されている（アクティビティＡ２２）。ここでは、リスト操作のための一般的な公理が必要なため、２つのステージの両方で利用できるように用意してある。“ＩｓＬｉｓｔ”と“Ｕｎｉｏｎ”などの公理はリスト操作用として予め用意してある。
【００２８】
表明検証用公理適用部３による表明の検証は、表明をそのままの形式で検証することは不可能なので、検証用の公理のグループをデータベース６に用意している。検証用の公理は、表明を入力として特定の状況を満たしているかどうかを判断するための検証結果を出力する。
【００２９】
一般にイベントは自身の名前と引数、以前に実行されたイベントによって累積した結果によりシステムの変数の生成もしくは変更を引き起こす。上記の公理は、イベントに対応して表明を生成するので、全てのイベント系列を表明に変換し、得られた表明をシステムの最終状態の表現とし、本実施の形態ではこれを検証結果として出力する。
【００３０】
図９はＶＷＣデバイスのＳｔａｔｅｃｈａｒｔｓを示している。このチャートは、状態遷移のトップレベルを示している。図１０には並行サブプロセスの部分を示してある。図９のチャートにおいて、“Ｐｏｗｅｒ＿Ｏｆｆ”が初期状態であり、電源が入れられると制御ユニットはリモートカメラをコントロールすることが可能となる。図中のアスタリスク（＊）は、並行サブ状態が存在することを示している。
【００３１】
用意してある公理には以下の３種類がある。（１）“Ｓｔａｒｔ（ ）”で用いる初期化用公理、（２）代数的表現に１対１に対応して表明を生成するための公理、（３）検証に用いるための公理である。このうち、（１）と（２）の公理を参照して表明を生成するが、これについて説明する。本実施の形態では、代数的仕様記述を関数呼び出しとして使用し表明を生成する。代数的仕様記述は“Ｓｔａｒｔ（ ）”から始まり、その内容に従ってシステムの初期化を行う。表明に含まれて検証で用いられる情報のリストを以下に挙げる。「状態名を列挙したリスト」、「イベント名を列挙したリスト」、「アクション名を列挙したリスト」、「全ての状態遷移を列挙したリスト」、「状態の階層構造に関する定義を列挙したリスト」、「遷移する可能性のある状態のリスト、またそれらの直積集合」、「イベントとアクションの直積集合」である。
【００３２】
本実施の形態では、状態遷移機械の検証のために、上記（３）の公理を用いて表明を検証するために、図１１に示すような完全性、強連結性、状態数の最小性を検証する第１の検証（ステップＳＱ１３）、図１２〜図１４に示すような階層構造記述の一貫性と並行状態の記述を検証する第２の検証（ステップＳＱ１４）、そして図１５に示すような非決定性問題を検証する第３の検証（ステップＳＱ１５）を実行する。
【００３３】
図１１に示したように、ステップＳＱ１３の完全性、強連結性、状態数の最小性の検証は次の通りである。
【００３４】
［完全性］完全性の検証では、全ての状態から少なくとも一つの他の状態への遷移が存在するかどうかを検証する。このために、公理中では、各々の状態からの遷移が定義されているかどうかを確認する。
【００３５】
［強連結性］強連結性の検証では、任意の状態ｕ及びｖの間での状態遷移と、その逆の遷移が可能であるかどうかの検証を行う。公理中では、状態名の直積集合を元に、ある状態から他の状態への遷移が可能であるかどうかを探索する。
【００３６】
［状態数の最小性］イベントとアクションの組み合わせから決まる最小限の個数の状態遷移を持つべき、同じイベントとアクションの組み合わせで並行した状態遷移が定義されている場合は、状態遷移の設計が不完全で、後述する非決定性問題を起こす可能性がある。このような場合、並行サブ状態などを用いて、イベントとアクションの組み合わせが単一の状態遷移を持つように、遷移の構造を見直す必要がある。そこで、公理では遷移を起こすイベントとアクションの組み合わせの数で検証する。
【００３７】
ステップＳＱ１４の階層構造の検証では、図１２〜図１４に示し、以下に列挙するように細分化された詳細な項目に関して行う。１つめの項目としては、サブ／スーパーの状態の関係（階層構造の定義）が一貫して、ツリー構造となっているか、２つめの項目としては、サブ状態からスーパー状態へ戻る遷移が少なくとも一つ定義されているかどうか。３つめの項目としては、スーパー状態への遷移が定義されているときに、その中で初期状態が宣言されているか、４つめの項目としては、終了状態への遷移が定義されているときに、終了状態に対応する外部の状態が宣言されているかどうか、５つめの項目としては、初期状態／終了状態への直接の遷移が定義されていないかどうか、６つめの項目としては、サブ状態からの遷移が一定の方式に従っているかどうかを検証する。
【００３８】
図１５に示したように、ステップＳＱ１５の非決定性仕様の検証は、階層構造の中で２つ以上の遷移が、同じイベント／アクションの組み合わせで発生する場合、その仕様は非決定性問題（矛盾した仕様）を含んでいる可能性がある。例えば、同じイベントによって階層構造の外側への遷移と、階層構造の内側での遷移が定義されているような場合である。このような状況を検出するために、本発明では階層構造中での同じイベントによる遷移をチェックし、必要であれば警告を出す。
【００３９】
本実施の形態によれば、特定の言語に依存しない特徴がある。また、静的な仕様と動的なイベント系列を入力とした仕様の検証の両方に適用できる特徴もある。さらに、有限状態機械に適用可能な公理の標準的な集合を定義できる特徴もある。
【実施例１】
【００４０】
次に、本発明の実施例について説明する。ＶＷＣデバイスのＵＩ挙動設計のため図１６、図１７に示したＳｔａｔｅｃｈａｒｔｓを作成し、これに対して、図１８に示す代数表現を作成して入力し、ＵＩ挙動の検証実験を実施した。この検証結果は、図１９〜図２１の検証結果１〜検証結果３に示すものであった。すなわち、図１９の検証結果１に示したように、サブ状態のさらに下で「待機中」という同じ状態名が出てくることを発見した。また、図２０の検証結果２に示したように、システム全体での初期状態の指定が欠けている点を発見した。つまり、“電源ＯＮ”中のどれが初期状態になるかが不明であることを発見した。この場合、四角で囲った「待機中」のサブ状態には開始を示すマークが付加されるべきであるのが、欠落しているのである。さらに、図２１の検証結果３に示したように、開始状態として定義された状態への複数の遷移を発見した。これは、他のサブ状態で同じ状態名「待機中」を使っている場合にも起こるものである。
【実施例２】
【００４１】
図２２、図２４に示すようなＳｔａｔｅｃｈａｒｔｓに対して代数表現を作成し、本実施の形態のＵＩ設計検証装置に入力し、非決定性仕様を検証した。その結果として、図２３、図２５の検証結果を得た。これにより、図２２、図２３よりサブ状態関係の状態ｓ２とｓ１からの同一のイベントによる遷移があるので、これを非決定性遷移として警告を発することができることを確認できた。また図２４、図２５より並行関係中で同一イベントによる外部への遷移がある場合、非決定性遷移として警告を発することが確認できた。
【図面の簡単な説明】
【００４２】
【図１】本発明の一つの実施の形態のＵＩ設計検証装置の機能ブロック図。
【図２】上記実施の形態のＵＩ設計検証装置のＵＩ設計検証動作のフローチャート。
【図３】上記実施の形態のＵＩ設計検証装置が実行するＵＩ設計検証動作のフローチャート（ＩＤＥＦ０形式による）。
【図４】上記実施の形態のＵＩ設計検証装置で入力する状態遷移機械の代数表現例１の説明図。
【図５】上記実施の形態のＵＩ設計検証装置で入力する状態遷移機械の代数表現例２の説明図。
【図６】上記実施の形態のＵＩ設計検証装置で入力する状態遷移機械の代数表現例３の説明図。
【図７】上記実施の形態のＵＩ設計検証装置に入力するＶＷＣデバイスのＵＩ設計仕様の代数表現例の説明図。
【図８】上記実施の形態のＵＩ設計検証装置による具体的なＵＩ設計検証動作のフローチャート（ＩＤＥＦ０形式による）。
【図９】上記実施の形態のＵＩ設計検証装置にて検証対象としたＶＷＣデバイスのＵＩ挙動仕様のトップレベルのＳｔａｔｅｃｈａｒｔｓの図。
【図１０】上記実施の形態のＵＩ設計検証装置にて検証対象としたＶＷＣデバイスのＵＩ挙動仕様の並行サブプロセスのＳｔａｔｅｃｈａｒｔｓの図。
【図１１】上記実施の形態のＵＩ設計検証装置にて検証する第１の検証項目の説明図。
【図１２】上記実施の形態のＵＩ設計検証装置にて検証する第２の検証項目の説明図（その１）。
【図１３】上記実施の形態のＵＩ設計検証装置にて検証する第２の検証項目の説明図（その２）。
【図１４】上記実施の形態のＵＩ設計検証装置にて検証する第２の検証項目の説明図（その３）。
【図１５】上記実施の形態のＵＩ設計検証装置にて検証する第３の検証項目の説明図。
【図１６】上記実施の形態のＵＩ設計検証装置にて検証対象とした実施例１のＶＷＣデバイスのＵＩ挙動仕様のトップレベルのＳｔａｔｅｃｈａｒｔｓの図。
【図１７】上記実施の形態のＵＩ設計検証装置にて検証対象とした実施例１のＶＷＣデバイスのＵＩ挙動仕様の並行サブプロセスのＳｔａｔｅｃｈａｒｔｓの図。
【図１８】上記実施の形態のＵＩ設計検証装置にて検証対象とした実施例１のＶＷＣデバイスのＵＩ挙動仕様の代数表現の一部を示す説明図。
【図１９】上記実施の形態のＵＩ設計検証装置にて検証対象とした実施例１のＶＷＣデバイスのＵＩ挙動仕様に対する検証結果１の説明図。
【図２０】上記実施の形態のＵＩ設計検証装置にて検証対象とした実施例１のＶＷＣデバイスのＵＩ挙動仕様に対する検証結果２の説明図。
【図２１】上記実施の形態のＵＩ設計検証装置にて検証対象とした実施例１のＶＷＣデバイスのＵＩ挙動仕様に対する検証結果３の説明図。
【図２２】上記実施の形態のＵＩ設計検証装置にて検証対象とした実施例２のＵＩ挙動仕様その１のＳｔａｔｅｃｈａｒｔｓの図。
【図２３】上記実施例２のＵＩ挙動仕様その１に対する検証結果の説明図。
【図２４】上記実施の形態のＵＩ設計検証装置にて検証対象とした実施例２のＵＩ挙動仕様その２のＳｔａｔｅｃｈａｒｔｓの図。
【図２５】上記実施例２のＵＩ挙動仕様その２に対する検証結果の説明図。
【符号の説明】
【００４３】
１ 代数表記入力部
２ 表明変換用公理適用部
３ 検証用公理適用部
３−１ 第１検証用公理適用部
３−２ 第２検証用公理適用部
３−３ 第３検証用公理適用部
４ 検証結果出力部
４−１ 第１検証結果出力部
４−２ 第２検証結果出力部
４−３ 第３検証結果出力部
５ 表明変換用公理データベース
６ 検証用公理データベース
【特許請求の範囲】
【請求項１】
表明変換用公理群を保持する表明変換用公理データベースと、
検証用公理群を保持する検証用公理データベースと、
図式表記のＵＩ設計仕様を代数的表記に変換したその代数表記を入力する代数表記入力部と、
入力された代数表記に対して、前記表明変換用公理データベースに登録されている表明変換用公理群の内の該当する公理を適用して表明を作成する表明変換用公理適用部と、
前記表明変換用公理が適用された表明に対して、前記検証用公理データベースに登録されている検証用公理群の内の該当する公理を適用して表明の検証を行う検証用公理適用部と、
前記検証用公理適用部にて検証した結果を出力する検証結果出力部とを備えたＵＩ設計検証装置。
【請求項２】
前記検証用公理適用部には、完全性、強連結性、状態数の最小性についての公理を適用して検証する第１検証用公理適用部と、階層構造の一貫性についての公理を適用して検証する第２検証用公理適用部と、非決定性仕様の公理を適用して検証する第３検証用公理適用部とを備えたことを特徴とする請求項１に記載のＵＩ設計検証装置。
【請求項３】
コンピュータを用いて、
図式表記のＵＩ設計仕様を代数的表記に変換したその代数表記を入力する処理と、
入力された代数表記に対して、表明変換用公理データベースに登録されている表明変換用公理群の内の該当する公理を適用して表明を作成する処理と、
作成された表明に対して、検証用公理データベースに登録されている検証用公理群の内の該当する公理を適用して表明の検証を行う処理と、
検証した結果を出力する処理とを実行することを特徴とするＵＩ設計検証方法。
【請求項４】
前記検証用公理群の内の該当する公理を適用して表明の検証を行う処理には、完全性、強連結性、状態数の最小性についての公理を適用して検証する第１の検証と、階層構造の一貫性についての公理を適用して検証する第２の検証と、非決定性仕様の公理を適用して検証する第３の検証とを含むことを特徴とする請求項３に記載のＵＩ設計検証方法。
【請求項１】
表明変換用公理群を保持する表明変換用公理データベースと、
検証用公理群を保持する検証用公理データベースと、
図式表記のＵＩ設計仕様を代数的表記に変換したその代数表記を入力する代数表記入力部と、
入力された代数表記に対して、前記表明変換用公理データベースに登録されている表明変換用公理群の内の該当する公理を適用して表明を作成する表明変換用公理適用部と、
前記表明変換用公理が適用された表明に対して、前記検証用公理データベースに登録されている検証用公理群の内の該当する公理を適用して表明の検証を行う検証用公理適用部と、
前記検証用公理適用部にて検証した結果を出力する検証結果出力部とを備えたＵＩ設計検証装置。
【請求項２】
前記検証用公理適用部には、完全性、強連結性、状態数の最小性についての公理を適用して検証する第１検証用公理適用部と、階層構造の一貫性についての公理を適用して検証する第２検証用公理適用部と、非決定性仕様の公理を適用して検証する第３検証用公理適用部とを備えたことを特徴とする請求項１に記載のＵＩ設計検証装置。
【請求項３】
コンピュータを用いて、
図式表記のＵＩ設計仕様を代数的表記に変換したその代数表記を入力する処理と、
入力された代数表記に対して、表明変換用公理データベースに登録されている表明変換用公理群の内の該当する公理を適用して表明を作成する処理と、
作成された表明に対して、検証用公理データベースに登録されている検証用公理群の内の該当する公理を適用して表明の検証を行う処理と、
検証した結果を出力する処理とを実行することを特徴とするＵＩ設計検証方法。
【請求項４】
前記検証用公理群の内の該当する公理を適用して表明の検証を行う処理には、完全性、強連結性、状態数の最小性についての公理を適用して検証する第１の検証と、階層構造の一貫性についての公理を適用して検証する第２の検証と、非決定性仕様の公理を適用して検証する第３の検証とを含むことを特徴とする請求項３に記載のＵＩ設計検証方法。
【図１】
【図２】
【図３】
【図４】
【図５】
【図６】
【図７】
【図８】
【図９】
【図１０】
【図１１】
【図１２】
【図１３】
【図１４】
【図１５】
【図１６】
【図１７】
【図１８】
【図１９】
【図２０】
【図２１】
【図２２】
【図２３】
【図２４】
【図２５】
【図２】
【図３】
【図４】
【図５】
【図６】
【図７】
【図８】
【図９】
【図１０】
【図１１】
【図１２】
【図１３】
【図１４】
【図１５】
【図１６】
【図１７】
【図１８】
【図１９】
【図２０】
【図２１】
【図２２】
【図２３】
【図２４】
【図２５】
【公開番号】特開２００６−２８５６２６（Ｐ２００６−２８５６２６Ａ）
【公開日】平成１８年１０月１９日（２００６．１０．１９）
【国際特許分類】
【出願番号】特願２００５−１０４５０３（Ｐ２００５−１０４５０３）
【出願日】平成１７年３月３１日（２００５．３．３１）
【新規性喪失の例外の表示】特許法第３０条第１項適用申請有り ２００４年１０月６日 ヒューマンインターフェース学会発行の「ヒューマンインターフェースシンポジウム２００４ 論文集」に発表
【出願人】（５０５１１９１６２）学校法人 北海学園 (1)
【出願人】（５０５１１９４５０）
【Ｆターム（参考）】
【公開日】平成１８年１０月１９日（２００６．１０．１９）
【国際特許分類】
【出願日】平成１７年３月３１日（２００５．３．３１）
【新規性喪失の例外の表示】特許法第３０条第１項適用申請有り ２００４年１０月６日 ヒューマンインターフェース学会発行の「ヒューマンインターフェースシンポジウム２００４ 論文集」に発表
【出願人】（５０５１１９１６２）学校法人 北海学園 (1)
【出願人】（５０５１１９４５０）
【Ｆターム（参考）】
[ Back to top ]