A Case Study of Formal Approach to Dynamically Reconfigurable Systems by Using Dynamic Linear Hybrid Automata

Networking systems and embedded systems are able to change their configuration, components and modules at run-time. Such a system is called dynamically reconfigurable system. For guaranteeing safety of the system, model checking is one of the effective methods. This paper presents a dynamic linear hybrid automaton (DLHA) as a specification language for designing dynamically reconfigurable systems. As a practical experiment, we describe an embedded cooperative system consisting of CPU and DRP by DLHAs and verify several properties for the system with a model checker that performs the reachability analysis by using monitor automata.