| Tweet | |
| Kozo Okano, Toshifusa Sekizawa, Hiroaki Shimba, Hideki Kawai, Kentaro Hanada, Yukihiro Sasaki, and S. Kusumoto, "Verification of Safety Property of Line Tracer Program Using Timed Automaton Model," International Workshop on Informatics 2012, pp. 136-142, September 2012. | |
| ID | 230 |
| 分類 | 国際会議 |
| タグ | automaton line model program property safety timed tracer verification |
| 表題 (title) |
Verification of Safety Property of Line Tracer Program Using Timed Automaton Model |
| 表題 (英文) |
|
| 著者名 (author) |
Kozo Okano, Toshifusa Sekizawa, Hiroaki Shimba, Hideki Kawai, Kentaro Hanada, Yukihiro Sasaki, and Shinji Kusumoto |
| 英文著者名 (author) |
|
| キー (key) |
|
| 定期刊行物名 (journal) |
International Workshop on Informatics 2012 |
| 定期刊行物名 (英文) |
|
| 巻数 (volume) |
|
| 号数 (number) |
|
| ページ範囲 (pages) |
136-142 |
| 刊行月 (month) |
9 |
| 出版年 (year) |
2012 |
| Impact Factor (JCR) |
|
| URL |
|
| 付加情報 (note) |
|
| 注釈 (annote) |
|
| 内容梗概 (abstract) |
Recently reliability of embedded systems has become very important. Such reliability can be ensured by formal verification techniques including model checking. We study such verification technique through a real example of embedded systems, a line tracer. This paper mainly describes how to model the behavior of the line tracer in a network of timed automata, as well as experimental results of verification. Using the model, several safety properties are successfully verified with a model checker, UPPAAL. The line tracer is built with LEGO Mindstorms kit. This paper also describes the implementation using LeJOS, a Java development environment for LEGO Mindstorms kit. |
| 論文電子ファイル | iwin2012.pdf (application/pdf) [一般閲覧可] |
| BiBTeXエントリ |
@article{id230,
title = {Verification of Safety Property of Line Tracer Program using Timed Automaton Model},
author = {Kozo Okano, Toshifusa Sekizawa, Hiroaki Shimba, Hideki Kawai, Kentaro Hanada, Yukihiro Sasaki, and Shinji Kusumoto},
journal = {International Workshop on Informatics 2012},
pages = {136-142},
month = {9},
year = {2012},
}
|