English

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

Software Engineering 2015-03-18 v1 Data Structures and Algorithms Formal Languages and Automata Theory

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.

Keywords

Cite

@article{arxiv.1503.04915,
  title  = {Using Model-Checking Techniques for Component-Based Systems with Reconfigurations},
  author = {Jean-Michel Hufflen},
  journal= {arXiv preprint arXiv:1503.04915},
  year   = {2015}
}

Comments

In Proceedings FESCA 2015, arXiv:1503.04378

R2 v1 2026-06-22T08:54:50.529Z