Requirements Analysis パッケージ

BTC EmbeddedPlatformの要求のCCC分析は、モデルもコードも必要なく、要求群のみでの早期検証を可能にします。

Requirements Analysis パッケージ

BTC EmbeddedPlatformのRequirements Analysis パッケージは、要求群の完全性(Completeness)、正確性(Correctness)、一貫性(Consistency)を評価します。モデリング前の、システム要求群のみの段階で要求群の矛盾や抜け漏れを検出できることから、モデルよりもさらに早期の検証を可能にします。 

Requirements Analysisパッケージ

サポートするユースケース

*1 Formal Specificationパッケージの機能はすべて含まれます。

追加可能なアドオン

 

要求のCCC分析

開発の起点であり、開発プロセス全体を通じて利用される要求群には高い質が求められます。一方で、いくつもの研究によって現状の不具合の多くは要求に由来するものであると特定されています。CCC分析は、要求群の完全性(Completeness)、正確性(Correctness)、一貫性(Consistency)の評価を通じて、要求に潜在する不具合を設計開始前に検出します。

 

要求群の完全性(Completeness)チェック

要求群の完全性(Completeness)チェックでは、Universal Patternで形式化された要求群を分析し、要求の不足を検出します。分析はそれぞれの要求に対して行われます。分析対象の要求を、その他の要求すべてに違反しない範囲で満たすことが可能であれば、その要求は完全と判定されます。要求が完全と判定された場合は分析対象の要求を満たす要求シミュレーション例(トレース)が提示されます。逆に要求が不完全と判定された場合は、追加の要求を必要とすることが判明します。

この分析ではテストケースを与える必要はありません。要求群を制約条件として、取りうるすべての入力値を対象に自動で分析が行われます。入力に対する出力の振る舞いは、正確性チェックの要求シミュレーションと同じく形式化された要求群を制約条件としてその範囲内で決定されます。要求は抽象的であるため一つの入力に対して取りうる出力値が一つとは限りませんが、要求群に違反しない範囲で可能な出力値全てが評価されます。しかし、要求に出力の振る舞いが記載されていない場合は、その出力は動作しないものとして取り扱われます。

このチェックは、その他の要求に違反せずに分析対象の要求を満たすことが可能であることを示しますが、分析対象の要求に違反するトレースが存在しないことを証明するものではありません。この証明は要求群の一貫性(Consistency)チェックの対象です。

要求群の正確性(Correctness)チェック

BTC EmbeddedPlatformの要求の正確性(Correctness)チェックでは、Universal Patternを用いて形式化された要求群によるシミュレーションが行えます。Requirements-basedテストのように、テストケースを記入してシミュレーションを実行すると、BTC EmbeddedPlatformは形式化された要求群を制約条件としてその範囲内で可能な振る舞いを分析し、各シミュレーションステップ毎に出力値を確定していきます。この出力値はどの要求にも違反しない値のみが採用されます。要求に違反する場合はシミュレーションエラーとなります。こうして要求シミュレーションで得られた出力値は、実装可能なソフトウェアの振る舞いの一例を表します。これをエンジニアの方の想定している振る舞いと比較し、合致していれば合格、合致していなければいずれかの要求に(もしくはいくつかの要求の組み合わせに)意図を正しく反映できていないか要求が不足していることが明らかとなります。

シミュレーション結果には各要求のステータスが含まれます。下図の例ではFulfilledのみが表示されていますが、さらにトリガフェーズが満たされたタイミングやアクションフェーズが満たされたタイミングなどの詳細を表示することも可能です。もし意図通りの振る舞いを得られなかった場合には、この情報を頼りに要求のデバッグを行うことができます。

要求群の一貫性(Consistency)チェック

