| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2024-03-07 13:30 Nested Timed Automataに対するZoneに基づく到達可能性解析 ○城 聖一郎（名大）・小川瑞史（北陸先端大）・結縁祥治（名大）  SS2023-53 |
|
| 抄録 | （和） | 本稿では時間オートマトンをスタックアルファベットとするプッシュダウンオートマトンであるNested Timed Automata（NeTA）に対してZoneに基づく到達可能性解析手法を示す． NeTAはサブルーチンや割り込みハンドラなどの入れ子機構を持つ実時間ソフトウェアの振舞いをモデル化する． プッシュ動作によってスタックトップに新たな時間オートマトンを生成して振舞いを切り替え，ポップ動作によってプッシュ前の時間オートマトンの振舞いに戻る． スタックトップ以外の時間オートマトンではクロックのみが増加する． NeTAは各時間オートマトンに局所的なクロックとすべての時間オートマトンに共通な大域クロックを持つ． Liらによってクロックの差分制約をガードに持たないNeTAのRegionに基づく制御状態（Location）の到達可能性解析が決定可能であることが示されている． 本稿では，クロックの差分制約を含むガードを持つNeTAに対してZoneに基づく制御状態の到達可能性解析手法を示す． 本稿の手法がNeTAの振舞いに対して完全かつ健全であることを示し，NeTAにおける制御状態の到達可能性に対するセミアルゴリズムを与えることを示す． |
| （英） | We present a zone-based reachability analysis for Nested Timed Automata (NeTA). NeTA is a timed pushdown automaton that uses timed automata as its stack alphabet. NeTA is used to model behavioral switches in real-time programs such as interrupt handlers and subroutine calls with local clocks. A fresh timed automaton is created on top of the stack whenever a push operation is performed, starting with the initial location. It behaves like the timed automaton until the corresponding pop operation is executed. When the pop operation is executed, the timed automaton on the stack-top is deleted, and the timed automaton most recently pushed in the stack is resumed. The clocks of the automata in the stack all proceed without any reset or guard testing. Each timed automaton has a set of local and global clocks, where local clocks are reset at the push operation, and the timed automata on the stack-top share global clocks. The stack-top timed automaton uses the global and local clocks for testing guards and resets them. Li et.al showed that the location reachability of a diagonal-free NeTA is decidable using the region-based analysis. We develop a Zone-based analysis of location reachability for NeTA with diagonal constraints. Our analysis has been shown to be sound and complete for the behavior of NeTA to give a semi-algorithm of location reachability. |
|
| キーワード | （和） | 時間プッシュダウンオートマトン / 制御状態到達可能性 / ゾーン解析 / / / / / |
| （英） | timed push-down automata / location reachability / zone-based analysis / / / / / | |
| 文献情報 | 信学技報, vol. 123, no. 414, SS2023-53, pp. 25-30, 2024年3月. | |
| 資料番号 | SS2023-53 | |
| 発行日 | 2024-02-29 (SS) | |
| ISSN | Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | SS2023-53 |
|
| 研究会情報 | |
| 研究会 | SS |
| 開催期間 | 2024-03-07 - 2024-03-09 |
| 開催地（和） | 石垣市健康福祉センター（沖縄） |
| 開催地（英） | |
| テーマ（和） | ソフトウェアサイエンスおよび一般 |
| テーマ（英） | |
| 講演論文情報の詳細 | |
| 申込み研究会 | SS |
| 会議コード | 2024-03-SS |
| 本文の言語 | 日本語 |
| タイトル（和） | Nested Timed Automataに対するZoneに基づく到達可能性解析 |
| サブタイトル（和） | |
| タイトル（英） | Zone-Based Reachability Analysis of Nested Timed Automata |
| サブタイトル（英） | |
| キーワード(1)（和/英） | 時間プッシュダウンオートマトン / timed push-down automata |
| キーワード(2)（和/英） | 制御状態到達可能性 / location reachability |
| キーワード(3)（和/英） | ゾーン解析 / zone-based analysis |
| キーワード(4)（和/英） | / |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 城 聖一郎 / Seiichiro Tachi / タチ セイイチロウ |
| 第1著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ) |
| 第2著者 氏名（和/英/ヨミ） | 小川 瑞史 / Mizuhito Ogawa / オガワ ミズヒト |
| 第2著者 所属（和/英） | 北陸先端科学技術大学院大学 (略称： 北陸先端大) Japan Advanced Institute of Science and Technology (略称： JAIST) |
| 第3著者 氏名（和/英/ヨミ） | 結縁 祥治 / Shoji Yuen / ユウエン ショウジ |
| 第3著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ) |
| 講演者 | 第1著者 |
| 発表日時 | 2024-03-07 13:30:00 |
| 発表時間 | 25分 |
| 申込先研究会 | SS |
| 資料番号 | SS2023-53 |
| 巻番号（vol） | vol.123 |
| 号番号（no） | no.414 |
| ページ範囲 | pp.25-30 |
| ページ数 | 6 |
| 発行日 | 2024-02-29 (SS) |
[研究会発表申込システムのトップページに戻る]