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 te...

Full description

Bibliographic Details
Main Author: Jean-Michel Hufflen
Format: Article
Language:English
Published: Open Publishing Association 2015-03-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1503.04915v1
id doaj-fa0525c783924180bf61e97a7e480f80
record_format Article
spelling doaj-fa0525c783924180bf61e97a7e480f802020-11-24T23:21:38ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802015-03-01178Proc. FESCA 2015334610.4204/EPTCS.178.4:11Using Model-Checking Techniques for Component-Based Systems with ReconfigurationsJean-Michel Hufflen0 FEMTO-ST & University of Franche-Comté 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.http://arxiv.org/pdf/1503.04915v1
collection DOAJ
language English
format Article
sources DOAJ
author Jean-Michel Hufflen
spellingShingle Jean-Michel Hufflen
Using Model-Checking Techniques for Component-Based Systems with Reconfigurations
Electronic Proceedings in Theoretical Computer Science
author_facet Jean-Michel Hufflen
author_sort Jean-Michel Hufflen
title Using Model-Checking Techniques for Component-Based Systems with Reconfigurations
title_short Using Model-Checking Techniques for Component-Based Systems with Reconfigurations
title_full Using Model-Checking Techniques for Component-Based Systems with Reconfigurations
title_fullStr Using Model-Checking Techniques for Component-Based Systems with Reconfigurations
title_full_unstemmed Using Model-Checking Techniques for Component-Based Systems with Reconfigurations
title_sort using model-checking techniques for component-based systems with reconfigurations
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2015-03-01
description 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.
url http://arxiv.org/pdf/1503.04915v1
work_keys_str_mv AT jeanmichelhufflen usingmodelcheckingtechniquesforcomponentbasedsystemswithreconfigurations
_version_ 1725570967008182272