ABSTRACT
This chapter introduces the techniques of modeling and verification of the enactment part of self-adaptation, dynamic evolution, so as to assure the adaptation is consistent with the specification. The dynamic evolution is a crucial intermediate enactment phase of the adaptation cycle. For the adaptation to be trusted, it is necessary to keep the dynamic evolution process consistent with the specification. Hierarchical architecture styles are common in the service oriented system. The chapter presents several kinds of evolution scenarios and proposes a novel verification approach based on hierarchical timed automata (HTA) to model check the underlying consistency with the specification. It presents a flattening algorithm to facilitate automated verification using the mainstream timed automata based model checker – UPPAAL. Timed automata are an extension of finite state automata to model real-time systems. HTA introduce a refinement function to describe the hierarchy relationship between states.
