Using Model-Checking Techniques for Component-Based Systems with Reconfigurations
This work addresses verification challenges for systems with dynamic reconfigurations, but it appears incremental as it applies existing model-checking techniques to a specific subclass of paths.
The paper tackled the problem of verifying architectural, event, and temporal properties in component-based systems with dynamic reconfigurations by modeling reconfiguration paths as finite state automata, enabling the use of model-checking techniques and proving the method's correctness.
Within a component-based approach allowing dynamic reconfigurations, sequences of successive reconfiguration operations are expressed by means of reconfiguration paths, possibly infinite. We show that a subclass of such paths can be modelled by finite state automata. This feature allows us to use techniques related to model-checking to prove some architectural, event, and temporal properties related to dynamic reconfiguration. Our method is proved correct w.r.t. these properties' definition.