JIS C 0508-7:2017 電気・電子・プログラマブル電子安全関連系の機能安全―第７部：技術及び手法の概観 | ページ 19

                                                                                             89
                                                                C 0508-7 : 2017 (IEC 61508-7 : 2010)
      − 仕様から導き出す同値クラス。仕様の解釈は,例えば,選択した値を同一方法で処理する入力
          指向か,又は例えば,一連の値が同じ機能結果に至る出力指向のどちらかである。
      − プログラムの内部構造から導き出す同値クラス。同値クラス結果は,プログラムの静的解析か
          ら,例えば,同じ経路で実行する一連の値として決定する。

参考文献

: The Art of Software Testing, second edition. G. J. Myers, T. Badgett, T. M. Codd, C. Sandler, John Wiley and
Sons, 2004, ISBN 0471469122, 9780471469124
Software engineering: Update. Ian Sommerville, Addison-Wesley Longman, Amsterdam; 8th ed., 2006, ISBN
0321313798, 9780321313799
Software Engineering. Ian Sommerville, Pearson Studium, 8. Auflage, 2007, ISBN 3827372577,
9783827372574
Static Analysis and Software Assurance. D. Wagner, Lecture Notes in Computer Science, Volume 2126/2001,
Springer, 2001, ISBN 978-3-540-42314-0
C.5.8 構造テスト
注記1 この技術及び手法は,JIS C 0508-3の表B.2で引用されている。
目的 : プログラム構造の幾つかのサブセットを実行するテストを適用する。
説明 : プログラムの解析に基づき,大きな割合(大抵,あらかじめ目的として定められている。)を占め
るプログラムコードを実行するために,一連の入力データを選ぶ。コードカバレッジ(E.13参照)
は,要求する厳密さの水準によって次のように異なる。全てのケースにおいて,選択するカバレッ
ジメトリックを100 %目標とすることが望ましい。100 %の範囲を達成できない場合は,100 %を達
成できない理由をテスト報告書に文書化する(例えば,ハードウェアの問題が発生したときだけに
入力する防御的コード)。次に示す最初の4技術は,JIS C 0508-3の表B.2の推奨事項として特に記
述しており,テストツールによって広く支援されている。残りの技術も考慮に入れてもよい。
− エントリー点(コールグラフ)カバレッジ 全てのサブプログラム(サブルーチン又は機能)
を1回以上(これは,最小限に厳格な構造的カバレッジ値である。)コールしていることを確実
にする。
注記2 オブジェクト指向言語には,動的ディスパッチングによって呼び出すことができる,
多様型の各種変異型(上書きされるサブプログラム)に適用する同一名のサブプロ
グラムが幾つかある。これらの場合,上書きされる全てのサブプログラムを個々に
テストすることが望ましい。
− ステートメント コード内の全てのステートメントを,1回以上実行したことを確実にする。
− 分岐 全ての分岐の両端をチェックすることが望ましい。ただし,幾つかの種類の防衛的コー
ドに対しては実行が難しい場合がある。
− 複合条件 複合条件付き分岐(すなわち,AND/ORによってリンクしている分岐)における,
全ての条件を実行する。MC/DC(modified condition/decision coverage,参考文献DO-178B)を参
照。
− LCSAJ 線形コードシーケンス及びジャンプは,ジャンプによって終了する,条件付きステー
トメントを含むコードステートメントの線形シーケンスである。多くの潜在的サブパスは,そ
の前のコードの実行によって課せられる入力データに対する制約のために,実行不可能となる。

――――― [JIS C 0508-7 pdf 91] ―――――

90
C 0508-7 : 2017 (IEC 61508-7 : 2010)
      − データフロー 実行経路,例えば,同一変数を書き込み,かつ,読み込むパスを,データ使用
          に基づいて選択する。
      − 基礎パス 全ての経路が含まれる,開始から終了までの有限パスの最小セットの一つ(この基
          礎セットの中でパスの重なり合う組合せによって,プログラム部分を通るパスを形成すること
          ができる。)。全ての基礎パスのテストは,エラー位置を突き止めるために有効であることが示
          されている。

参考文献

