| Item type |
SIG Technical Reports(1) |
| 公開日 |
2022-07-21 |
| タイトル |
|
|
タイトル |
充足可能性判定を利用した実現可能な時間オートマトンの検証 |
| タイトル |
|
|
言語 |
en |
|
タイトル |
Verification of implementable Timed Automata via satisfiability checking |
| 言語 |
|
|
言語 |
jpn |
| 資源タイプ |
|
|
資源タイプ識別子 |
http://purl.org/coar/resource_type/c_18gh |
|
資源タイプ |
technical report |
| 著者所属 |
|
|
|
名古屋大学情報学研究科 |
| 著者所属 |
|
|
|
名古屋大学情報学研究科 |
| 著者所属(英) |
|
|
|
en |
|
|
Graduate School of Informatics, Nagoya University |
| 著者所属(英) |
|
|
|
en |
|
|
Graduate School of Informatics, Nagoya University |
| 著者名 |
城, 聖一郎
結縁, 祥治
|
| 著者名(英) |
Seiichiro, Tachi
Shoji, Yuen
|
| 論文抄録 |
|
|
内容記述タイプ |
Other |
|
内容記述 |
クロックのずれやサンプリングを考慮した実現可能な時間オートマトンの到達可能性検証の手法として，SMT ソルバを用いた有界検証手法を示す．有界検証のために，Uppaal を用いて記述した時間オートマトンを入力として制約式を生成する変換器を作成し，実現可能な時間オートマトンに対して制約式を構築する．生成した制約式を SMT ソルバ Z3 を用いて解を求め，制約式の生成方法と解を得るための計算コストに対する評価を行った． |
| 論文抄録(英) |
|
|
内容記述タイプ |
Other |
|
内容記述 |
We present a technique for bounded model-checking the reachability in timed automata with implementability assuming that uncertain drifts and digital sampling of clocks exist. Then, we develop a method to automatically generate a clock constraint formula of timed automata from the XML description in Uppaal and convert the formula with the implementable features. Finally, we use Z3, a well-known SMT solver, to find the existence of the clock valuation sequence to reach a specified location and evaluate the computation cost to check the reachability property for three encodings of timed automata behaviour. |
| 書誌レコードID |
|
|
収録物識別子タイプ |
NCID |
|
収録物識別子 |
AN10112981 |
| 書誌情報 |
研究報告ソフトウェア工学（SE）
巻 2022-SE-211,
号 17,
p. 1-6,
発行日 2022-07-21
|
| ISSN |
|
|
収録物識別子タイプ |
ISSN |
|
収録物識別子 |
2188-8825 |
| Notice |
|
|
|
SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. |
| 出版者 |
|
|
言語 |
ja |
|
出版者 |
情報処理学会 |
IPSJ-SE22211017.pdf (993.1 kB)
