| 講演名 | 2017-03-03 キャッシュの効率利用による自己適応システムの動的モデル検査法改善 外山 大夢(阪大), 中川 博之(阪大), 小島 英春(阪大), 土屋 達弘(阪大), |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 近年，システム自身の振る舞いを変化させる自己適応システムに注目が集まっているが，振る舞い変更時に変更後の振る舞いの正しさを検証する必要があり，その効率的な検証に関して様々な研究がなされている．その一つに，設計時に検証の大部分を計算し，実行時に簡単な計算のみを行なうFilieriら手法や，キャッシュを利用し，Filieriらの手法の適用範囲を拡大を試みた小川らの手法がある．本研究では，既存手法を改善し，実行時の計算時間を削減を試みた．実験の結果，本手法は，設計時段階の計算時間とキャッシュサイズが増加するものの，実行時の計算時間を削減できることが確認できた．またこの手法は振る舞い変更の種類に依存しにくく，システムの状態数が大きいほど有用であることも確認できた． |
| 抄録(英) | Self-adaptive systems, which change their behaviors to adapt to their environmental changes, are focused on in recent years. In a self-adaptive system, the correctness of its behavior after adaptation should be verified when the system is changing its behaviors. Some studies of efficient verification for self-adaptive systems have been developed. Filieri et al. have proposed a method that calculates the most part of the verification at design time and the simple value calculation at runtime. Ogawa et al. have proposed a method that uses a cache and improved the method proposed by Filieri et al.. In this thesis, for the verification faster, We improve the existing approaches and reduce computational time at runtime. The experimental results demonstrate that the proposed approach is effective to reduce the computational time at runtime, even though the memory size for caching and computational time at design time increase. We identified that our approach does not tend to be affected on the variety of model changes and has scalability, and it is capable in a larger system. |
| キーワード(和) | モデル検査 / 離散時間マルコフ連鎖モデル / ラプラス展開 / LU 分解 / 行列式 |
| キーワード(英) | model checking / discrete time Markov chains (DTMC) / Laplace expansion / LU decomposition / determinant |
| 資料番号 | KBSE2016-40 |
| 発行日 | 2017-02-24 (KBSE) |
| 研究会情報 | |
| 研究会 | KBSE |
|---|---|
| 開催期間 | 2017/3/3(から2日開催) |
| 開催地（和） | 石川県金沢市 ITビジネスプラザ武蔵 研修室1 |
| 開催地（英） | |
| テーマ（和） | 一般 |
| テーマ（英） | |
| 委員長氏名（和） | 金田 重郎(同志社大) |
| 委員長氏名（英） | Shigeo Kaneda(Doshisha Univ.) |
| 副委員長氏名（和） | 粂野 文洋(日本工大) |
| 副委員長氏名（英） | Fumihiro Kumeno(Nippon Inst. of Tech.) |
| 幹事氏名（和） | 小形 真平(信州大) / 橋浦 弘明(日本工大) |
| 幹事氏名（英） | Shinpei Ogata(Shinshu Univ.) / Hiroaki Hashiura(Nippon Inst. of Tech.) |
| 幹事補佐氏名（和） | 岩田 一(神奈川工科大) / 櫻井 孝平(金沢大) |
| 幹事補佐氏名（英） | Hajime Iwata(Kanagawa Inst. of Tech.) / Kohei Sakurai(Kanazawa Univ.) |
| 講演論文情報詳細 | |
| 申込み研究会 | Technical Committee on Knowledge-Based Software Engineering |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | キャッシュの効率利用による自己適応システムの動的モデル検査法改善 |
| サブタイトル（和） | |
| タイトル（英） | Improvement of Efficient Runtime Model Checking for Self-adaptive Systems Using Cashe |
| サブタイトル（和） | |
| キーワード(1)（和/英） | モデル検査 / model checking |
| キーワード(2)（和/英） | 離散時間マルコフ連鎖モデル / discrete time Markov chains (DTMC) |
| キーワード(3)（和/英） | ラプラス展開 / Laplace expansion |
| キーワード(4)（和/英） | LU 分解 / LU decomposition |
| キーワード(5)（和/英） | 行列式 / determinant |
| 第 1 著者 氏名（和/英） | 外山 大夢 / Hiromu Toyama |
| 第 1 著者 所属（和/英） | 大阪大学(略称：阪大) Osaka University(略称：Osaka Univ) |
| 第 2 著者 氏名（和/英） | 中川 博之 / Hiroyuki Nakagawa |
| 第 2 著者 所属（和/英） | 大阪大学(略称：阪大) Osaka University(略称：Osaka Univ) |
| 第 3 著者 氏名（和/英） | 小島 英春 / Hideharu Kojima |
| 第 3 著者 所属（和/英） | 大阪大学(略称：阪大) Osaka University(略称：Osaka Univ) |
| 第 4 著者 氏名（和/英） | 土屋 達弘 / Tatsuhiro Tsuchiya |
| 第 4 著者 所属（和/英） | 大阪大学(略称：阪大) Osaka University(略称：Osaka Univ) |
| 発表年月日 | 2017-03-03 |
| 資料番号 | KBSE2016-40 |
| 巻番号（vol） | vol.116 |
| 号番号（no） | KBSE-493 |
| ページ範囲 | pp.7-12(KBSE), |
| ページ数 | 6 |
| 発行日 | 2017-02-24 (KBSE) |