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

54
C 0508-7 : 2017 (IEC 61508-7 : 2010)
      ことが最善のアプローチである。各バブルは,明瞭な変換を表す必要がある。すなわち,出力は,
      何らかの形で,入力とは異なっていることが望ましい。図式の全般的構造を決めるための規則は全
      くなく,データフロー図を作成することは,システム設計の創造的な面の一つである。全ての設計
      と同様に,これは,最終的な図式を作成するまでに初期の試みを何段階にもわたって詳細化する反
      復手順である。

参考文献

: 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
JIS X 0121:1986 情報処理用流れ図・プログラム網図・システム資源図記号
注記 対応国際規格 : ISO 5807:1985,Information processing−Documentation symbols and conventions
for data, program and system flowcharts, program network charts and system resources charts
ISO/IEC 8631:1989,Information technology−Program constructs and conventions for their representation
C.2.3 構成図
注記 この技術及び手法は,JIS C 0508-3の表B.5で引用されている。
目的 : プログラムの構成を図の形で示す。
説明 : 構成図は,データフロー図を補足する表記法である。構成図はプログラミングシステム及び部品の
階層を記述し,これを木構造として図に表す。構成図は,データフロー図の要素を,プログラム単
位の階層としてどのように実装できるかを文書化する。
構造化チャートは,プログラムモジュール間の関係を,これらのユニットを起動する順序につい
ての情報は一切含まずに示す。構造化チャートは,次の四つの記号を用いて描く。
− モジュールの名前を付けた長方形
− 構造化を形成する,これらの長方形を接続する線
− 構造化チャート内の要素とやりとりできるデータの名前を付けた,丸付き矢印(白丸)(通常,
丸付き矢印は,チャート中の長方形を結ぶ線に平行に描く。)
− 構造化チャート内の一つのモジュールから他のモジュールへ送られる制御信号の名前を付け
た,丸付き矢印(黒丸)。丸付き矢印は,同様に二つのモジュールを結ぶ線に平行に描く。
自明ではないデータフロー図から,多数の異なる構造化チャートが導き出されることもある。
データフロー図は,システムにおける情報と機能との間の関係を表す。構造化チャートは,シス
テムの要素をどのように実装するか,その方法を表す。これらの技術は表現方法が異なるが,両方
ともシステムの全体像を表現している。

参考文献

: Software Design & Development. G. Lancaster. Pascal Press, 2001, ISBN 1741251753, 9781741251753
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

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

                                                                                             55
                                                                C 0508-7 : 2017 (IEC 61508-7 : 2010)
C.2.4 形式手法
    注記 この技術及び手法は,JIS C 0508-3の表A.1,表A.2,表A.4及び表B.5で引用されている。
C.2.4.1 一般
目的 : 数学に基づく方法によるソフトウェアの開発。これには,形式的設計及び形式的なコーディング技
      術が含まれる。
説明 : 形式手法は,システムの仕様作成,設計又は実装における一部の段階において,システムを記述し
      ようとする手法である。結果としての記述は,様々なクラスの矛盾又は不正確さを検出するために
      数学的解析を受けることができるように,厳密な表記法で表す。さらに,この記述は,場合によっ
      ては,コンパイラによるソースプログラムの文法検査に似た厳密さで,機械によって解析したり,
      記述対象のシステムの挙動の種々の面を表示するためにアニメーション化したりすることもでき
      る。アニメーションを用いる場合,システムの規定された動作に対する認識が高まるため,形式的
      に規定された要求事項に加えて,実際の要求事項に適合しているかどうかの確認ができる。
        形式手法は,一般に,表記法(一般に,用いられている離散数学のある形式),その表記法による
      記述を導き出す技術,及びその記述を種々の正確さを表す要素についてチェックするための各種解
      析形式を提供する。
        幾つかの形式手法,すなわち,CCS,CSP,HOL,LOTOS,OBJ,時相論理,VDM及びZについ
      て,概要をC.2.4.2C.2.4.9で説明する。他の技術,例えば,有限状態機械及びペトリネット(附属
      書B参照)は,これらの技術が使用時にどのくらい厳密に数学的根拠に準拠しているかによって,
      形式手法とみなすこともできる。

