Specification and Verification of Dynamically Reconfigurable Systems Using Dynamic Linear Hybrid Automata  

作　　者：Ryo Yanase Tatsunori Sakai Makoto Sakai Satoshi Yamane 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)

机构地区：[1]Graduate School of Natural Science & Technology, Kanazawa University, Kanazawa, Japan [2]Institute of Science and Engineering, Kanazawa University, Kanazawa, Japan

出　　处：《Journal of Software Engineering and Applications》2016年第9期452-478,共27页软件工程与应用（英文）

摘　　要：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.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 

分 类 号：TP3[自动化与计算机技术—计算机科学与技术]