WEKO3
インデックスリンク
アイテム
Abstraction refinement for non-zeno fairness verification of linear hybrid automata
https://doi.org/10.24517/00050514
https://doi.org/10.24517/00050514bfd30c9d-40a3-4f12-ac0b-62593d30072e
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
TE-PR-YANASE-R-567.pdf (60.0 kB)
|
.png)
|
| Item type | 学術雑誌論文 / Journal Article(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2018-04-16 | |||||||
| タイトル | ||||||||
| タイトル | Abstraction refinement for non-zeno fairness verification of linear hybrid automata | |||||||
| 言語 | ||||||||
| 言語 | eng | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||
| 資源タイプ | journal article | |||||||
| ID登録 | ||||||||
| ID登録 | 10.24517/00050514 | |||||||
| ID登録タイプ | JaLC | |||||||
| 著者 |
Yanase, Ryo
× Yanase, Ryo |
|||||||
| 著者別表示 |
栁瀨, 龍
× 栁瀨, 龍
|
|||||||
| 提供者所属 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 金沢大学新学術創成研究機構 | |||||||
| 書誌情報 |
Proceedings - 10th IEEE International Conference on Software Testing, Verification and Validation, ICST 2017 巻 2017-May, p. 567-568, 発行日 2017-05-15 |
|||||||
| DOI | ||||||||
| 関連タイプ | isVersionOf | |||||||
| 識別子タイプ | DOI | |||||||
| 関連識別子 | 10.1109/ICST.2017.78 | |||||||
| 出版者 | ||||||||
| 出版者 | Institute of Electrical and Electronics Engineers Inc. | |||||||
| 抄録 | ||||||||
| 内容記述タイプ | Abstract | |||||||
| 内容記述 | Linear hybrid automaton is a specification language for hybrid systems. For verification of hybrid systems, it is important to check fairness assumptions. For example, an embedded system keeps running forever when it starts to move by turning on the switch. Such a system has to be checked not only system safety but also fairness and non-Zenoness. The state space explosion is a fundamental problem in model checking, since it is a method that performs an exhaustive search of states. To avoid state space explosion problem in model checking, CEGAR (Counter Example Guided Abstraction Re?nement) is an effective technique. In this paper, we propose transition predicate abstraction and CEGAR verification algorithm for linear hybrid automata. © 2017 IEEE. | |||||||
| 権利 | ||||||||
| 権利情報 | Copyright © 2017 IEEE. | |||||||
| 著者版フラグ | ||||||||
| 出版タイプ | AM | |||||||
| 出版タイプResource | http://purl.org/coar/version/c_ab4af688f83e57aa | |||||||
| 関連URI | ||||||||
| 識別子タイプ | URI | |||||||
| 関連識別子 | http://aster.or.jp/conference/icst2017/ | |||||||
| 関連名称 | http://aster.or.jp/conference/icst2017/ | |||||||
| 関連URI | ||||||||
| 識別子タイプ | URI | |||||||
| 関連識別子 | https://www.ieee.org/ | |||||||
| 関連名称 | https://www.ieee.org/ | |||||||