: The Art of Software Testing, second edition. G. J. Myers, T. Badgett, T. M. Codd, C. Sandler, John Wiley and
Sons, 2004, ISBN 0471469122, 9780471469124
Software engineering: Update. Ian Sommerville, Addison-Wesley Longman, Amsterdam; 8th ed., 2006, ISBN
0321313798, 9780321313799
Software Engineering. Ian Sommerville, Pearson Studium, 8. Auflage, 2007, ISBN 3827372577,
9783827372574
RTCA, Inc. document DO-178B and EUROCAE document ED-12B, Software Considerations in Airborne
Systems and Equipment Certification, dated December 1, 1992
C.5.9 制御フロー解析
注記 この技術及び手法は,JIS C 0508-3の表B.8で引用されている。
目的 : 不完全プログラム構造及び潜在的不良プログラム構造を検出する。
説明 : 制御フロー解析は,コードにおいて適正プログラミング規範に従わない,疑わしい部分を見つける
ための静的テスト技術である。プログラムを解析して有向グラフを作成し,このグラフは次の事項
について更に解析することができる。
− アクセス不可能なコード,例えば,コードのブロックを到達不可能にしておく無条件ジャンプ
− 結節付きコード。正しく構造化されたコードは,単一ノードに縮小する継続的なグラフによっ
て,単純化することが可能な制御グラフをもつ。逆に,不完全に構造化されたコードは,幾つ
かのノードが構成する一つの結節に縮小することができるだけである。

参考文献

: Software engineering: Update. Ian Sommerville, Addison-Wesley Longman, Amsterdam; 8th ed., 2006, ISBN
0321313798, 9780321313799
Software Engineering. Ian Sommerville, Pearson Studium, 8. Auflage, 2007, ISBN 3827372577,
9783827372574
C.5.10 データフロー解析
注記 この技術及び手法は,JIS C 0508-3の表B.8で引用されている。
目的 : 不完全プログラム構造及び潜在的不良プログラム構造を検出する。
説明 : データフロー解析は,制御フロー解析から得られる情報を,変数をコードの種々の部分において読
み出す,又は書き込むことに関する情報と組み合わせる静的テスト技術である。この解析では,次
の事項についてチェックすることができる。
− 値が割り当てられる前に,読み出される可能性がある変数。これは,新しい変数を宣言すると
きに常に値を割り当てることによって避けることができる。

――――― [JIS C 0508-7 pdf 92] ―――――

                                                                                             91
                                                                C 0508-7 : 2017 (IEC 61508-7 : 2010)
      − 複数回の書き込みにおいて,読み出しを伴わない書き込みが1回以上ある変数。これは,コー
          ドが抜けていることを示す場合がある。
      − 書き込みが行われるが,一度も読み出されない変数。これは,余分なコードを示す場合がある。
        データフロー異常は,必ずしもプログラムフォールトに直接的に結び付くとは限らないが,この
      異常を回避した場合,そのコードがフォールトを含む可能性は小さくなる。

参考文献

: Software engineering: Update. Ian Sommerville, Addison-Wesley Longman, Amsterdam; 8th ed., 2006, ISBN
0321313798, 9780321313799
Software Engineering. Ian Sommerville, Pearson Studium, 8. Auflage, 2007, ISBN 3827372577,
9783827372574
C.5.11 記号的実行
注記 この技術及び手法は,JIS C 0508-3の表B.8で引用されている。
目的 : ソースコードと仕様との間の一致を示す。
説明 : プログラム変数を,全ての代入について左辺を右辺で置き換えた後に評価する。条件付き分岐及び
ループを,ブール式に変換する。最終結果は,各プログラム変数の記号表現である。この表現は,
プログラムが実データを与えられた場合に計算をする値の公式である。これを,期待する表現と対
照することができる。
記号的実行の関連用法としては,プログラムロジックによって,パスに対してテストデータを系
統的に発生させる方法がある。記号的実行の機能は,ソフトウェア要素テスト及びコード解析のた
めの機能を提供する統合ツールセットに組み込んでもよい。

参考文献