要求群の一貫性(Consistency)チェックでは、Universal Patternで形式化された要求群を分析し、要求間の矛盾を検出します。分析はそれぞれの要求に対して行われます。分析対象の要求を満たすときに他の要求を違反することがあればそれを矛盾として検出します。矛盾が検出されなかった場合は要求群は如何なる入力に対しても互いに矛盾しない(一貫している)ことが証明されます。逆に矛盾が一つでも存在する場合にはそれが検出され、矛盾を再現するシミュレーション例が提示されます。矛盾が検出された場合は、分析対象の要求を満たすときに他の要求に違反し得ることが判明します。さらにBTC EmbeddedPlatformの一貫性(Consistency)チェックでは、要求が大量の場合にも効率的に矛盾の原因の特定と修正を行えるよう、矛盾を引き起こすために必要最小限の要求の組み合わせを提示します。

この分析ではテストケースを与える必要はありません。要求群を制約条件として、取りうるすべての入力値を対象に自動で分析が行われます。入力に対する出力の振る舞いは、要求シミュレーションと同じく形式化された要求群を制約条件としてその範囲内で決定されます。要求は抽象的であるため一つの入力に対して取りうる出力値が一つとは限りませんが、要求群に違反しない範囲で可能な出力値全てが評価されます。しかし、要求に出力の振る舞いが記載されていない場合は、その出力は動作しないものとして取り扱われます。

分析対象の要求と他の要求が矛盾しないことを証明しますが、分析対象の要求を満たすトレースが存在することを示すものではありません。このトレースの存在の確認は要求群の完全性(Completeness)チェックの対象です。

 

要求のCCC分析の対象

形式化されたシステム要求群

Vプロセスの左上に位置する、システム要求群を分析の対象とします。モデルやコードは不要です。

 

要求のCCC分析で検出される問題の具体例

要求が不足していて、出力の振る舞いが決まらない

図の例では、Req.02のトリガフェーズにOut1 >=1.0と記載されていますが、どのような条件でOut1が1.0以上の値を取るのかがどこにも定義されていません。これはOut1の振る舞いを示す要求の不足として検出されます。

これらの要求はぱっと見ただけではOut1とOut2の振る舞いをどちらも適切に定義しているように見えますが、上述の通り、実は情報が足りていません。自然言語で書かれた要求を読み解いてこういった欠落を検出することは困難です。この問題を残したままモデリングを開始したとすれば、Req.02に対応した振る舞いは実装されないか、もしくはOut >=1.0となれるような要求に無い振る舞いが暗黙的に追加されるリスクが残ります。

 

分析対象の要求が単独で自己矛盾していて実現しようがない

図の例では、Req.01のトリガフェーズに「tr(In1)が100ms保持されたら」と記載されていますが、tr(In1)はIn1の立ち上がりエッジを取る関数であるため一瞬のイベントであり、100msも保持することは不可能であるため、これは実現不可能な条件として検出されます。

単純な形式化のミスでもこのようなことは起こり得ますが、原因は要求に対する人間の解釈の問題ですので、ここで検出しておかなければ同じ要求に基づいたモデリングでも同様のミスを生じる可能性があります。 

 

要求間の優先順位付けが不足している

図の例は、UpがTrueになったら指定時間以内にPosが増える、DownがTrueになったら指定時間以内にPosが減るという単純な要求です。しかしUpとDownが同時にTrueになったときにはPosは増えても減っていもいずれかの要求に違反してしまいます。これは要求間の部分的な矛盾として検出されます。

このような矛盾は実際に要求を記述している最中にはよく生じます。しかし要求をレビューしたとしても矛盾する状況に気づくのは簡単ではありません。特に要求の数が増えるとなおさらです。この問題を残したままモデリングを開始したとすれば、UpとDownのどちらが優先されるかは特に意識されないまま不適切な選択がされるリスクが残ります。

 

多数の要求を組み合わせると矛盾する

図の例では、3つの要求のうち2つだけを選択した組み合わせではいずれも矛盾は生じません。しかし3つセットになると完全に矛盾します。これは要求間の矛盾として検出されます。

