Universal Pattern

Universal Patternは、要求を形式化するための言語です。グラフィカルかつ直感的な操作でご利用いただけます。

要求を形式化するための言語は従来、専門的で難解なものでした。BTC Embedded Systems AGはテスト・検証の高度な自動化を実用化するために、要求の形式化を日々のエンジニアリングで誰もが使えるほど容易で身近なものにしたいと考え、組み込みシステムの要求の記述に特化することで直感的かつ可読性の高い形式言語を開発し発展させて参りました。

当社設立初期に開発され形式検証の実用化に貢献したPattern、そしてこれを発展させた現行のSimplified Universal Patternを経て、2020年末にはUniversal Patternのリリースを控えています。これらの言語は、難解な形式手法の専門知識を持たずとも読み書きが可能です。

Univeral Pattern

Universal Patternは要求の形式化に特化して開発された言語です。設計や実装に活用されている言語とは異なり、要求を読み書きすることに対して最適化されています。BTC EmbeddedPlatformのテスト・検証の高度な自動化の多くは、Universal Patternを利用して実現されています。Universal Patternは数学的な裏付けを持ってシンタックスとセマンティクスが完全に定義された形式言語です。しかしこの難解な裏付けを理解する必要はありません。ユーザが直接触れるインタフェースには直感的かつ可読性の高いグラフィカルな表現を採用しています。

 

トリガフェーズとアクションフェーズ

Universal Patternでは上図のように、各要求をトリガフェーズ(Trigger)とアクションフェーズ(Action)に分けて記述します。トリガフェーズが満たされたら、指定した時間以内にアクションフェーズが満たされなければなりません。指定したタイミングでアクションが発生しなければ要求違反と判定されます。これらの各フェーズの中にはそれぞれ時間を伴った条件を設定できます。例えば、「あるボタンが一定時間継続して押下されたら」といった条件が設定されます。

上図の例では、「シフトポジションがDに入った状態でACCモードに設定されたのち、SETボタンが押されたら、追従モードを開始しなければならない。」という要求をUniversal Patternで形式化しています。

各フェーズには、この例にあるような条件に加えて、評価の開始イベント、終了イベント、脱出イベントなどを設定することもできます。また、トリガフェーズ、アクションフェーズはそれぞれ複数追加することができます。そのため、シンプルな要求から複雑な要求まで表現することが可能です。Universal Patternの文法の詳細はBTC EmbeddedPlatformの評価版を通じてご確認いただけます。ユーザビリティの確認や各種自動検証も含めてぜひご評価ください。

マクロ

各フェーズで利用される頭に$が付いた文字列(例えば、$シフトポジションがD)は、マクロと呼ばれます。マクロの名称は要求内の単語または短い文章を使って与えられます。一方でマクロの定義は、検証対象のモデルやコードのインタフェース名を使って与えられます。例えば、「$シフトポジションがD」の定義は、shift_pos == 3のようにして与えられます。基本的な要求の読み書きにはマクロを使った人間に理解し易い表記が用いられ、検証時にはツールがマクロの定義に基づいた解釈を自動で行います。

マクロは複数の要求間で共通で利用することやマクロ同士の入れ子関係を表現することができることから、マクロの利用は要求間の依存関係の整理に繋がります。 要求では抽象的な表現になっている単語がモデルでは具体的な信号や状態の組み合わせで表現されている場合の、表現のギャップもこのマクロの定義を通じて埋められます。個別のモデルに合わせて要求の表現を変更する必要はありません。例えば下図の例では、「SETボタンを押す」というマクロに対してfs(set_btn)という定義が与えられています。これはset_btnと名付けられたBooleanの信号の立ち下がりエッジを以てSETボタンが押されたと見做すことを示しています。しかし実際の開発ではしばしば要求を記述する段階ではボタンの押下判定に関して立ち上がりエッジを取るのか、立ち下がりエッジを取るのかまで具体的には決まっていないことがあります。今回の例でも要求にはSETボタンを押すとしか記載はなく、立ち下がりエッジを用いることは明示されていません。その場合は設計や実装が進む過程でこれが決定されますので、検証時には考慮しなければなりません。マクロの定義を用いることで要求にも検証対象にも変更を加えることなく要求と検証対象間のギャップを埋めることが可能となります。

要求カバレッジ

テストの完全性を要求の観点から評価する要求カバレッジのメトリクスはUniveral Patternに基づいて定義されています。Universal Patternで要求を記述するだけで、フォーマルテスト実行時に要求カバレッジが自動測定されるようになります。

 

Simplified Universal Pattern

Simplified Universal PatternはEP2.7以前で利用されている言語です。Universal Patternの簡易版で、トリガフェーズとアクションフェーズを最大でも一つずつしか設定することができません。Universal Patternほどの表現能力はありませんが、実践における多くの要求を形式化することができる十分に実用的かつ実績を持った言語です。