期刊名称:Journal of Software Engineering and Applications
印刷版ISSN:1945-3116
电子版ISSN:1945-3124
出版年度:2016
卷号:09
期号:09
页码:452-478
DOI:10.4236/jsea.2016.99030
语种:English
出版社:Scientific Research Publishing
摘要: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