ホーム ARMソリューション 製品 サポート 技術情報 ダウンロード IARについて お問合せ マイページ
評価キット コンパイラ・デバッガ RTOS / ミドルウェア ステートマシン設計ツール ICE ソリューション ご注文について
 
製品ニュース
製品パッケージ
コンポーネント
Navigator（ナビゲーションツール）
Designer（モデル設計ツール）
Validator（機能テストツール）
Verificator（形式テストツール）
Prototyping（プロトタイプテストツール）
Coder（コード生成ツール）
Integration（ターゲットの構築）
Documenter（レポート作成ツール）
C-SPY連携
ユーザガイド
Webinar/video recordings
オンラインデモ
 
 
製品   >   ステートマシン設計ツール   >   コンポーネント   >   Verificator（形式テストツール）   >  

Verificator （形式テストツール）
ステートマシン設計モデルやアプリケーションが、次のような問題のありそうなプロパティをいずれも含んでいないことをどのようにテストしますか？

  • ステート、ローカル、システム範囲でのデッドロック
  • ステート間トランジション衝突
  • 到達できないステート(環境領域からのあらゆるイベントシーケンスによっても入ることができないステート)
  • 未使用イベント、シグナル(システムに影響を与えないトリガ)
  • 未使用トランジション (システムへのあらゆるイベントシーケンスに関わらず活性化しないトランジション)
  • 未使用アクション、代入式
  • 未使用変数、パラメータ、定数

これらのプロパティがアプリケーション中に存在する場合、潜在的な不整合性のある設計の兆候、あるいはより悪い致命的な論理上の欠陥を備えた設計と言えます。

ステート空間の爆発的増加との戦い

それほど複雑なアプリケーションでなくても、上記のプロパティのすべてに対して、手動で完全にテストする作業は大変です。あるいは事実上、不可能と言えるかも知れません。従来のブラックボックスあるいはホワイトボックスを使用する場合、許容される時間内ですべての設計エレメントの１００%テストカバレッジを達成するアプローチは一般的には不可能です。同じアプリケーション内のステートマシンあるいまステートマシンの1つのシステム中のステート、イベント、トランジションの組合せ数は、ステートマシンまたはステートマシンのシステムが大きくなるとともに、急速に増大します。

形式検証とモデル駆動設計

テストジレンマから脱出するためには、形式検証に基づいた方式で、従来のテスト方針を補完することです。設計モデルは定理証明とグラフ理論に基づいた方式を利用して、純粋に形式上の視点から見てチェックされます。

visualSTATE verificatorはこれらの形式上の方法を利用し、システムの非常に効率的な抽象的な内部表現とそれらを組み合わせます。したがって、形式検証技術に通常関連した時間やメモリ消費量をそれにより徹底的に削減します。visualSTATE verificatorで、設計初期フェーズでの不具合を、この方法で発見することができます。このような不具合は実機テストで検出するのは不可能です。

カスタム設計プロパティの検証

上記のすべての設計プロパティのすべてを形式テストすることに加えて、 visualSTATE verificaftorは設計のカスタムプロパティをテストすることができます。これは、アプリケーション設計と並行して1つ以上のUMLステートマシンで必要な検証プロパティを表現することにより達成されます。
(例えば「システムがStateAからStateBを経由しStateCへ遷移することがあるか？」、「StateMachine1がStateDの状態であるとき、同時にStateMachine2がStateEの状態であることがありまか？」など)形式検証は設計モデル上で行なわれるので、全開発サイクルのいたる所で行なうことができます。このように、利用者が困難な方法で発見するまで待つ事なく、エラーをすぐに見つけることが可能です。
問題のステートがステートマシンモデルの中で発見される場合、システムがこのステートへどのように遷移することができるか示すイベントシーケンスは、自動的に生成することができます（到達可能なステートの場合）。このイベントシーケンスは、後で、機能テストやアプリケーション検証
の入力テストベクタとして利用できます。生成されたイベントシーケンスの重要なプロパティは、それがそのステートに達するできるだけ短いシーケンスであるということです。

Verificator（形式テストツール）と強力なシミュレータデバッガを有するValidator（機能テストツール）を組み合せ、繰り返しテスト、検証することにより、設計モデルが実機で正常に実行可能であることを保証できます。

例1:ステートデッドエンド

この例はデッドエンドを含んだ1つのステートマシンを示します。
ステートデッドエンドを含んだvisualSTATEモデル
 
visualSTATEは上図の設計において次の検証結果を報告します:
 
CHECKING FOR STATE DEAD ENDS
State dead end(s) (Warnings):
B
 
ステートデッドエンドとは一旦そこに入ると出ることができないステートです。ステートマシンがリセットされるまで、ステートマシンはそのステートに止まります。
ステートBはステートを出て他のステートに行くトランジションを持たないので、ステートデッドエンドです。

