Using Model-Checking Techniques for Component-Based Systems with Reconfigurations

TL;DR

This paper introduces a model-checking approach for component-based systems with dynamic reconfigurations, using finite automata to verify properties of reconfiguration paths, including infinite sequences.

Contribution

It presents a novel method to model certain reconfiguration paths with finite automata, enabling formal verification of dynamic reconfiguration properties.

Findings

Finite automata can model a subclass of reconfiguration paths.

Model-checking techniques verify architectural, event, and temporal properties.

The method is proven correct for the specified properties.

Abstract

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.