この手の複雑な矛盾はモデリングの最中に気づくことも容易ではありません。もしこの問題を残したままモデリングを完了したとすれば、モデルのテスト時にはいずれかの要求に対する要求違反が見つかります。それを修正するとまた他の要求への違反が見つかります。これを何度も修正を繰り返すうちに要求の組み合わせで矛盾が生じていることに気づくことはできるかも知れませんが、それまでに多くの工数をかけることとなります。

 

中間値と入出力との関係が言及されていない

理想的には要求は入力と出力の関係を端的に表現することが好ましいとされるため、要求内で中間値を多用することは推奨されませんが、実際の要求では中間値に対する言及は多用されています。このとき生じがちな問題が中間値と入出力間の関係の未定義です。図の例では、入力In1に対する中間値Local1の振る舞いは定義されています。しかしLocal1と出力Out1の関係は言及されていません。出力Out1は常に50以下のいずれかの値を取ることが指定されているのみです。このような要求の組み合わせでは、要求シミュレーション時に与えた入力値に対して予想外の出力値が提示されることで、問題に気づくことができます。

この問題を残したままだとしても、この要求に基づいたモデリングをすること自体は可能です。ただし、中間値と出力の関係が明示的でないため、モデリング中に暗黙的に関係性が決定されるか、中間値が出力に影響しないようなモデルとなるリスクが残ります。

 

要求の形式化

要求の形式化はUniversal Patternを用いて行います。Universal Patternは直感的かつ可読性の高いグラフィカルな形式言語です。形式手法の専門知識が無い方でも簡単に読み書きすることができます。形式化という言葉に構える必要はありません。

要求の形式化について、詳しくは要求記述と形式化をご参照ください。

要求の再利用性

要求は要求だけで質をどれだけ高めたとしても、それが開発対象のソフトウェアやシステムに確実に反映されないのでは十分な価値を発揮できません。同じ要求をプロセス全体で一貫して利用することが重要です。CCC分析に利用された要求は、その後のテスト・検証に再利用することができます。例えば、システム要求であればVプロセスの右上に位置するシステムテスト(HILシミュレーションを用いたオフライン・フォーマルテストまたはRTT-Observer)に利用することが可能です。

 

各種機能安全規格準拠 

BTC EmbeddedPlatformによる要求のCCC分析は、各種機能安全規格の最新版に準拠し、 ドイツTÜV Süd社による認証を受けています。

 

 

なぜわざわざ工数をかけてまで要求群に対するCCC分析が必要?

この後の設計フェーズにおけるモデリングは、要求群に基づいて行われます。要求群が適切でなければ、不具合は後段の開発フェーズに伝搬し、そして検出することさえ困難になります。

例えば、要求の正確性(Correctness)チェックで期待した振る舞いが得られていないのであれば、それに基づいて設計されたモデルも期待した振る舞いはしません。しかし要求は満たしているため、テストには合格してしまいます。

要求が完全でなければ(要求に不足があれば)、不足部分の要求に対応するモデルの振る舞いはモデリングをする方次第となります。意図しない振る舞いが実装されたとしても、対応する要求が無いため(少なくともシステマチックなアプローチで)問題を見つけることは困難です。要求に書かれていないことがテストされて、しかもそれで得られた振る舞いがどの要求にも違反していないにも関わらず問題だと特定されることは、一般的な開発プロセスの多くでは偶然に頼るものになりがちです。

要求間が一貫していなければ、ある要求を満たすように設計されたモデルは、他の要求に違反してしまいます。もしくはどの要求にも違反しないためにモデリングの段階で新たな制約が加えられることになるかも知れません。このようにして暗黙的に追加された制約は、要求を考えた方の意図に反するものであったとしても、どの要求にも違反はしないため(少なくともシステマチックなアプローチで検出することは困難です。

このような類の要求の不具合は、要求に基づいたテストでは見つけられるとは限らないため、各開発フェーズで行われるテスト・検証をすり抜け、開発の後段で偶発的に検出されるか、最悪の場合は検出されないこともあり得ます。要求の段階でCCC分析を行うことにより、複雑さの増す後段の開発フェーズでの問題を予防し、開発全体での修正コストを抑制します。