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...
Main Author: | |
---|---|
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 |