Author(s)

Ryo Yanase¹, Tatsunori Sakai¹, Makoto Sakai¹, Satoshi Yamane²

¹Graduate School of Natural Science & Technology, Kanazawa University, Kanazawa, Japan.
²Institute of Science and Engineering, Kanazawa University, Kanazawa, Japan.

A dynamically reconfigurable system can change its configuration during operation, and studies of such systems are being carried out in many fields. In particular, medical technology and aerospace engineering must ensure system safety because any defect will have serious consequences. Model checking is a method for verifying system safety. In this paper, we propose the Dynamic Linear Hybrid Automaton (DLHA) specification language and show a method to analyze reachability for a system consisting of several DLHAs.

Formal Method, Model Checking, Hybrid Automata, Embedded Systems, Dynamically Reconfigurable Systems

Yanase, R. , Sakai, T. , Sakai, M. and Yamane, S. (2016) Specification and Verification of Dynamically Reconfigurable Systems Using Dynamic Linear Hybrid Automata. Journal of Software Engineering and Applications, 9, 452-478. doi: 10.4236/jsea.2016.99030.