SCODEメソッド

SCODE-ANALYZERに実装されたSCODEメソッドにより、このツールで行われる形式的検証で発生するエラーが通知されるので、開発者はそれらを直ちに訂正することができます。そのため、システム開発者は常に形式的検証が完了した状態のシステムを扱うことができ、ソフトウェアエンジニアはその成果物を利用して既存のソフトウェアの最適化や新規のソフトウェアの設計を行い、テスタビリティを高めることができます。

成果物は全て、プログラムコードの自動生成といった後続の工程に用いる事が出来ます。

SCODEメソッド

電気機械式ブレーキの問題空間(例)

SCODEメソッドは、システムの表示と分析を容易に行うことのできる、3つのステップからなる反復プロセスです。このプロセスでは、1つの問題をそれぞれ独立的に解決できる小問題に分け、それらの小問題の解を使用して元の問題の解決を図ります。SCODE-ANALYZERはこのプロセスの案内役となってユーザーを積極的にサポートします。

ステップ1 – プロブレムスペースを定義する

第1ステップでは、 システムまたはシステムに変化をもたらす可能性のある環境(たとえば、ユーザーの介入や、センサから得られる測定結果など)のあらゆる側面を考慮に入れて、プロブレムスペースを定義します。生じる変化(変数や信号の変更など)は、すべて出力と見なされます。

“compressing brake calipers”(ブレーキキャリパ加圧)モード の定義(例)

ステップ2 – モードを定義する

第2ステップでは、有効なシステムモードと無効なシステムモードを記述します。ファンクション開発者は、ディメンションごとに選択されたオプションを組み合わせることによってモードを定義していきます。

いくつかの異なる入力が、全く同じ変化をシステムにもたらす場合

異なる入力ディメンションの組み合わせから、同じ出力ディメンションを持つ組み合わせが作り出される可能性があります。つまり、いくつかの異なる入力が、全く同じ変化をシステムにもたらす場合があります。

SCODE-ANALYZERでは、すべての組み合わせが考慮されていることを確認して、いかなる例外も見過ごしがないようにサポートします。これにより、たとえば、開発当初は一部の要件しか定義されていなかったとしても、その後に予期せぬ出来事でコストが発生するといった事態を防ぐことができます。このソフトウェアはさらに、各プロブレムスペースの組み合わせがそれぞれ1つのモードにしか割り当てられていないこと、およびモードの定義同士が全くオーバーラップしていないことを確認します。

ステップ3 – モード遷移を定義する

モード遷移表とモード遷移図

第3ステップでは、機能開発者は、モード間遷移時にシステムがどのように反応しなければならないかを定義します。テーブル形式のインターフェースまたはグラフィカルユーザーインターフェースを用いて、あるモードから別のモードへの遷移をどのイベントでトリガするかを決定します。また、所定のモード間の遷移を不正と定めることも可能です。開発者は定義されたイベントについてもモードと同様に、完全性、デッドロックの可能性、およびその他の特性を調べます。