参考文献

: Formal Specification: Techniques and Applications. N.Nissanke, Springer-Verlag Telos, 1999, ISBN
1852330023
The Practice of Formal Methods in Safety-Critical Systems. S. Liu, V. Stavridou, B. Dutertre, J. Systems
Software 28, 77-87, Elsevier, 1995
Formal Methods: Use and Relevance for the Development of Safety-Critical Systems. L. M. Barroca, J. A.
McDermid, The Computer Journal 35 (6), 579-599, 1992
How to Produce Correct Software−An Introduction to Formal Specification and Program Development by
Transformations. E. A. Boiten et al, The Computer Journal 35 (6), 547-554, 1992
C.2.4.2 通信システムの計算法(CCS)
目的 : CCSは,同時通信プロセスのシステムの挙動を説明し,その理由付けをする手法である。
説明 : CCSは,システムの挙動に関する数学的計算法である。システム設計を,順次に又は並行して動作
する独立プロセスのネットワークとしてモデル化する。プロセスは,ポート(CSPのチャネルに似
たもの)を経て通信することができ,通信は両方のプロセスの準備ができているときだけ行う。非
決定論をモデル化することができる。システム全体の高水準抽象説明(トレースとして知られてい
る。)から始め,その通信プロセスの全挙動が全システムに要求する全挙動となる通信プロセスの
構成へと,システムの段階的詳細化を実施することが可能である。同様に,ボトムアップ方式で作
業すること,プロセスを組み合わせること,及び結果としてのシステムの特性を構成規則に関連す
る推論規則を用いて推定することが可能である。

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

56
C 0508-7 : 2017 (IEC 61508-7 : 2010)

参考文献

: Communication and Concurrency. R. Milner. Pearson Education, 1989, ISBN 9780131150072
C.2.4.3 通信順次プロセス(CSP)
目的 : CSPは,同時ソフトウェアシステム,すなわち,同時に動作する通信プロセスのシステムの仕様作
成のための技術である。
説明 : CSPは,プロセスのシステムの仕様用の言語を提供し,プロセスの実装がシステムの仕様を満たし
ていることを検証するための証拠(トレース,すなわち事象の許容シーケンスとして記述される。)
を提供する。
システムを,順次に又は並行して構成する独立プロセスのネットワークとしてモデル化する。各
プロセスでは,プロセスで起こる可能性のある挙動の全てを明確に説明できる。プロセスは,チャ
ネルを経て通信する(同期する,又はデータを交換する。)ことができ,通信は両方のプロセスの準
備ができているときだけ行う。事象の相対タイミングはモデル化することができる。
CSPの背景にある理論は,INMOSトランスピュータのアーキテクチャに直接組み込まれており,
OCCAM言語を用いることによって,CSP規定システムをトランスピュータのネットワーク上にお
いて直接実装することが許される。

参考文献

: Communicating Sequential Processes: The First 25 Years. A. Abdallah, C. Jones, J. Sanders (Eds.). Springer,
2004, ISBN 3540258132, 9783540258131
C.2.4.4 上位論理 (HOL)
目的 : これは,ハードウェア仕様作成及び適合確認の基礎として意図している形式言語である。
説明 : HOLとは,具体的な論理表記法及びこの表記法の機械支援システムのことであり,これらは両方
とも,ケンブリッジ大学のコンピュータ研究所で開発されたものである。この論理表記法は,ほと
んどチャーチの単純型理論から採用されており,機械支援システムは,コンピュータ処理可能な機
能の論理(LCF)システムに基づいている。

参考文献

