SearcharxivSearch

arXiv subjects

Jean-Michel Hufflen

Publications and source records attributed to Jean-Michel Hufflen.

2 recordsLinked to original sources

Checking Properties along Multiple Reconfiguration Paths for Component-Based Systems

Reconfiguration paths express sequences of successive reconfiguration operations within a component-based approach allowing dynamic reconfigurations. We use constructs from regular expressions-pin particular, alternatives-to introduce multiple reconfiguration paths. We show how to put into action procedures allowing architectural, event, and temporal properties to be proved. Our method, related to finite state automata and using marking techniques, generalises what we did within previous work, where the regular expressions we processed were more restricted. But we can only deal with a subset of first-order logic formulas.

cs.SE

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

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.

cs.SE