: Using symbolic execution for verifying safety-critical systems. A. Coen-Porisini, G. Denaro, C. Ghezzi, M.
Pezz. Proceedings of the 8th European software engineering conference, and 9th ACM SIGSOFT
international symposium on Foundations of software engineering. ACM, 2001, ISBN:1-58113-390-1
Using symbolic execution to guide test generation. G. Lee, J. Morris, K. Parker, G. Bundell, P. Lam. In Software
Testing, Verification and Reliability, vol 15, no 1, 2005. John Wiley & Sons, Ltd
C.5.12 形式的証明(形式的適合確認)
注記 この技術及び手法は,JIS C 0508-3の表A.5及び表A.9で引用されている。
目的 : 理論的かつ数学的なモデル及び規則を用いて,プログラムを抽象モデル化して,プログラムの正確
さを証明する。
説明 : テストは,プログラムの正確さを調べるために通常使われる方法であるが,実際の値によるプログ
ラムの複雑さを考える場合,徹底的なテストは実現できないのが普通である。したがって,考えら
れるプログラム挙動の一部だけをテストによって調べることができるにすぎない。これに対して,
形式的適合確認は,考えられる全ての入力に対してプログラムが定義どおりに挙動することを確定
するために,数学的に表現したプログラムに数学的手法を適用する。
システムの形式的適合確認では,プログラム及び要求する挙動を,厳密な数学的意味をもつ言語
で抽象モデル化(すなわち,仕様化)する必要がある。仕様は完全なものでも,次のような特定の
プログラム特性に限定したものでもよい。

――――― [JIS C 0508-7 pdf 93] ―――――

92
C 0508-7 : 2017 (IEC 61508-7 : 2010)
      − 機能的な正確さに関する特性。すなわち,プログラムは個別の機能性を提示することが望まし
          い。
      − 安全特性(すなわち,ある不良挙動が決して発生しないことを示す。)及び活性特性(すなわち,
          ある優れた挙動が必ず発生することを示す。)。
      − タイミング特性。すなわち,ある挙動が特定の時間に発生することを示す。
        形式的適合確認の結果,考えられる全ての入力に対する仕様に関してプログラムの抽象モデルが
      正しい,すなわち,モデルが規定の特性を満たしているという厳密な論拠を得ることができる。
        ただし,モデルの正確さがそのまま実際のプログラムの正確さを証明するものではなく,対象の
      特性について,このモデルが実際のプログラムを正確に抽象しているかを明らかにするために,更
      にステップが必要になる。実践的な対象のプログラム特性は,数学的(例えば,タイミング及びス
      ケジューリング,明瞭で簡単なユーザインタフェース,又は形式言語で容易に表現できない全ての
      特性若しくは設計オブジェクティブ)に形式化することができない。したがって,形式的適合確認
      は,シミュレーション及びテストに完全に取って代わるのではなく,むしろ,全ての入力に対する
      プログラムの正しい動作を支援する更なる証拠を提供することで,これらの技術を補足するもので
      ある。形式的適合確認はプログラムの抽象モデルの正確さを確実にするが,テストは実際のプログ
      ラムが期待どおりに挙動することを確実にする。
        設計フェーズで形式的適合確認を採用することによって,設計フェーズの早い段階で重大なエラ
      ー及びミスを発見することが可能になるため,開発時間を大幅に低減でき,これによって,設計と
      テストとの間を往復する時間を減らすことができる。
        実用化されている形式方法の幾つか,例えば,CCS,CSP,HOL,LOTOS,OBJ,時相論理,VDM
      及びZをC.2.4に示す。
C.5.12.1 モデルチェック
  モデルチェックは,リアクティブシステム及び並行システムの形式的適合確認を行う方法の一つである。
システムの挙動を記述する有限状態構造の場合,時相論理の公式として書き込んだ特性を,構造に対して
有効であるかどうかチェックする。効率的アルゴリズム(例えば,SPIN,SMV及びUPPAAL)を用いて,
構造の状態全体を自動的かつ包括的に詳細検討する。特性が有効でない場合は,反例を生成する。この反
例は,特性がいかにして構造内で邪魔されているかを示し,システムを調査する非常に有用な情報を含ん
でいる。モデルチェックは,従来の検査及びテストでは見逃したかもしれない“困難なバグ”を検出でき
る。
  モデルチェックは,捉えにくい複雑さを解析するのに役立つ。これは,一部の低SILアプリケーション
