![パターンの定義
? ループの導入
α
α
α
μα.T -> T[μα.T / α]](https://image.slidesharecdn.com/sigpro-131111021111-phpapp02/85/Sigpro-20-320.jpg)
Sigpro
- 1. アシュアランスケース言語の 設計と実装（へ向けて） 電気通信大学 JST CREST DEOS 倉光チーム 松野裕 www.dcase.jp 情報処理学会プログラミング言語研究会（SIGPRO） １１月１１日 IBM東京基礎研究所（豊洲）で発表
- 2. 内容 ? アシュアランスケースについて – GSN (Goal Structuring Notation)表記法 ? ? ? ? ? GSNパターン アシュアランスケース言語の設計 プロトタイプ実装 関連研究 まとめ
- 3. アシュアランスケース Assurance Case ? システムが与えられた適用先と環境で、 十分にディペンダブル（安全）であるこ とを提供する構造化された証拠ドキュメ エビデンス ント（他にも定義あり） ゴール 例: FTA(Fault Tree Analysis) の結果 など エビデンス 例: システムは安全である エビデンス 議論の構造 2013/07/31 3
- 4. アシュアランスケースの背景 ? 1988年の北海油田事故(167名死亡)などを契機に、欧米 で規格認証の際に提出が義務付けられるまでに普及 – 手順のみでなく、なぜ安全性が保たれるのか、明示された議論 で、エビデンスをもとに保証する – 北海油田事故の事故報告書により「Safety Case」という言葉 が普及したs ? Prescriptive(宣言的) と Goal Based（ゴール指向） – Prescriptive:認証者から与えられたチェックリストをチェックす る – Goal Based: 要求される安全ゴールを満たしていることの議論 を構築する – ISO26262 (自動車の機能安全規格), EUROCONTROL (Eurocontrol, 2006), the Rail Yellow Book (Rail Track, 2000), and MoD Defense Standard 00-56 (MoD, 2007) などがGoal Basedな認証を要求してい 2013/07/31 4 ? 2013 D-Case委員会 る
- 5. Safety Caseの利用状況 ? イギリス “Using safety cases in industry and health care”, UK Health Foundation, 2012.12 – 高安全分野、医療分野におけるSafety Caseの利用状況 を分析 ? 商用飛行機、自動車、防衛、原子力、石油化学、鉄道、医療 器具、健康管理 – http://www.health.org.uk/publications/using-safetycases-in-industry-and-healthcare ? アメリカ 食品医薬品局によって、輸血ポンプな どを認証のためにSafety Caseの提出が義務づけら れている ? 日本 自動車会社はISO26262(自動車の機能安全規 格)で義務づけられたため、調査を行っている – JST DEOSプロジェクト
- 6. アシュアランスケースの呼び方 ? 日本語だと保証ケース – Caseは法廷用語で、証拠書類などの意味 ? 安全性を議論する場合は Safety Case, ディペンダビリティを議論す る場合はDependability Caseと呼ばれる Assurance Case 2013/07/31 Safety Case Dependability Case Security Case … ? 2013 D-Case委員会 6
- 7. アシュアランスケースの表記法 ? 多くは自然言語で記述される – 99% word文書？ ? グラフィカルな表記法が提案されている CAE (Claim, Argument. Evidence) GSN (Goal Structuring Notation) CAEとGSN 基本的には同じ 表記法 両者を統合した OMG SACM (structured assurance case metamodel) 規格が策定されている
- 9. 骋厂狈の例
- 10. アシュアランスケースの評価 ? 肯定 Goal-Basedな規格認証では、システムの安全性を満たすための手法は システム開発者、運用者側に委ねられており、自由に安全技術を導入でき るなど、ベストエフォートでシステムの安全性達成ができるなど利点があ る （Robin Bloomfield, Peter Bishop, City Univ. London） – システム開発者や運用者は定められた項目を充足するのみで、法的責任を満たすこと ができる。定められた項目が安全性に不十分であったと後に判明しても、責任は規制 側のみにある。 – Prescriptiveに定められた項目は、過去の経験に基づくものであり、技術的発展に伴い、 不十分になる、さらには不必要なリスクを伴う可能性がある。 – Prescriptiveに定められた項目は、新しい安全技術の導入を阻む。 – Prescriptiveに定められた項目は、国際市場への展開、他分野との統合を阻む。 – Prescriptiveに定められた項目を満たすために、不必要なコストがかかることがある。 ? 否定 多くのSafety Caseの研究は、個人的な意見を述べているか、記述例を 示しているのみで、本当に効果的であるかどうかは示していない （Nancy Leveson, MIT） 2013/07/31 ? 2013 D-Case委員会 10
- 11. 内容 ? アシュアランスケースについて – GSN (Goal Structuring Notation)表記法 ? ? ? ? ? GSNパターン アシュアランスケース言語の設計 プロトタイプ実装 関連研究 まとめ
- 14. constructed to be as flexible as possible such that they are applicable to a wide range of systems. There are a wide range of different development processes used on different projects, and it is important that the argument pattern may be instantiated no matter what development process is used. The structure of the pattern is therefore based upon a generalized ‘tier’ model of development such as that proposed in reference 10. Each tier corresponds to one level of decomposition of the design. The number of tiers of development may be different for different software systems, but the general safety considerations at each tier are unchanged. In addition, different parts of the design of any software system may be decomposed over a different number of tiers. Note that the term ‘tier’ is used principally to avoid the potential confusion of overloading the term ‘level’. GSNパターン ? ループ構造 R. Hawkins et al A Systematic Approach for Developing Software Safety Arguments, ループカウンタ Figure 4 - The structure of the software contribution safety argument pattern ISSC2009
- 15. 内容 ? アシュアランスケースについて – GSN (Goal Structuring Notation)表記法 ? ? ? ? ? GSNパターン アシュアランスケース言語の設計 プロトタイプ実装 関連研究 まとめ
- 16. アシュアランスケース/GSNの課 題 ? GSN, GSNパターンの形式的な定義が定まっ ていない – 実装したツールがまだない – 例えば、パラメータのスコープなどが定義さ れてない ? 関数型言語の形式を利用すると容易なの ではないか ? GSN, GSNパターンを形式化、プロトタイプ 実装
- 17. GSNの構造化 (G4, S2, ((G5, E2),(G6, ◇)),C2)
- 18. パターンの定義 ? パラメータにスコープ、型を導入 Definition of Availability Definition of SIL SILのs スコープ パラメタの型 Availability のスコープs
- 20. パターンの定義 ? ループの導入 α α α μα.T -> T[μα.T / α]
- 21. GSNパターンの定義 1からk (i <= k <= j) 番目のサブパターンを 選択 k (i <= k <= j) 個複製 例 g = “{システム}はディペンダブルである” {システム}はパラメータ ループ
- 22. 骋厂狈パターンのインスタンス化
- 23. パターンとインスタンスの関係
- 25. プロトタイプ実装 D-Case Editor ? DEOSプロジェクトで開発したオープン ソースのGSNエディタ ? グラフィカル表記、パターン、モジュー ル – パターンは現時点でパラメタのみ ? Assure-Itなどと互換性 ? Google “D-Case Editor”
- 26. 関連研究 ? Makoto Takeyama, D-Case/Agdaツール – 関数型言語/定理証明器Agdaを用いたGSNの形式 化 他に形式手法の ? 関数型言語?GSNの対応に基づく世界初のツール – ユーザはAgdaを理解することが必要 応用研究あり ? どこまで形式性を導入するかは課題 ? E.Denny, G.Pai. A Formal Basis for Safety Case Patterns, SAFECOMP2013 – GSNをコントロールフローグラフとみなし、 GSNパターンを形式化 – 定義、変換アルゴリズムが複雑
- 27. まとめ ? アシュアランスケース言語の設計と実装へむ けて、GSNパターンを形式化、プロトタイプ 実装を行った – 関数型言語の形式を用いることにより、容易に形 式化、実装できた – 有用なパターンをどれぐらい表現できるか今後検 証 ? 安全性認証などのために構造化ドキュメント が導入されつつある。パターン、モジュール、 整合性検査などに、関数型言語の形式がより 適用できる可能性がある