博 士 論 文 概 要

早稲田大学大学院 基幹理工学研究科

博 士 論 文 概 要

論 文 題 目

離散事象システムのための充足可能な安全性 の識別に関する研究

Satisfiable Safety Property Identification for Discrete Event Systems

申 請 者

相澤 和也 Kazuya AIZAWA

情報理工・情報通信専攻 自律エージェント工学研究

2020 年 5 月

No. 1

離 散 事 象 シ ス テ ム と は 事 象 の 発 生 に よ っ て 状 態 が 離 散 的 に 遷 移 す る シ ス テ ム で あ る ． 業 務 系 の シ ス テ ム や 交 通 シ ス テ ム ， 生 産 管 理 シ ス テ ム な ど の よ う に ， 離 散 事 象 シ ス テ ム は こ の 数 十 年 間 で 我 々 の 社 会 に 不 可 欠 な も の と な っ た ． 離 散 事 象 シ ス テ ム に お い て ， 望 ま し い 事 象 を 発 生 さ せ ， 望 ま し く な い 事 象 を 抑 制 す る こ と は 当 該 シ ス テ ム の 重 要 な 要 求 と し て 挙 げ ら れ る ． 特 に 「 起 き る べ き 事 象 が 常 に い つ か は 起 き る 」 と い う 活 性 要 求 （l i v e n e s s p r o p e r t y） と 「 起 き る べ き で な い 事 象 は 決 し て 起 き な い 」 と い う 安 全 性 要 求 （s a f e t y p r o p e r t y） を 充 足 す る と い う 課 題 は 数 十 年 間 に 渡 っ て 頻 繁 に 扱 わ れ て き た ．

離 散 事 象 シ ス テ ム の 動 作 環 境 で は シ ス テ ム 自 身 が 制 御 可 能 な 事 象 と 制 御 不 能 な 事 象 が 存 在 す る ． シ ス テ ム の 制 御 器 は 制 御 不 能 な 事 象 の 発 生 を 検 知 し な が ら 制 御 可 能 な 事 象 を 発 生 さ せ る こ と で 与 え ら れ た 活 性 や 安 全 性 を 充 足 し よ う と す る ． こ れ ら の 要 求 の 充 足 可 否 は 動 作 環 境 に 置 く こ と の で き る 仮 定 に 依 存 す る ． 制 御 不 能 な 事 象 に 対 し て そ の 発 生 の 有 無 に 仮 定 を 置 き ， そ の 仮 定 に 基 づ い て 活 性 や 安 全 性 を 充 足 す る 動 作 仕 様 を 構 築 す る ． し か し ， 実 環 境 に 対 し て 置 く こ と の で き る 仮 定 に は 不 確 実 性 が あ り ， シ ス テ ム の 運 用 初 期 に は 成 立 し た 仮 定 も 動 作 環 境 の 変 化 に よ っ て 崩 れ る こ と が 考 え ら れ る ． 業 務 遂 行 に 不 可 欠 な シ ス テ ム は ど の よ う な 環 境 で も 安 全 に 動 作 を 継 続 す る こ と が 求 め ら れ る ． し た が っ て 離 散 事 象 シ ス テ ム の 開 発 者 に は 仮 定 の 崩 れ た 環 境 下 で も 最 大 限 に 安 全 性 を 充 足 す る よ う に 動 作 仕 様 を 策 定 す る こ と が 求 め ら れ る ．

