Development of model checker of dynamic linear hybrid automata

• Yanase, Ryo

• Sakai, Tatsunori

• Sakai, Makoto

• Yamane, Satoshi

Abstract

Dynamically reconfigurable systems have attracted public attention from the point of view of miniaturization and saving power consumption for embedded systems in recent years. In this study, we propose dynamic linear hybrid automata as specification language of dynamically reconfigurable systems and the verification technique of reachability analysis. A dynamic linear hybrid automaton(DLHA) is a linear hybrid automaton extended with actions of creation and destruction. This paper presents the model checker and applies it to the model of an embedded system consisting CPU and DRP. © 2013 IEEE.

Journal

• Proceedings - International Computer Software and Applications Conference

  Proceedings - International Computer Software and Applications Conference 6649888 607-608, 2013-05-24

  IEEE

Keywords

• Dynamically reconfigurable systems
• Hybrid automata
• Model checking
• Verification

Details

• CRID: 1050282810916148352
• NII Article ID: 120005418465
• ISSN: 07303157
• Web Site: http://hdl.handle.net/2297/36977
• Text Lang: en
• Article Type: journal article
• Data Source:
  • IRDB
  • CiNii Articles