Detail of a work
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},
}