離 散 事 象 シ ス テ ム の 開 発 に お い て ， 策 定 し た 動 作 仕 様 が 与 え ら れ た 活 性 や 安 全 性 を 充 足 す る こ と を 保 証 す る た め に 多 く の コ ス ト が 費 や さ れ て き た ． こ れ は シ ス テ ム の 誤 っ た 動 作 に よ る 経 済 的 ， 人 的 損 失 の リ ス ク を 低 減 す る た め で あ り ， 特 に シ ス テ ム の 動 作 継 続 に 関 わ る よ う な 安 全 性 の 充 足 の 保 証 は 注 力 さ れ る べ き も の で あ る ． 従 来 の シ ス テ ム 開 発 に お い て は 開 発 者 が 策 定 し た 動 作 仕 様 を 実 装 し て か ら テ ス ト 検 証 を 行 っ て き た ． し か し 社 会 的 ニ ー ズ に 応 え る た め に シ ス テ ム が 複 雑 化 し た こ と に 伴 い ，テ ス ト ケ ー ス の 作 成 に よ る 網 羅 的 な 検 証 が 困 難 と な っ た ．ま た ， テ ス ト を 通 じ て 発 見 さ れ た 仕 様 の 誤 り を 修 正 す る た め の 時 間 的 コ ス ト も 膨 大 と な っ て き た ． こ れ に 対 し て 実 装 前 に 動 作 仕 様 の 状 態 遷 移 モ デ ル を 構 築 し ， 形 式 化 し た 活 性 や 安 全 性 を 網 羅 的 に 検 証 す る モ デ ル 検 査 が 用 い ら れ る よ う に な っ た ． し か し な が ら ， 仮 定 が 崩 れ た 環 境 に お い て シ ス テ ム の 動 作 を 継 続 す る た め に は ， 仮 定 の 崩 れ た そ れ ぞ れ の 環 境 に お け る 動 作 仕 様 を 準 備 す る 必 要 が あ る ． こ れ ら の 仕 様 を 開 発 時 に 準 備 す る に は 高 い コ ス ト を 必 要 と す る ． ま た ， 離 散 事 象 シ ス テ ム の 運 用 時 に は 外 部 シ ス テ ム の エ ラ ー や 予 期 せ ぬ 環 境 の 変 化 に よ っ て 開 発 時 に 置 い た 仮 定 が 崩 れ る 可 能 性 も あ る ． 開 発 者 は こ の と き に も シ ス テ ム の 動 作 を 維 持 継 続 で き る よ う に ， 崩 れ た 仮 定 を 考 慮 し て 動 作 仕 様 を 変 更 す る こ と が 求 め ら れ る ． こ の と き ， 開 発 者 は 迅 速 に 動 作 仕 様 を 変 更 す る こ と が 求 め ら れ る が ， モ デ ル 検 査 を 用 い

No. 2

た 開 発 で は 依 然 と し て 動 作 仕 様 そ の も の の 策 定 は 人 手 で 行 わ れ る た め ， そ の 迅 速 化 に は 限 界 が あ る ．

仕 様 策 定 の 自 動 化 技 術 と し て 離 散 制 御 器 合 成（D i s c r e t e C o n t r o l l e r S y n t he s i s） の 研 究 が 進 め ら れ て き た ． 離 散 制 御 器 合 成 と は 与 え ら れ た 環 境 下 で 与 え ら れ た 要 求 を 充 足 す る 動 作 仕 様 モ デ ル の 合 成 を 試 み る 技 術 で あ る ． 動 作 環 境 を 状 態 遷 移 モ デ ル と し て ， そ し て 安 全 性 や 活 性 な ど の 要 求 を 線 形 時 相 論 理 式 の 集 合 と し て 定 式 化 す る こ と で 分 析 空 間 を 構 築 し ， 制 御 器 の 合 成 可 否 を 分 析 す る ． そ し て 合 成 が 可 能 で あ れ ば そ の モ デ ル を 出 力 す る の で あ る ． 離 散 制 御 器 合 成 で は ， 安 全 性 と 活 性 の 充 足 を 保 証 す る 動 作 仕 様 モ デ ル を 多 項 式 時 間 で 合 成 で き る ． こ れ を 用 い て 動 作 仕 様 を 自 動 合 成 す る こ と で 開 発 者 は 動 作 仕 様 そ の も の の 策 定 に 掛 け て い た 開 発 コ ス ト と ，活 性 や 安 全 性 の 充 足 に 対 す る 検 証 コ ス ト を 同 時 に 削 減 す る こ と が で き る ． ま た ， 離 散 制 御 器 合 成 は 環 境 と 要 求 を 定 め て か ら の 開 発 プ ロ セ ス を 自 動 化 す る こ と か ら ， そ の 適 用 範 囲 は 開 発 時 の み な ら ず 運 用 時 に ま で 広 が る ． 開 発 時 に は 想 定 し 得 な か っ た 事 象 が 運 用 時 に 発 生 し た 場 合 に ， そ の 事 象 を 動 作 環 境 の モ デ ル に 反 映 し て か ら 離 散 制 御 器 を 合 成 す る こ と で ， 要 求 の 充 足 を 保 証 し な が ら シ ス テ ム を 継 続 あ る い は 復 旧 す る こ と が で き る ．