で役に立つが,高SILアプリケーションに捉えにくい複雑さがある場合,注意が必要である。

参考文献

: Is Proof More Cost-Effective Than Testing・ S. King, R. Chapman, J. Hammond, A. Pryor. IEEE Transactions
on Software Engineering, vol. 26 no. 8, August 2000
Model Checking. E. M. Clarke, O. Grumberg, and D. A. Peled. MIT Press, 1999, ISBN 0262032708,
9780262032704
Systems and Software Verification: Model-Checking Techniques and Tools. B. Berard, M. Bidoit, A. Finkel, F.
Laroussinie, A. Petit, L. Petrucci, Ph. Schnoebelen, and P. Mckenzie, Springer, 2001, ISBN 3-540-41523-8
Logic in Computer Science: Modelling and Reasoning about Systems. M.Huth and M. Ryan. Cambridge

――――― [JIS C 0508-7 pdf 94] ―――――

                                                                                             93
                                                                C 0508-7 : 2017 (IEC 61508-7 : 2010)
        University Press, 2000, ISBN 0521652006, 0521656028
    The Spin Model Checker: Primer and Reference Manual. G. J. Holzmann. Addison-Wesley, 2003, ISBN
        0321228626, 9780321228628
C.5.12.2 (規定なし)
C.5.13 複雑さ測定
    注記 この技術及び手法は,JIS C 0508-3の表B.9及び表C.19(詳細特性−モジュラーアプローチ)
          で引用されている。
目的 : ソフトウェア自体の特性から,又はソフトウェアの開発若しくはテスト履歴から,プログラムの属
      性を予測する。
説明 : これらのモデルは,ソフトウェアの構造特性を評価し,そのソフトウェアを,信頼性又は複雑さな
      ど,望まれる属性に関係付ける。大半の手法は,評価するためにソフトウェアツールを必要とする。
      適用可能な測定方法を,次に示す。
      − グラフ理論的複雑さ。この手法は,トレードオフを評価するためにライフサイクルの初期にお
          いて適用でき,その循環数が表すプログラム制御グラフの複雑さに基づいている。
      − あるソフトウェアモジュールを作動させる多くの方法(アクセスしやすさ)。ソフトウェアモジ
          ュールへのアクセスが多くなるほど,デバッグしやすくなる。
      − ハルステッドのメトリックス。この手法では,演算子及びオペランドの数を数えることによっ
          てプログラムの長さを計算する。これによって,将来の開発リソースを予測する場合の,比較
          のためのベースラインを形成する複雑さ及びサイズの指標を得る。
      − ソフトウェアモジュール当たりの開始及び終了の数。開始点及び終了点の数を最小限に抑える
          ことが,構造化設計及びプログラミング技術の重要な特徴である。

参考文献

: Metrics and Models in Software Quality Engineering. S.H. Kan. Addison-Wesley, 2003, ISBN 0201729156,
9780201729153
C.5.14 形式的検査
注記 この技術及び手法は,JIS C 0508-3の表B.8で引用されている。
目的 : ソフトウェア要素の欠陥を明らかにする。
説明 : 形式的検査は,欠陥を発見するため及び作成者がソフトウェア生成物を改善できるようにするた
め,作成者と対等な技術者が実施する,ソフトウェア生成物を検査するための構造化したプロセス
である。作成者は,習熟段階で検査員にプログラム内容の概要説明をする以外は,検査プロセスに
加わらないことが望ましい。形式的検査は,ソフトウェア開発ライフサイクルのいずれかの段階で
作成する特定のソフトウェア要素について実施してもよい。
検査を行う前に,検査員は,検査対象の生成物を十分に知る必要がある。検査プロセスでの検査
員の役割を,明確に定義しておくことが望ましい。検査項目は用意しておくことが望ましい。ソフ
トウェア要素に要求する特性に基づき,開始基準及び終了基準を定義する。開始基準とは,検査を
実施する前に満たさなければならない基準又は要求事項である。終了基準は,特定のプロセスを完
了するために満たさなければならない基準又は要求事項である。

――――― [JIS C 0508-7 pdf 95] ―――――

次のページ PDF 96