TITLE:
Specification and Verification of Dynamically Reconfigurable Systems Using Dynamic Linear Hybrid Automata
AUTHORS:
Ryo Yanase, Tatsunori Sakai, Makoto Sakai, Satoshi Yamane
KEYWORDS:
Formal Method, Model Checking, Hybrid Automata, Embedded Systems, Dynamically Reconfigurable Systems
JOURNAL NAME:
Journal of Software Engineering and Applications,
Vol.9 No.9,
September
30,
2016
ABSTRACT: 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.