し か し ， 離 散 制 御 器 合 成 の 失 敗 時 は そ の 旨 が 伝 え ら れ る の み で ， 与 え ら れ た 要 求 の 集 合 の 中 で 保 証 不 能 な も の と 保 証 可 能 な も の と の 識 別 な ど は 行 わ れ て こ な か っ た ． こ の た め ， 失 敗 時 に は 動 作 環 境 の モ デ ル お よ び 定 式 化 さ れ た 要 求 を 人 手 で 調 査 す る 必 要 が あ っ た ． 原 因 分 析 に お い て は 特 に 動 作 環 境 の モ デ ル の 改 善 よ り も 充 足 可 能 な 要 求 の 識 別 が 重 要 と さ れ る ． な ぜ な ら ば シ ス テ ム が 要 求 を 満 た せ る よ う に 動 作 環 境 を 完 全 に 整 え る こ と は 困 難 な た め で あ る ． し か し な が ら ， こ の 原 因 分 析 に は 離 散 制 御 器 合 成 の 背 景 技 術 で あ る プ ラ ン ニ ン グ や 2 人 対 戦 型 ゲ ー ム の 知 識 と 開 発 ド メ イ ン の 知 識 の 両 方 が 開 発 者 に 求 め ら れ ， 高 い コ ス ト を 要 す る ． こ の コ ス ト 削 減 の た め に 充 足 可 能 な 要 求 の 自 動 識 別 が 課 題 と な る ．

本 論 文 で は こ の 合 成 失 敗 時 の 原 因 分 析 を 支 援 す る た め に ， 動 作 環 境 の モ デ ル 上 で 充 足 可 能 な 要 求 を 識 別 す る た め の 分 析 空 間 構 築 手 法 と 分 析 ア ル ゴ リ ズ ム を 提 案 す る ． 特 に 本 研 究 で は 動 作 を 維 持 す る 上 で 保 証 が 不 可 欠 で あ り ， そ の 違 反 が 深 刻 な 問 題 と な り 得 る 安 全 性 を 識 別 す る ． 本 論 文 で は 安 全 性 と 活 性 の 両 方 を 扱 う こ と が で き ， 多 項 式 時 間 で の 制 御 器 合 成 を 可 能 と し て い る こ と か ら ，2 人 対 戦 型 ゲ ー ム を 背 景 と し た 離 散 制 御 器 合 成 を 対 象 と す る ． そ の 上 で ， 充 足 可 能 な 安 全 性 の 識 別 を 離 散 制 御 器 合 成 と 同 様 に 多 項 式 時 間 で 実 現 す る 手 法 を 提 案 す る ． ま た ， 開 発 時 の み な ら ず 運 用 時 の 利 用 を 想 定 し て 環 境 変 化 の 差 分 更 新 に 特 化 し た 効 率 的 な 識 別 手 法 も 提 案 す る ． 更 に ， 手 法 の 適 用 範 囲 を 拡 大 さ せ る た め ，2 人 対 戦 型 ゲ ー ム を 行 う 状 態 空 間 を 削 減 す る 手 法 も 提 案 す る ． こ の 削 減 は 充 足 可 能 な 安 全 性 の 識 別 に 不 要 な 情 報 の 抽 象 化 に よ っ て 実 現 す る ．

No. 3

本 論 文 は 第 1 章 か ら 第 7 章 ま で で 構 成 さ れ て お り ，第 1 章 で は 本 論 文 の 背 景 と 意 義 ・ 目 的 を 説 明 す る ． 続 く 第 2 章 で は 本 論 文 が 対 象 と す る 2 人 対 戦 型 ゲ ー ム を 用 い た 離 散 制 御 器 合 成 の 技 術 に つ い て 述 べ る ．