例2:ローカルデッドエンド

この例はシステムを2つのステートマシンM0およびM1で示します。
M0はローカルデッドエンド{B(C})を持っています。
M1はローカルデッドエンド{B(C})を持っています。
M0
M1
2つのステートマシンM0、M1から構成されるvisualSTATEシステム。
M0はローカルデッドエンド{B(C})を持っています。
M1はローカルデッドエンド{B、C}、Dを持っています。
 
visualSTATEは上図の設計において次の検証結果を報告します:
 
CHECKING FOR LOCAL DEAD ENDS
Local dead end(s) for 'M_0_M0' (Warning):

Local dead end 1:
B
C

Local dead end(s) for 'M_1_M1' (Warning):

Local dead end 1:
D

Local dead end 2:
B
C
 
A local dead end is a combination of states from one or more state machines that prevents a state machine from changing state. Please check transitions with state conditions.
このシステムは3つのローカルデッドエンドを持っています。イベント：Event1がイベント：Event2の前に生じれば、システムはステート{B、C}に入り、ステートマシン：M0とステートマシン：M1の両方がローカルデッドエンドとなります。Event2が最初に生じれば、ステートマシン：M1はローカルのデッドエンドDに入るでしょう。

すべてのステートデッドエンドとシステムデッドエンドがローカルデッドエンドにもなるということに注意してください。ガード式を含んでいないシステムでは、デッドエンドは、ステート条件によって最も多く引き起こされます。

例3:システムデッドエンド

このシステムは2つのステートマシンM0およびM1から構成されます。M1は1つのシステムデッドエンドを持っています。
M0
M1
1つのシステム・デッドエンド{B、F}を含んだvisualSTATEシステム。
 
visualSTATEは上図の設計において次の検証結果を報告します:
 
CHECKING FOR SYSTEM DEAD ENDS

Printing system dead end(s) (Warnings):

System dead end 1:
B
F
 
A system dead end is a combination of states from all the state machines, which prevents the complete system from changing state. Please check transitions with state conditions.
Verficatorは、ステート{B、F}がシステムデッドエンドであることを見つけます。

Event1とEvent3の両方がEvent3とEvent4の前に生じる場合、任意のイベントシーケンスでシステムデッドエンドになります。

例4:トランジション衝突

次の例は、トランジション衝突を持ったた簡単なvisualSTATEシステムを示します。
トランジション衝突を持った簡単なシステム。
 
visualSTATEは上図の設計において次の検証結果を報告します:
 
CHECKING CONFLICTS

Conflicting Transitions: (Error)
A: Event1() /
-> B

A: Event1() /
-> C
 
If guard expressions are used in the transitions above please check
these guard expressions manually to ensure that they are mutually
exclusive.
イベント：Event1が発生したとき、システムは衝突し、ステートBもしくはステートCどちらに入って良いかわからくなります。衝突はガード式やステート条件の追加または他のイベントをトリガとしてトランジションのうちの1つを起こすことによって解決できるかもしれません、。

例5:強制ステートアクションと衝突

次の例は、強制ステートアクションがどのようにトランジションの衝突を引き起こすかを示します。このシステムは、ステートマシン：M0(ステートA、Bを含む）およびステートマシン：M1(ステートC、D、Eむ)から構成されます。
M0
M1
2つのステートマシンM0とM1から構成されるvisualSTATEシステム。
 
visualSTATEは上図の設計において次の検証結果を報告します:
 
CHECKING CONFLICTS

Conflicting Transitions: (Error)
A:
Event1() / D
-> B

C:
Event1() /
-> E
 
If guard expressions are used in the transitions above please check
these guard expressions manually to ensure that they are mutually
exclusive.
AからBのトランジションの強制ステートアクションでトランジションの衝突がステートマシン：M1で発生します。ステートマシン：M1は、イベント：Event1が発生したときステートDかステートEのどちらに入って良いかわかりません。

例6:階層構造と衝突

階層システムで衝突を検知するのは難しいかもしれません。ここに表示された例は単純ですが、ネストが深く最上位レベルでトランジションの衝突が起こったことを想定してください。
衝突を持った階層システム。
 
visualSTATEは上図の設計において次の検証結果を報告します:
 
Conflicting Transitions: (Error)
A:
Event1() /
-> B

C:
Event1() /
-> D
 
If guard expressions are used in the transitions above please check
these guard expressions manually to ensure that they are mutually
exclusive.
イベント：Event1が発生した場合、2つのトランジション：A ->BおよびC ->Dが衝突します。システムはステートA、DまたはステートBのどちらに入るべきか分かりません。
 
 

ダウンロード
 

テクノロジ
 

詳細情報
 
 
 
Design your Chronos watch from TI with IAR visualSTATE.   >>