Microsoft Word - _DEIM2014_Shida.docx

Transcription

1 DEIM Forum 2014 E3-6 AssureNote: Wiki 記 法 ベースの GSN オーサリングツール 松 村 哲 郎 志 田 駿 介 倉 光 君 郎 横 浜 国 立 大 学 大 学 院 神 奈 川 県 横 浜 市 保 土 ヶ 谷 区 常 盤 台 79-1 横 浜 国 立 大 学 神 奈 川 県 横 浜 市 保 土 ヶ 谷 区 常 盤 台 {matsumura.t.lab, shunsuke.sida, あらまし 本 論 文 では,Wiki 記 法 ベースの GSN エディタ AssureNote の 提 案 を 行 う.GSN は,Assurance Cases のビジュアル 表 記 法 として 標 準 化 が 進 み,オーサリングツールが 開 発 されている.しかし, 従 来 のオーサリングツ ールは, 図 形 エディタをベースにしており,エディタを 利 用 出 来 ない 環 境 では Assurance Cases の 再 利 用 性 がえられ ない. 我 々は,Wiki 記 法 ベースの 表 記 法 を 提 案 し,データ 再 利 用 性 とグラフィカル 編 集 の 両 立 を 実 現 するツールを 開 発 した. キーワード Wiki,Assurance Cases,GSN 1. はじめに 本 論 文 では,Assurance Cases の 代 表 的 なビジュアラ イズ 方 である GSN の, Wiki 記 法 ベースの 編 集 法 を 採 用 した 編 集 ツールである AssureNote を 提 案 する. Assurance Cases はシステムの 安 全 性 やディペンダビリ ティ 要 求 を 議 論 し, システムのステークホルダ 間 で 合 意 を 形 成 するための 技 術 文 章 である. GSN は, Assurance Cases の 代 表 的 なビジュアル 記 法 であり, GSN を 用 いて Assurance Cases を 記 述 するための GSN オーサリングツールの 開 発 が 行 われている. しかし, 従 来 のオーサリングツールは Eclipse の 図 形 描 画 プラ グインを 利 用 するなど, 図 形 エディタをベースとして 開 発 されており,Assurance Cases のデータ 再 利 用 性 が えられない. 例 えば,こうした GSN オーサリングツー ルではツール 上 のユーザインターフェースを 介 した 編 集 のみを 想 定 しており, 保 存 形 式 である SACM (Structured Assurance Case Metamodel) や ARM (Argument Meta Model)を 直 接 編 集 することは 難 しい. そこで 我 々は, Wiki 記 法 ベースの 表 記 法 を 採 用 し, データの 再 利 用 性 とグラフィカル 編 集 の 両 立 を 実 現 す る GSN オーサリングツールである AssureNote を 提 案 する. AssureNote は WGSN (Wiki-Style GSN)のエディ タを GSN 編 集 のインターフェースとして 採 用 してい る. WGSN はテキストベースの 統 一 的 な GSN 編 集 の ために 設 計 された 表 記 法 であるが, 変 数 の 定 義 やノー ドの 参 照 など,GSN の 記 述 に 十 分 な 機 能 を 備 えている. WGSN の 記 法 を 用 いることで, 木 構 造 で 表 される GSN を, AssureNote 上 のテキストエリア 上 から 編 集 するこ とが 可 能 となり, 複 雑 なユーザインターフェースを 介 さない GSN の 編 集 が 実 現 される. 本 論 文 の 構 成 は 以 下 の 通 りである. 第 2 章 では GSN の 説 明 を 行 い, 第 3 章 では 関 連 研 究 について 説 明 する. 第 4 章 では AssureNote の 設 計 について 述 べ, 第 5 章 で は WGSN について 説 明 する. 第 6 章 では 実 装 を 述 べる. 第 7 章 では AssureNote を 使 った 実 証 実 験 を 行 う. 最 後 に, 第 8 章 で 本 論 文 を 総 括 する. 2. GSN (Goal Structuring Notation) GSN の 表 記 法 の 抜 粋 を 図 1 に 示 す.GSN は 主 に Goal, Strategy, Context, Evidence の 4 種 類 のノードから 成 る 木 構 造 の 表 記 法 である. それぞれの 意 味 と 役 割 は 以 下 の 通 りである. Goal: 安 全 性 やセキュリティ,ディペンダビリテ ィといった,システムが 満 たすべき 性 質 が 満 たさ れていることを 示 すための 主 張 である. Context: システムの 状 態 や 構 成 要 素 といった 前 提 条 件 を 示 す 際 に 用 いられるノードである. Strategy: Goalをいくつかの SubGoal に 分 割 する ための 議 論 構 造 を 表 す. 例 えば, システムの 構 成 要 素 ごとに 考 える という Strategy は, シス テムは 安 全 である という Goal を, サブシステ ム A は 安 全 である, サブシステム B は 安 全 で ある, サブシステムの 相 互 作 用 は 安 全 である に 分 割 する. Evidence: Goal が 成 立 することを 示 すための 証 跡 である. 例 えば,ソフトウェアテストの 結 果 や 合 意 書 などが Evidence として 用 いられる.Evidence に 支 持 されていない Goal は 下 部 にひし 形 の Undeveloped エ ン テ ィ テ ィ が 付 与 さ れ, Undeveloped Goal として 区 別 される. 3. 関 連 研 究 本 章 では, 関 連 研 究 及 び GSN オーサリングツールの 開 発 動 向 について 説 明 する.

2 Assurance Cases の 基 となる Safety Cases はシステム が 十 分 に 安 全 であることが 正 当 な 証 跡 によって 示 され た, 構 造 化 された 議 論 を 表 す 文 章 と 定 義 されており[6], 例 えば 原 子 力 産 業 においてはプラントでの 怪 我 や 生 命 の 危 機 を 引 き 起 こすものや 故 障 の 分 析 と,それらが 引 き 起 こされる 確 率 が 十 分 に 低 いことを 示 すために 用 い られている.この 他 にも 特 に 人 命 に 関 わるシステムへ の 適 用 に 感 心 が 高 まってきている[5][7]. GSN の 図 形 描 画 を 行 うためのエディタは 複 数 存 在 する.Adelard LLP が 開 発 する ASCE[4]は GSN や GSN の 議 論 構 造 の 基 となる CAE の 編 集 を 行 うためのツー ルである. 商 用 利 用 が 進 んでいるものの, 有 料 のツー ルであり,また Windows のみでしかサポートされてい ない.Eclipse のプラグインとして 開 発 された D-Case Editor[3]は ASCE と 同 等 の 機 能 を 持 っており, 近 年 ソ ースコードが 公 開 されたオープンソースソフトウェア である. この 他 にも NASA が 開 発 した GSN のオーサリング ツールとして,CertWare[1]や,GSN の 議 論 構 造 をパタ ーンとして 再 利 用 し, 自 動 的 に 展 開 する 機 能 を 持 つ AdvoCATE[2][8]がある. インの 3 つを 用 いて 行 う. サイドメニューは AssureNote の 編 集 画 面 の 左 上 部 に 常 に 表 示 されるメニ ュー 群 を 差 し,WGSN ファイルの 読 み 込 みや 保 存 を 行 うメニューが 表 示 される.メニューバーは 図 2 に 示 す とおり,ノードを 右 クリックすることで 表 示 される 項 目 群 を 指 す.コマンドラインは,コマンドをタイプす ることで 動 作 する 機 能 である. それぞれ,WGSN の 保 存 などの 常 に 有 効 な 操 作 と, ノード 毎 に 行 う 操 作, 補 助 的 な 操 作 として 分 類 される. これらのユーザインターフェースは, 後 述 のプラグイ ン 機 構 を 用 いることで 拡 張 することが 可 能 である. 図 2 メニューバーの UI 4.2. プラグイン 機 構 AssureNote は,WGSN が 編 集 機 能 の 中 心 として 採 用 され, 複 雑 なユーザインターフェースの 表 示 箇 所 を 限 定 する 設 計 を 行 っており, 基 本 機 能 はシンプルな 設 計 となっている. 我 々は 機 能 の 拡 張 を 行 うための, プラ グイン 機 構 を 採 用 した. プラグインはファイル 単 位 で 定 義 されており, AssureNote のソースツリー 内 の 特 定 の 箇 所 に 配 置 することで 有 効 化 される. AssureNote を ブラウザで 読 み 込 む 際 にエントリポイントが 呼 び 出 さ れ,プラグインの 初 期 化 と AssureNote への 登 録 を 行 う. 5. WGSN (Wiki-Style GSN) 本 説 では Wiki スタイルの GSN 表 記 法 である WGSN の 設 計 について 説 明 する. 図 3 は,WGSN の 表 記 法 の 定 義 のうち,Goal に 関 する 箇 所 を 抜 粋 したものである. 図 1 Goal Structuring Notation( GSN) 4. AssureNote の 設 計 本 章 では, AssureNote の 設 計 について 説 明 する ユーザインターフェースと 編 集 機 能 AssureNote のユーザインターフェースは 主 に,( 1) サイドメニュー,( 2)メニューバー,( 3)コマンドラ

3 Goal は WGSN の 記 法 上 は 定 義 されておらず, AssureNote などの GSN オーサリング 上 で, Evidence の 存 在 しない Goal に 対 して 自 動 的 に Undeveloped エン ティティを 付 与 する 設 計 となっている. ラベルの 直 後 にコロン : か ら 開 始 さ れ る シ ン ボ ル を 記 述 す る こ と が 可 能 だが, これはノードを 一 意 に 表 す 際 に 用 いられ る 識 別 子 として 扱 われる ノードの 親 子 関 係 ノードの 親 子 関 係 は 以 下 のルールに 基 づき, アスタ リスクの 数 によって 決 定 される. 図 3 WGSN の 表 記 法 5.1. WGSN への 要 求 第 1 章 でも 述 べたとおり, 我 々は WGSN を 用 いた GSN をテキストベースの 編 集 を 実 現 することで,デー タの 再 利 用 性 を 高 めることを 目 的 としている. そのた めには, WGSN には GSN を 記 述 するに 足 る 十 分 な 表 現 力 が 必 要 となる. 我 々は,WGSN に 要 求 される 記 述 力 を, 以 下 のように 定 義 した. GSN の 基 本 構 造 を 記 述 することができる 能 力. GSN のノードを 定 義 し, ノード 間 の 親 子 関 係 をテキストベースで 表 す 必 要 がある. 既 存 の GSN エディタがサポートする 機 能 を WGSN のみで 表 現 することができる 能 力. AssureNote における GSN の 編 集 を, WGSN を 中 心 に 行 うためには, 既 存 のエディタが GUI を 用 いて 行 っていた 操 作 をテキストベースで 表 現 しなければならない. 特 に 後 者 の 要 求 に 対 して,WGSN を 機 械 的 に 解 釈 す るためのタグと 呼 ばれる 記 法 を 定 義 することで, 既 存 の GSN エディタが 持 つ 機 能 と 同 等 のものをサポート する 設 計 を 行 った 基 本 構 造 WGSN は Wiki 表 記 を 基 にして 開 発 されたものであ る.それぞれのノードはアスタリスク * か ら 始 ま る ラベル 行 を 先 頭 とし, それ 以 降 の 自 由 記 述 が 可 能 な 行 とで 構 成 される.Goal, Context, Strategy, Evidence のい ずれかのノードを 示 すためのラベルは,G, C, S, E のよ うに 各 ノードのイニシャルを 用 いる. Undeveloped 図 N 個 のアスタリスクを 持 つ Goal は N-1 個 のアスタリスクを 持 つ 直 前 の Strategy の 子 N 個 のアスタリスクを 持 Strategy と Evidence は N-1 個 のアスタリスクを 持 つ 直 前 の Goal の 子 N 個 のアスタリスクを 持 つ Context は, N 個 のアスタリスクを 持 つ 直 前 のノードの 子 最 上 位 の Goal (TopGoal) はアスタリスク 一 つ 4 は, WGSN の 記 述 例 である. この 例 では, G:TopGoal が 最 上 位 の Goal であり, C:Context と S の ラベルを 持 つ 二 つのノードがその 子 となっている. G:SubGoal の アスタリスクの 数 は 2 つとなっているが, これは G:SubGoal が S の 子 であることを 表 す タグ ラベル 行 以 降 はノードの 本 文 となる. 自 由 記 述 が 可 能 な 箇 所 だが,WGSN ではタグと 呼 ばれる 記 法 を 用 い ることでパラメータの 定 義 を 行 うことができる. 図 4 の 例 では,C:Context においてタグの 定 義 がなされてお り, システム というパラメータに 対 して Web 教 育 システム という 値 がセットされている. タグの 記 法 を 用 いることで,より 構 造 化 された GSN を 記 述 する ことが 可 能 である. この 例 では Web 教 育 システム に 用 いられている WGSN を, 改 良 された Web 教 育 シ ステム へと 容 易 に 修 正 することができる. また, タグは AssureNote 上 で WGSN をレンダリン グする 際 の 補 助 として 用 いられる 他, Evidence として 実 行 時 のシステムの 状 態 を 与 えるためのモニタリング 機 構 などに 用 いられる. これらの 機 能 は 後 述 のプラグ イン 機 構 を 用 いて 拡 張 することが 可 能 である.

4 6. AssureNote の 実 装 AssureNote は Web ブラウザ 上 で 動 作 する Web アプ リケーションとして 実 装 されており, JavaScript 生 成 言 語 である TypeScirpt が 使 用 されている. 静 的 な HTML と JavaScript ファイルによって 構 成 され, サー バサイドとのやりとりは 無 い. このため, ユーザは AssureNote のファイル 群 を 事 前 に 入 手 し, オフライン 環 境 で 使 用 することが 可 能 である. 図 5 は AssureNote の 編 集 画 面 を 示 している.AssureNote は WGSN を 主 な 編 集 法 としているため,Eclipse をベースとした 多 くの GSN オーサリングツールと 比 較 して,ボタン 等 のユー ザインターフェースが 少 ないのが 特 徴 である. 図 4 WGSN の 例 5.5. ラベルとタグの 参 照 シンボルによって 一 意 に 表 されたラベルやタグを 参 照 するには 角 括 弧 [] を 用 いる. 図 4 の 例 では, G:TopGoal において[システム]と 書 かれている 箇 所 や, C:Context で [G:TopGoal]とラベルを 参 照 している 箇 所 で 使 用 されている. これらの 記 法 を 用 いて 記 述 された WGSN を AssureNote 上 で 閲 覧 すると,AssureNote が 自 動 的 に 割 り 振 った 値 に 置 き 換 えて 表 示 される. 定 義 されたラベルは WGSN 中 のあらゆる 箇 所 から 参 照 することが 可 能 である. 他 方, タグにはスコープ が 定 義 されており, スコープの 外 からこれを 参 照 する ことは 出 来 ない. タグのスコープの 以 下 の 通 りに 定 義 される. 定 義 されたタグはその 子 ノードや 孫 ノードの みで 参 照 することができる 例 外 として, Context で 定 義 されたタグのスコ ープは, Context の 親 と 同 一 である タグが 重 複 して 定 義 されている 場 合 は, 最 も 近 い 親 のものが 優 先 される Context は Goal や Strategy の 前 提 条 件 を 記 述 するた めのノードであるため, 例 外 的 なスコープを 持 つ. 図 4 の 例 では, システム を 定 義 する C:Context は 子 を 持 たないが,その 親 である G:TopGoal と 同 じスコープ を 持 つためこれを G:TopGoal や E で 参 照 することがで きる. 図 5 AssureNote の 編 集 画 面 6.1. WGSN パーサの 実 装 WGSN パーサは, 第 5 章 で 定 義 される WGSN の 構 文 解 析 などを 行 う 機 構 であり, 主 に 以 下 の 二 つの 役 割 を 持 つ. 1. 構 文 解 析 :WGSN の 構 文 解 析 を 行 い, 抽 象 構 文 木 ( AST)を 生 成 する 機 能. なお, WGSN の AST はそのまま AssureNote の 内 部 表 現 として 用 いら れる. 2. WGSN 生 成 : 任 意 の AST から WGSN を 生 成 する 機 能. AssureNote 上 で 編 集 中 の GSN をエディタ へと 出 力 する 際 や,WGSN 形 式 で 保 存 する 際 に 用 いられる. AssureNote は, 任 意 のノードの 部 分 木 のみを 編 集 す る 機 能 を 持 つため, WGSN パーサは GSN 中 の 任 意 の 箇 所 からパース WGSN 生 成 が 行 える 必 要 がある.そ のため,WGSN 生 成 を 行 う 際 にはノードの 親 子 関 係 を 表 すアスタリスクの 数 を 必 ず 1 から 始 まるようになっ ている. このため, TopGoal 以 外 のノードから WGSN 生 成 を 行 った 際, 生 成 された WGSN の 見 かけ 上 は WGSN 生 成 の 基 点 となるノードが TopGoal となる.な お,Strategy や Context,Evidence を 基 点 として WGSN

5 生 成 を 行 う 事 も 可 能 だが, その 場 合 もアスタリスクは 1 から 開 始 される 編 集 機 構 AssureNote の 編 集 機 構 はそれぞれのノードを 右 クリ ックすることで 表 示 されるメニューバーから 行 う. メ ニューバーの 中 には WGSN による 編 集 を 行 うための エディタを 開 くメニューが 存 在 し, これを 編 集 のため に 主 に 用 いるが, ノードの 削 除 など 一 部 の 操 作 につい ては UI から 行 う プラグイン 機 構 の 実 装 AssureNote の プラグインの 分 類 は 以 下 に 述 べる 通 り である. プラグインの 実 行 は, レンダリングの 開 始 時 点 や, メニューバーの 選 択 時 などに 設 定 されるフック ポイントから 行 われる WGSN を 用 いた 編 集 機 構 図 6 は AssureNote 上 で WGSN を 編 集 する 際 に 用 い られる 全 画 面 エディタを 表 している. 全 画 面 エディタ は 各 ノードのメニューバーから 開 くことができるが, メニューバーを 表 示 されるノードに 応 じて 全 画 面 エデ ィタ 上 の WGSN は 変 化 する. 最 上 位 の Goal である TopGoal から 全 画 面 エディタを 表 示 させた 際 は WGSN の 全 体 をエディタ 上 から 編 集 することが 出 来 るが, そ れ 以 外 の 任 意 のノードの 場 合 は, その 部 分 木 に 当 たる 箇 所 のみが WGSN 生 成 器 を 用 いてエディタ 上 に 表 示 される. 図 7 プラグインによるレンダリング UI の 拡 張 プラグイン AssureNote 上 のサイドバーやメニューバーに 項 目 を 追 加 する. メニューに 表 示 される 画 像 や 項 目 名 を 指 定 し, 項 目 が 選 択 された 際 の 処 理 を 記 述 する コマンドライン 拡 張 プラグイン AssureNote で 補 助 的 な 操 作 を 行 うためのコマンドラ インで 使 用 するコマンドは, 組 み 込 みの 物 も 含 めて 全 てがプラグインとして 実 装 されている. コマンドライ ン 拡 張 プラグインでは, コマンド 名 と, パースされた コマンド 引 数 を 基 に 処 理 を 行 う 関 数 を 定 義 する. プラ グインとして 定 義 される 機 能 の 抜 粋 を 以 下 に 示 す. な お, これらのコマンドには 引 数 が 必 要 となるものも 存 在 するが, 省 略 して 説 明 を 行 う. 図 6 全 画 面 エディタ 6.4. 補 助 的 な 編 集 機 構 前 述 の 通 り, 一 部 の 編 集 機 能 はメニューバーから 直 接 呼 び 出 すためのボタンが 備 わっている. ただし, こ れらの 機 能 は WGSN を 用 いたテキストベースの 編 集 の 欠 点 を 補 うことを 目 的 としている. ノードの 削 除 を 行 うためのメニューはその 代 表 で ある. WGSN を 用 いたノードの 削 除 を 行 うためには, 削 除 したいノードの 部 分 木 に 当 たる 箇 所 を 全 て 選 択 し, 削 除 しなければならず, 操 作 が 煩 雑 になってしまう. そこで, 右 クリックでメニューバーを 表 示 したノード の 部 分 木 を 削 除 する 機 能 は,WGSN を 用 いた 編 集 機 能 とは 別 途 用 意 した. help:ヘルプの 参 照 new: TopGoal のみの 新 しい GSN を 作 成 する open:ファイルを 開 く save:ファイルを 保 存 する save-as-svg: SVG 形 式 でファイルを 保 存 する set-scale: GSN の 拡 大 率 を 変 更 する set-color:ノードを 色 付 けする connect: 複 数 人 同 時 編 集 サーバへ 接 続 同 時 編 集 者 へメッセージを 送 信 する レンダリングプラグイン レンダリングプラグインは, 画 像 の 表 示 や 特 定 のノ ードのスタイルを 変 更 する 際 に 用 いられる. ただし, レンダリングプラグインは 個 々のノードのレンダリン グを 行 うためのものであり, AssureNote のレイアウト の 変 更 やノードの 配 置 を 変 更 することはできない.

6 WGSN のタグを 解 釈 することで,レ ンダリングを 行 う. 例 えば, TODO を 表 示 するプラグインでは, TODO というパラメータが 定 義 されているか, 空 の 値 がセッ トされているパラメータが 定 義 されているノードは 枠 が 点 線 で 表 示 される. 図 7 の 例 では, 3 つの Context のスタイルがレンダリングプラグインによって 変 更 さ れている. 7. GSN の 記 述 実 験 本 章 では,AssureNote を 用 いて GSN を 記 述 し,WGSN を 用 いることで GSN の 記 述 に 十 分 な 表 現 が 可 能 であ ることを 確 認 する.ここで WGSN の 表 現 力 とは, 第 1 章 で 述 べた 通 り,( 1) 木 構 造 の 文 書 である GSN の 基 本 的 な 構 造 を 定 義 することが 可 能 な 点 と,( 2) 既 存 の GSN エディタが GUI を 用 いて 行 っていた 操 作 が, WGSN を 用 いて 表 現 可 能 な 点 である. た Assurance Cases は 表 1 の 通 り,250 ノードとなった. この Assurance Cases は 854 行 の WGSN として 編 集 が 行 われたものである. 既 存 の GSN オーサリングツールとは 異 なり, GSN の 編 集 を,WGSN を 用 いて 行 うため, 記 法 の 習 得 に 不 慣 れな 段 階 では 編 集 に 手 間 取 る 場 合 が 見 受 けられた. しかし,WGSN に 慣 れてきた 実 験 参 加 者 は,WGSN の 一 部 をコピー&ペーストすることで GSN の 部 分 木 をそ のまま 複 製 するといった 操 作 手 法 を 独 自 に 見 つけ 出 し, 用 いていた.こうした 機 能 は 他 の GSN オーサリングツ ールでも 採 用 されている 機 能 の 一 つである. 既 存 の GSN オーサリングツールでは GUI のメニューより 一 つ 一 つノードを 作 成 し, 本 文 を 記 述 する 必 要 がある. 他 方,WGSN を 用 いることで,Assurance Cases 作 成 者 は 複 数 のノードの 追 加 や 削 除, 編 集 を 行 う 事 ができる Web 教 育 システムの GSN 本 記 述 実 験 では, 我 々が 開 発 を 行 っている Aspen と 呼 ばれる Web 教 育 システム( 図 8)の Assurance Cases を AssureNote に 組 み 込 まれた WGSN を 用 いて 記 述 す る. そして, WGSN を 用 いた GSN の 基 本 的 な 構 造 の 記 述 が, 実 際 のシステムの Assurance Cases を 記 述 する 際 にも 十 分 に 有 用 であることを 確 認 する. Aspen はプログラミング 初 学 者 向 けの 教 育 システム であり, ブラウザ 上 でプログラムを 記 述 し, その 結 果 を 表 示 することでプログラミング 学 習 を 進 めていく. Aspen はプログラムの 編 集 と 実 行 結 果 の 表 示 を 行 う Aspen クライアントと, ユーザデータの 管 理 やプログ ラムのコンパイルを 行 う Aspen サーバから 構 成 される. Aspen サーバはロードバランサによって 冗 長 化 されて おり,2 つのアプリケーションサーバが 動 作 している. 本 記 述 実 験 は Assurance Cases 記 述 経 験 が 豊 富 な 3 名 と, Aspen の 設 計 開 発 運 用 に 関 わった 技 術 者 を 中 心 として 行 われた.いずれのメンバも 既 存 の GSN オー サリングツールを 用 いた Assurance Cases の 作 成 経 験 はあるものの, AssureNote の 使 用 経 験 は 無 い. なお, 本 来 Assurance Cases の 作 成 はシステムの 設 計 段 階 か ら 始 める 必 要 があるが, 今 回 は 既 に 構 築 済 みのシステ ムに 対 して, システムの 設 計 から 運 用 を 担 当 した 技 術 者 への 聞 き 取 りの 基, 当 時 のプロセスを 追 跡 する 形 で 行 われた. 記 述 実 験 参 加 者 は Aspen はディペンダブルである を TopGoal として 設 定 し, Aspen のディペンダビリテ ィを, Aspen は 正 常 に 運 用 することができる 運 用 者 は Aspen のリスク 毎 に 障 害 対 応 できる Aspen は 要 求 の 変 化 に 対 して 対 応 することができる の SubGoal に 分 割 し, それぞれについて 議 論 を 行 った. 作 成 され 図 8 Aspen の 操 作 画 面 表 1 記 述 実 験 で 作 成 された GSN の 概 要 ノード 数 250 ノード WGSN の 行 数 854 行 8. まとめ 我 々は,Assurance Cases の 代 表 的 なビジュアル 表 記 法 である GSN の データ 再 利 用 性 とグラフィカル 編 集 機 能 を 両 立 させた GSN オーサリングツールである AssureNote の 設 計 と 実 装 を 行 った. AssureNote は GUI による 機 能 の 追 加 を 最 小 限 に 抑 え, プラグインによる 機 能 拡 張 を 行 う 設 計 がなされている.そのために,GSN をテキストベースで 編 集 するための 表 記 法 である WGSN の 設 計 を 行 い, WGSN のパーサを AssureNote に 組 み 込 んだ.WGSN を 用 いることで,GSN オーサリ ングツールの 補 助 無 しに 十 分 な 記 述 力 を 得 る 事 が 可 能 となり, AssureNote の 機 能 拡 張 も 容 易 に 行 う 事 が 可 能 であった. また, GSN の 基 本 構 造 の 記 述 や, 既 存 の GSN オーサリングツールが 持 つ 機 能 のサポートが AssureNote でも 行 えることが 記 述 実 験 より 確 認 された. 我 々が 行 った AssureNote の 記 述 実 験 では,WGSN の

7 記 述 力 や 機 能 性 関 して AssureNote 使 用 者 の 感 覚 的 な 変 化 にのみ 注 目 しているため, 同 一 の Assurance Cases の 作 成 コストの 比 較 など, 定 量 的 な 評 価 が 必 要 である. 現 在 の AssureNote はサーバとのやりとりなしにブラ ウザ 上 で 動 作 するアプリケーションとなっている. 現 在 実 装 が 行 われており, 試 験 的 に 導 入 されている 複 数 人 による GSN の 同 時 編 集 機 能 やサーバへの GSN アッ プロード 機 能 などのサポートを 行 い, 実 用 的 なソフト ウェアを 目 指 す 予 定 である. AssureNote はオープンソースで 開 発 が 行 われている ソフトウェアであり, 下 記 の URL から 自 由 にダウンロ ードし, 使 用 する 事 が 可 能 である. また, これらの 入 手 可 能 なファイルは 下 記 の URL に 設 置 されており, ブラウザ 上 からアクセスすること で AssureNote を 使 用 することができる. and Security. Springer Berlin Heidelberg, 謝 辞 本 研 究 は,JST/CREST 実 用 化 を 目 指 した 組 込 みシステム 用 ディペンタブル オペレーティングシ ステム 領 域 の 研 究 課 題 実 行 時 の 安 全 性 を 確 保 する SecurityWeaver と P-SCRIPT の 一 部 として 行 われた. 参 考 文 献 [1] Matthew R. Barry CertWare: A workbench for safety case production and analysis. In Proceedings of the 2011 IEEE Aerospace Conference (AERO '11). IEEE Computer Society, Washington, DC, USA, [2] Ewen Denney, Ganesh Pai, and Josef Pohl AdvoCATE: an assurance case automation toolset. In Proceedings of the 2012 international conference on Computer Safety, Reliability, and Security (SAFECOMP'12), Frank Ortmeier and Peter Daniel (Eds.). Springer-Verlag, Berlin, Heidelberg, [3] Matsuno, Yutaka, Hiroki Takamura, and Yutaka Ishikawa. "A dependability case editor with pattern library." High-Assurance Systems Engineering (HASE), 2010 IEEE 12th International Symposium on. IEEE, [4] LLP, A.: Adelard ASCE, [5] Jee, Eunkyoung, Insup Lee, and Oleg Sokolsky. "Assurance cases in model-driven development of the pacemaker software." Leveraging Applications of Formal Methods, Verification, and Validation. Springer Berlin Heidelberg, [6] ine Menon, Cather, Richard Hawkins, and John McDermid. "Defence standard issue 4: Towards evidence-based safety standards." Safety-Critical Systems: Problems, Process and Practice. Springer London, [7] Bloomfield, Robin, and Peter Bishop. "Safety and assurance cases: Past, present and possible future an Adelard perspective." Making Systems Safer. Springer London, [8] Denney, Ewen, and Ganesh Pai. "A Formal Basis for Safety Case Patterns." Computer Safety, Reliability,