第 3 章 で は 開 発 時 を 想 定 し ， 離 散 事 象 シ ス テ ム の 達 成 目 標 に 当 た る 単 一 の 活 性 を 充 足 し よ う と す る と き に ， 同 時 に 充 足 可 能 な 安 全 性 を 識 別 す る ． こ の た め の ゲ ー ム の 定 式 化 と 識 別 ア ル ゴ リ ズ ム の 提 案 を 行 っ て い る ． こ の ア ル ゴ リ ズ ム は 入 力 で あ る 動 作 環 境 と 要 求 か ら 構 築 さ れ た ゲ ー ム 上 で ， 制 御 器 が ゲ ー ム の 勝 利 戦 略 を 持 て る 領 域 （ 以 下 ， 勝 利 領 域 と よ ぶ ） を 入 力 さ れ た 安 全 性 の 組 み 合 せ 毎 に 識 別 す る ． 第 3 章 の 貢 献 は （1） 活 性 と 同 時 に 充 足 可 能 な 安 全 性 を 識 別 可 能 な ゲ ー ム と 勝 利 領 域 の 定 式 化 ，（2） 勝 利 領 域 を 求 め る た め の ア ル ゴ リ ズ ム の 提 案 ，（3） ア ル ゴ リ ズ ム に よ り 勝 利 領 域 が 求 ま る こ と の 証 明 の 3 つ で あ る ．

第 4 章 で は 運 用 時 に 発 生 す る 想 定 外 の 事 象 に 即 応 的 に 対 応 す る た め の 支 援 を 行 う た め に ， 環 境 変 化 時 に 充 足 可 能 な 安 全 性 を 効 率 的 に 識 別 す る ア ル ゴ リ ズ ム を 提 案 し て い る ． こ の ア ル ゴ リ ズ ム が 扱 う 環 境 変 化 は ， 動 作 環 境 の モ デ ル に 新 し い 状 態 遷 移 関 係 が 追 加 さ れ る よ う な 場 合 で ， 環 境 変 化 に よ っ て 生 じ る 差 分 に 着 目 し ， 動 作 環 境 の モ デ ル 上 で 追 加 さ れ た 遷 移 に 基 づ い て 安 全 性 毎 に 特 定 さ れ た 勝 利 領 域 を 差 分 更 新 す る こ と で 計 算 時 間 を 削 減 し た ． 第 4 章 の 貢 献 は （1） 運 用 時 に 変 化 の 生 じ た 動 作 環 境 下 で 充 足 可 能 な 安 全 性 を 識 別 す る た め の ゲ ー ム と 勝 利 領 域 の 定 式 化 ，（2） 勝 利 領 域 の 差 分 更 新 を 行 う た め の ア ル ゴ リ ズ ム の 提 案 ，（3） ア ル ゴ リ ズ ム に よ り 勝 利 領 域 が 求 ま る こ と の 証 明 ，（4） ア ル ゴ リ ズ ム に よ っ て 充 足 可 能 な 安 全 性 を 識 別 す る ま で の 計 算 時 間 の 実 装 評 価 の 実 施 の 4 つ で あ る ．

第 5 章 で は 充 足 可 能 な 安 全 性 の 識 別 に 適 用 可 能 な 状 態 抽 象 化 手 法 を 提 案 す る ． 従 来 の 合 成 手 法 で は ， あ る 安 全 性 の 違 反 後 の 状 態 を 保 持 し た ま ま ， 他 の 安 全 性 の 充 足 状 況 を 観 測 し て 状 態 空 間 を 構 築 し て い た ． し か し ， 安 全 性 の 充 足 可 否 を 分 析 す る た め に は 充 足 す べ き 安 全 性 を 初 め て 違 反 す る 瞬 間 だ け を ゲ ー ム 空 間 が 記 憶 し て お け ば よ い ． ま た シ ス テ ム の 動 作 継 続 に 必 須 な 安 全 性 の 違 反 後 は 他 の 安 全 性 の 充 足 可 否 を 分 析 す る 必 要 が な い ． よ っ て ， 第 5 章 で は 安 全 性 を 必 須 と 任 意 に 分 類 す る ． そ し て 必 須 に 分 類 し た 安 全 性 を 違 反 し た 後 の 状 態 を 1 つ に 抽 象 化 す る ． 任 意 に 分 類 し た 安 全 性 に つ い て は 違 反 し た 安 全 性 に 関 す る 情 報 の み 抽 象 化 し ， そ の 他 の 安 全 性 の 分 析 を 継 続 可 能 に し な が ら 状 態 空 間 を 削 減 し た ．第 5 章 の 貢 献 は（1） 安 全 性 を 必 須 と 任 意 に 分 類 し 2 つ の 抽 象 化 を 併 用 す る 手 法 の 提 案 ，（2） 提 案 手 法 に よ っ て 削 減 さ れ た ゲ ー ム 空 間 が 充 足 可 能 な 安 全 性 を 識 別 す る た め の 条 件 を 満 た す こ と の 証 明 ，（3） 提 案 手 法 に よ る 分 析 空 間 の 状 態 削 減 効 果 の 評 価 ，（4） 提 案 手 法 に よ る 分 析 空 間 で の 保 証 可 能 な 安 全 性 識 別 の 計 算 時 間 の 評 価 の 4 つ で あ る ． 第 6 章 で は 本 研 究 に 関 連 す る 他 の 研 究 に つ い て 触 れ ， 第 7 章 で は 本 論 文 の 内 容 を ま と め ， 今 後 の 展 望 を 示 す ．