: Higher-Order Computational Logic. J. Lloyd. In Computational Logic: Logic Programming and Beyond,
Lecture Notes in Computer Science, Springer Berlin / Heidelberg, 2002, ISBN 978-3-540-43959-2
C.2.4.5 時間的順序仕様記述用言語(LOTOS)
目的 : LOTOSは,同時通信プロセスのシステムの挙動を説明し,その理由付けをする手法である。
説明 : LOTOSは,CCSに基づくものであり,関連代数学CSP及びCIRCAL(回路計算法)からの追加の
特徴をもつ。これは,データ構造及び値表現の取扱いにおけるCCSの弱点を,CCSと抽象データ
型言語ACT ONEの特質とを組み合わせることによって克服している。LOTOSのプロセス記述の特
質は,抽象データ型の記述のために他の形式手法とともに用いることができる。

参考文献

: Model Checking for Software Architectures. R. Mateescu. In Software Architecture, Lecture Notes in Computer
Science, Springer Berlin / Heidelberg, 2004, ISBN 978-3-540-22000-8
ISO 8807:1989,Information processing systems−Open Systems Interconnection−LOTOS−A formal

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

                                                                                             57
                                                                C 0508-7 : 2017 (IEC 61508-7 : 2010)
        description technique based on the temporal ordering of observational behaviour
C.2.4.6 OBJ
目的 : 実装に先立って,正確なシステム仕様に実装使用者フィードバック及びシステム妥当性確認を提供
      する。
説明 : OBJは,代数的仕様記述言語である。使用者は,要求事項を代数方程式の形で規定する。システム
      の挙動面又は構造面は,抽象データ型(ADT)への作用の形で規定されている。ADTは,作用の挙
      動は目に見えるが,実装の詳細は“隠されている”ADAパッケージに似ている。
        OBJ仕様作成及びその後の段階的実装は,他の形式アプローチと同じ形式的証明技術に従う。さ
      らに,OBJ仕様の作成における特徴はこれが実行可能であることから,仕様自体からシステムの妥
      当性確認を直接的に達成できる。実行とは,本質的には特定の出力値を得るまで継続する等式への
      代入(書換え)によって機能を評価することである。この実行可能性によって,計画中のシステム
      のエンドユーザは,根拠となっている形式仕様作成技術に精通する必要なしに,システムの仕様作
      成段階において,将来できあがるシステムの“概観”を得ることができる。
        他の全てのADT技術の場合と同様に,OBJは,順次システムに,又は同時システムの順次面だ
      けに適用できる。OBJは,小規模及び大規模工業用の両方の仕様作成に用いられてきている。

参考文献

: Software Engineering with OBJ: Algebraic Specification in Action. J. Goguen, G. Malcolm. Springer, 2000,
ISBN 0792377575, 9780792377573
C.2.4.7 時相論理
目的 : 安全性及び運転時の要求事項の直接的表現,並びにこれらの特性が後に続く開発段階においても維
持されることの形式実証。
説明 : 標準第一階の述語論理は,時間の概念を含まない。時相論理は,モーダル演算子(例えば,“今後
は”及び“最終的に”)を追加することによって,一階論理を拡張する。これらの演算子は,シス
テムについてのアサーションを修飾するために用いることができる。例えば,安全特性は,“今後
は”を保持することが必要になるかもしれないが,他の望まれるシステム状態では,他のある開始
状態から“最終的に”達成することが必要になるかもしれない。時間的論理式は,状態(挙動)の
シーケンスとして解釈される。何が“状態”を構成するかは,選択された記述水準によって異なる
が,システム全体,システムの一つの要素又はコンピュータプログラムのことを指すことがある。
定量化されている時間間隔及び制約条件は,時相論理では積極的に取り扱わない。絶対タイミン
グは,状態記述の一部として,追加の時間状態を作成することによって処理する必要がある。

参考文献

