Reconfigurable Hierarchical Timed Automata: Modeling and Stochastic Verification
Roufaida Bettira, Laïd Kahloul, Mohamed Salah Khalgui, Zhiwu Li · 2019
This paper deals with formal modeling and verification of reconfigurable hierarchical discrete-event control systems (RDECSs). The system's behavior is with a dynamic structure for being adapted to related environment. We propose an extension of timed automata named reconfigurable hierarchical timed automata (RHTA) to consider hierarchy and reconfigurability of the considered system. Since the verification becomes an expensive task in terms of computation time and memory, an improved verification methodology is proposed for RHTA where redundancies and similarities between system's configurations are considered which controls verification cost. The proposed contribution is applied to an example to evaluate the related performance where gains in term of verification time are marked.