Ｎｏ.1

早稲田大学 博士（工学） 学位申請 研究業績書

氏 名 相澤 和也 印

（2020年 5月 現在）

種 類 別 題名、 発表・発行掲載誌名、 発表・発行年月、 連名者（申請者含む）

〇論文

〇論文

〇論文

〇査読付き 国際会議

〇査読付き 国際会議

査読付き 国際会議

その他 (口頭発表)

その他 (口頭発表)

その他 (口頭発表)

その他 (口頭発表)

「活性と同時に保証可能な安全性特定のためのゲーム分析アルゴリズム」，情報処理学会論文 誌，Vol. 61，No.4, pp.853 – 862，2020年4月，相澤 和也，鄭 顕志，本位田 真一 (査読 付)[フルペーパー]

「違反状態抽象化による保証可能な安全性特定のための分析空間削減」，電子情報通信学会論 文誌D，Vol.J103-D，No.04, pp.238 – 246，2020年4月，相澤 和也，鄭 顕志，本位田 真 一 (査読付)[フルペーパー]

「環境変化時に保証可能な安全性を特定するためのゲーム分析アルゴリズム」，情報処理学会 論文誌，Vol. 60，No.4，pp.1025 - 1039，2019年4月，相澤 和也，鄭 顕志，本位田 真一 (査読付)[フルペーパー]

“Analysis space reduction with state merging for ensuring safety properties of self-adaptive systems”, The 16th IEEE International Conference on Advanced and Trusted Computing 2019 (ATC 2019)，Leicester, U.K.，pp.1363 - 1370，2019.8，Kazuya Aizawa，Kenji Tei, Shinichi Honiden (査読付)[フルペーパー]

“Identifying safety properties guaranteed in changed environment at runtime”，The 3rd IEEE International Conference on Agent (ICA'18)，Singapore，pp.75-80，2018.7，Kazuya Aizawa，Kenji Tei, Shinichi Honiden (査読付)[フルペーパー]

“HoppingDuster: self-adaptive cleaning robot based on aerial vehicle”，2014 ACM International Joint Conference on Pervasive and Ubiquitous Computing: Adjunct

Publication，Seattle, U.S.，pp.271 - 274，2014.9，Kenji Tei, Kazuya Aizawa, Shunichiro Suenaga, Ryuichi Takahashi, Shun Lee, Yoshiaki Fukazawa (共著)(査読付)

[デモペーパー]

“Toward identifying safety properties guaranteed simultaneously with a liveness property at runtime”， The 8th Asian Workshop of Advanced Software Engineering (AWASE2019)，Fukuoka, Japan，2019.10，Kazuya Aizawa，Kenji Tei, Shinichi Honiden

“Identifying physical security risks with using two-players game at runtime”，GRACE Workshop on Smart-city and Security，Hakone, Japan，2018.12，Kazuya Aizawa，Kenji Tei, Shinichi Honiden

“Reducing the size of two-player game for identifying guaranteeable safety property at runtime”，The 7th Asian Workshop of Advanced Software Engineering (AWASE2018)，

Gold Coast, Australia，2018.11，Kazuya Aizawa，Kenji Tei, Shinichi Honiden

“Relaxing requirements with environment changes for graceful degradation”，The 5th Asian Workshop of Advanced Software Engineering (AWASE2016)，Nara, Japan，

2016.3，Kazuya Aizawa，Kenji Tei, Shinichi Honiden, Yoshiaki Fukazawa