| 講演名 | 2017-06-20 組込みアセンブリプログラムのリアルタイム安全性の演繹的検証 山根 智(金沢大), |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 組込みシステムでは, 論理的正当性だけではなく, リアルタイム性の検証が重要である. 本論文では, 組込みプログラムのリアルタイム性の検証を目的に, 以下のような離散時間のリアルタイム性を検証する演繹的検証の手法を提案する. (1)まず, 組込みアセンブリプログラムから実行時間を付与した状態遷移モデルを構築する. (2)次に, 状態遷移モデルを対象に, RTLTL式の演繹的検証を行う. |
| 抄録(英) | It is important to verify both the correctness and real-time properties for embedded systems. In this paper, we propose deductive verification method in order to verify real-time safety properties based on discrete time as folllows: (1)First we construct a state transition system including the execution time. (2)Next we verify whether a state transition system satisfies RTLTL formulas by deductive verification. |
| キーワード(和) | 組込みアセンブリプログラム / リアルタイム性安全検証 / 演繹的検証 / リアルタイム時相論理 |
| キーワード(英) | embedded assembly program / verifying real-time safety properties / deductive verification / real-time temporal logic |
| 資料番号 | CAS2017-12,VLD2017-15,SIP2017-36,MSS2017-12 |
| 発行日 | 2017-06-12 (CAS, VLD, SIP, MSS) |
| 研究会情報 | |
| 研究会 | SIP / CAS / MSS / VLD |
|---|---|
| 開催期間 | 2017/6/19(から2日開催) |
| 開催地（和） | 新潟大学五十嵐キャンパス 中央図書館ライブラリーホール |
| 開催地（英） | Niigata University, Ikarashi Campus |
| テーマ（和） | システムと信号処理および一般 |
| テーマ（英） | |
| 委員長氏名（和） | 奥田 正浩(北九州市大) / 平木 充(ルネサス エレクトロニクス) / 名嘉村 盛和(琉球大) / 越智 裕之(立命館大) |
| 委員長氏名（英） | Masahiro Okuda(Univ. of Kitakyushu) / Mitsuru Hiraki(Renesas) / Morikazu Nakamura(Univ. of Ryukyus) / Hiroyuki Ochi(Ritsumeikan Univ.) |
| 副委員長氏名（和） | 村松 正吾(新潟大) / 相川 直幸(東京理科大) / 岡崎 秀晃(湘南工科大) / 髙井 重昌(阪大) / 峯岸 孝行(三菱電機) |
| 副委員長氏名（英） | Shogo Muramatsu(Niigata Univ.) / Naoyuki Aikawa(TUS) / Hideaki Okazaki(Shonan Inst. of Tech.) / Shigemasa Takai(Osaka Univ.) / Noriyuki Minegishi(Mitsubishi Electric) |
| 幹事氏名（和） | 宮田 高道(千葉工大) / 渡邊 修(拓殖大) / 山口 基(ルネサスシステムデザイン) / 橘 俊宏(湘南工科大) / 豊嶋 伊知郎(東芝) / 金澤 尚史(阪大) / 永山 忍(広島市大) / 宮崎 昭彦(NTT) |
| 幹事氏名（英） | Takamichi Miyata(Chiba Inst. of Tech.) / Osamu Watanabe(Takushoku Univ.) / Motoi Yamaguchi(Renesas) / Toshihiro Tachibana(Shonan Inst. of Tech.) / Ichiro Toyoshima(Toshiba) / Takahumi Kanazawa(Osaka Univ.) / Shinobu Nagayama(Hiroshima City Univ.) / Akihiko Miyazaki(NTT) |
| 幹事補佐氏名（和） | 中本 昌由(広島大) / 中村 洋平(日立) / 金城 秀樹(沖縄大) |
| 幹事補佐氏名（英） | Masayoshi Nakamoto(Hiroshima Univ.ひろ) / Yohei Nakamura(Hitachi) / Hideki Kinjo(Okinawa Univ.) |
| 講演論文情報詳細 | |
| 申込み研究会 | Technical Committee on Signal Processing / Technical Committee on Circuits and Systems / Technical Committee on Mathematical Systems Science and its applications / Technical Committee on VLSI Design Technologies |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 組込みアセンブリプログラムのリアルタイム安全性の演繹的検証 |
| サブタイトル（和） | □≦TIME q = □(q∧(time≦TIME)) |
| タイトル（英） | Deductive Verification Method of real-time safety properties for embedded assembly program |
| サブタイトル（和） | □≦TIME q = □(q∧(time≦TIME)) |
| キーワード(1)（和/英） | 組込みアセンブリプログラム / embedded assembly program |
| キーワード(2)（和/英） | リアルタイム性安全検証 / verifying real-time safety properties |
| キーワード(3)（和/英） | 演繹的検証 / deductive verification |
| キーワード(4)（和/英） | リアルタイム時相論理 / real-time temporal logic |
| 第 1 著者 氏名（和/英） | 山根 智 / Satoshi Yamane |
| 第 1 著者 所属（和/英） | 金沢大学(略称：金沢大) Kanazawa University(略称：Kanazawa Univ.) |
| 発表年月日 | 2017-06-20 |
| 資料番号 | CAS2017-12,VLD2017-15,SIP2017-36,MSS2017-12 |
| 巻番号（vol） | vol.117 |
| 号番号（no） | CAS-96,VLD-97,SIP-98,MSS-99 |
| ページ範囲 | pp.59-64(CAS), pp.59-64(VLD), pp.59-64(SIP), pp.59-64(MSS), |
| ページ数 | 6 |
| 発行日 | 2017-06-12 (CAS, VLD, SIP, MSS) |