: Mathematical Logic for Computer Science. M. Ben-Ari. Springer, 2001, ISBN 1852333197, 9781852333195
C.2.4.8 VDM,VDM++ −ウィーン開発方法
目的 : 順次(VDM)及び同時リアルタイム(VDM++)プログラムの系統的な仕様作成及び実装。
説明 : VDMは数学に基づく仕様作成技術であり,仕様の正確さを証明することができる方法によって実
装を詳細化するための技術である。
仕様作成技術は,モデルに基づくものである。すなわち,システム状態は,不変量(述部)を記

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

58
C 0508-7 : 2017 (IEC 61508-7 : 2010)
      述する基礎となる集合論的構造の形でモデル化し,その状態に基づく動作は,動作の事前条件及び
      事後条件をシステム状態の形で規定することによってモデル化する。システム不変量が維持されて
      いることは,動作によって証明することができる。
        仕様の実装は,システム状態を目標言語によるデータ構造の形で具体化すること,及び動作を目
      標言語によるプログラムの形で詳細化することによって行う。具体化及び詳細化段階では,正確さ
      を確立する証明義務が生じる。これらの義務を実行するかどうかは,設計者が決める。
        VDMは,主として仕様作成段階において用いられているが,ソースコードに至る設計及び実装
      段階において用いることもできる。これは,順次に構造化したプログラム,又は同時システムの順
      次プロセスだけに適用できる。
        VDMのオブジェクト指向同時リアルタイム拡張版であるVDM++は,ISO言語VDM-SL及びオ
      ブジェクト指向言語であるスモールトークに基づく形式仕様記述言語である。
        VDM++は,使用者が同時リアルタイムシステムをオブジェクト指向方式で形式規定することがで
      きるように,広範囲の構造を提供する。VDM++において,完全な形式仕様を,クラス仕様の集合,
      及び状況に応じて,作業空間で構成する。
        VDM++のリアルタイム条件を,次に示す。
      − メソッド本体に,現時点及びメソッド呼出時点の両方を表すため一時的表現式を与える。
      − 適切な実装のための運用時間の上限(又は下限)を規定するためにメソッドに,時限後置表現
          を加えてもよい。
      − 時間連続変数を導入する。仮定及び影響の節を設けることによって,これらの時間の関数間の
          関係(例えば,微分方程式)を指定してもよい。この特徴は,時間連続環境において動作する
          システムの要求事項の規定に非常に有用であることが分かっている。詳細化手順は,これらの
          種類のシステムについて,離散的ソフトウェアソリューションに至る。

参考文献

: ISO/IEC 13817-1:1996,Information technology−Programming languages, their environments and system
software interfaces−Vienna Development Method−Specification Language−Part 1: Base language
Systematic Software Development using VDM. C. B. Jones. Prentice-Hall. 2nd Edition, 1990
Conformity Clause for VDM-SL, G. I. Parkin and B. A. Wichmann, Lecture Notes in Computer Science 670,
FME'93 Industrial-Strength Formal Methods, First International Symposium of Formal Methods in Europe.
Editors: J. C. P. Woodcock and P. G. Larsen. Springer Verlag, 501-520
C.2.4.9 Z
目的 : Zは,順次システムのための仕様記述言語表記法であり,開発者が,仕様に対して,Z仕様から実
行可能なアルゴリズムまでの正確さを証明可能な方法で進めることができる設計技術である。
Zは,主として仕様作成段階において用いられるが,仕様作成から設計及び実装に進めるための
方法が考案されている。Zは,データ指向順次システムの開発に最適である。
説明 : 仕様作成技術は,VDMと同様,モデルに基づくものである。すなわち,システム状態を,不変量
(述部)を記述する基となる集合論的構造の形でモデル化し,その状態に基づく動作は,動作の事
前条件及び事後条件をシステム状態の形で規定することによってモデル化する。システム不変量が
維持されていることは動作によって証明することができ,これによって,システム不変量の一貫性
を実証することができる。仕様の形式部分は,詳細化によって仕様を構造化することを可能とする

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

次のページ PDF 61