Checking Properties along Multiple Reconfiguration Paths for Component-Based Systems

TL;DR

This paper presents a method for verifying properties along multiple reconfiguration paths in component-based systems using regular expressions and automata techniques, extending previous work to handle more complex reconfiguration sequences.

Contribution

It introduces a generalized approach for checking architectural, event, and temporal properties along multiple reconfiguration paths using regular expressions and automata, handling more complex sequences.

Findings

Method can verify properties along multiple reconfiguration paths

Uses automata and marking techniques for property verification

Extends previous work to handle more complex reconfiguration sequences

Abstract

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.

Equations

$$B\ni ({\text{cache}}_{\text{CacheHandler}},{\text{getCache}}_{\text{RequestHandler}})$$

$$⟨temp⟩$$

$$⟨trace⟩$$

$$⟨event⟩$$

$$q\mapsto q^{\prime }$$

$$q<q^{\prime }$$

$$\forall q_j:q_0\le q_j<q_i,\text{mark-for-always}(q_j)=\mathtt{checked}\vee \text{mark-for-always}(q_j)=\mathtt{again}$$

$$\forall q_j:q_0^{\prime }\le q_j\nless q_0^{\prime },\text{mark-for-always}(q_j)=\mathtt{checked}$$

Full text

Keywords  Component-based approach, dynamic reconfiguration paths, multiple reconfiguration paths, checking invariance properties, finite state automata, marking techniques.

1 Introduction

Dynamic reconfigurations of software architectures are active research topics [2, 4, 6, 20, 21, 22, 19, 26]. They provide large increase in value for component-based software. Such an approach allows some components to be replaced or removed, in particular if they fail. In order to provide more services, more components may be added dynamically, too. So dynamic reconfigurations increase the availability and reliability of such systems by allowing their architecture to evolve at run-time.

The work presented hereafter is an extension of [15], which addresses the verification of architectural, event, or temporal properties. Such properties may be crucial for systems with high-safety requirements. About the definition of such properties, [10] proposes ftpl111Fractal Temporal Pattern Logic., a temporal logic for dynamic reconfigurations applied to components defined by means of the Fractal toolbox [5] and including such properties. ftpl allows successive reconfigurations—modelled by reconfiguration paths—to be applied to successive configurations (or component models). Since ftpl is based on first-order predicate logic, such properties are undecidable in general, there only exist partial solutions for proving them.

Many authors developed methods that work whilst software is running and may be reconfigured—e.g., [18, 19], based on ftpl, or [13] as another example. Therefore we know if a property holds for the successive members of a chain of reconfigurations, until the current run-time state. Our method is very different, more related to the approach of a procedure’s developer when such a developer aims to prove its procedure before deploying it and putting it into action. In fact, we do not verify such properties at run-time, but on a static abstraction of the reconfiguration model, so we aim to ensure that such a property holds before the software is deployed and working, that is, at design-time. Of course, we cannot consider reconfigurations caused by totally unexpected events but we think that our approach is complementary to such works, our goal is to go as far as possible within this static approach. In [15], we proposed a method based on this point of view and using marking techniques related to model-checking: given a reconfiguration path that may be applied when the software is running, we aimed to ensure that a property holds if this path is actually applied when the software works. We were able to deal with some cases of infinite reconfiguration paths, but we only processed one possible reconfiguration path. Dealing with only one path is not restrictive for methods applied at run-time, whilst the software is working, but is rather limited at design-time, where several possible futures could be studied. In the present article, we propose the new notion of multiple reconfiguration paths, which are expressions denoting several possible reconfiguration processes. However, this extension has a price: the correctness of our new implementations—w.r.t. the definitions of [10]—is guaranteed only for a strict subset of formulas, in comparison with formulas used within [15].

Section 2 gives some recalls about the component model we use, our operations of reconfiguration, and the temporal logic for dynamic reconfigurations. Of course, most definitions presented in this section come from [10, 11, 12, 18]. Section 3 precisely introduces our notion of multiple reconfiguration path and Section 4 recalls the organisation of our framework. Then we give updated versions of our programs in Section 5 and study the correctness of these implementations w.r.t. the operators defined in Section 2. We do not examine all the operators, but our examples are representative: implementation techniques and correctness proofs are analogous. Section 6 discusses some advantages and drawbacks of our method, in comparison with other approaches. It also introduces future work. In order for this article to be self-contained, most of the definitions put hereafter are identical to [15]’s. Readers familiar with that article can skip Section 2—except for the definition of the $\mathit{CP}^{\flat}$ set—and § 4.1.

2 Architectural Reconfiguration Model

First we recall how our component model is organised. Then we sum up the operations used for reconfiguring an architecture. Last, we make precise operators used in ftpl, the temporal logic used in [10, 11, 12, 18] for dynamic reconfigurations.

2.1 Component Model

Roughly speaking, a component model describes an architecture of components. Some simpler components may be subcomponents of a composite one, and components may be linked. Let $\mathcal{S}$ be a set of type names 222… or class names within an object-oriented approach., a component $\mathcal{C}$ is defined by:

• •

three pairwise-disjoint sets of parameters333Some authors use the term ‘attributes’ instead. A parameter is related to an internal feature, e.g., the maximum number of messages a component can process. $P_{\mathcal{C}}$, input port names $I_{\mathcal{C}}$, and output port names $O_{\mathcal{C}}$;

• •

the class $t_{\mathcal{C}}$ encompassing the services implemented by the component;

• •

additional functions to get access to the class of a parameter or port ($\tau_{C}:P_{\mathcal{C}}\cup I_{\mathcal{C}}\cup O_{\mathcal{C}}\rightarrow\mathcal{S}$), or to a parameter’s value ($v_{\mathcal{C}}:P_{\mathcal{C}}\rightarrow\bigcup_{s\in\mathcal{S}}s$);

• •

the set $\mathit{sub\text{-}c}_{\mathcal{C}}$ of its subcomponents if the $\mathcal{C}$ component is composite444Of course, the binary relation ‘is a subcomponent of’ must be a direct acyclic graph. A composite component cannot have parameters. More precisely, it implicitly has the parameters of all its sub-components.;

• •

the set $B$ of bindings of ports—that is, couples of input and input port names, being the same type, and the set $D$ of delegation links, between composite component ports and port of contained components.

Possible components of an http server are given in Fig. 1, as an example of a component-based architecture, already used in [7]. Requests are read by the RequestReceiver component and transmitted to the RequestHandler component. When the latter processes a request, it may consult the cache by means of the CacheHandler component or transmit this request to the RequestDispatcher component, which manages file servers. This architecture is based on a cache and load balancer, in order for response times to be as short as possible. The cache must be used only if the number of similar requests is very high, and the amount of memory devoted to the cache component must be automatically adjusted to the Web server’s load. The validity duration of the data put in the cache must also be adjusted with respect to the Web server’s load. In addition, more data servers have to be deployed if the servers’ average load is high. According to these conventions, we see that some components may be added or removed, depending on some parameters.

2.2 Configuration Properties

Example 1

Looking at Fig. 1’s architecture, we can notice that the CacheHandler component is connected to the RequestHandler component through their respective ports cache and getCache. We can express this configuration property—so-called CacheConnected—as follows:

[TABLE]

In fact, such properties—that may be viewed as constraints—are specified using first-order logic formulas over constants (‘true’, ‘false’), variables, sets and functions defined in § 2.1, predicates ($=,\in,\ldots$), connectors ($\wedge,\vee,\ldots)$ and quantifiers ($\forall,\exists$). These configuration properties form a set denoted by $\mathit{CP}$. The subset $\mathit{CP}^{\flat}$ is build analogously, but connectors and quantifiers are restricted to $\wedge$ and $\forall$. Roughly speaking, formulas belonging to $\mathit{CP}^{\flat}$ are comparable to premises of Horn clauses within logic programming.

2.3 Reconfiguration Operations

Primitive reconfiguration operations apply to a component architecture, and the output is a component architecture, too555They may be viewed as graph transformations applied to component models if we consider such models as graphs.. They are the addition or removal of a component, the addition or removal of a binding, the update of a parameter’s value. Let us notice that the result of such an operation is consistent from a point of view related to software architecture: for example, a component is stopped before it is removed, and removing it causes all of its bindings to be removed, too. These operations are robust in the sense that they behave like the identity function if the corresponding operation cannot be performed. For example, if you try to remove a component not included in an architecture, the original architecture will be returned. The same if you try to add a component already included in the architecture666The reason: the name of a component—part of its definition—can only identify one component. But you can clone a component under a new name.. As a consequence, these topological operations—addition or removal of a component or a binding—are idempotent: applying such an operation twice results in the same effect than applying it once. General reconfiguration operations on an architecture are combinations of primitive ones, and form a set denoted by $\mathcal{R}$. The set of evolution operations is $\mathcal{R}_{\mathit{run}}=\mathcal{R}\cup\{\mathit{run}\}$ where $\mathit{run}$ is an action modelling that all the stopped components are restarted and the software is running777Strictly speaking, we have to stop a component before removing it, and to start it before having added it, as abovementioned. This convention about the $\mathit{run}$ action allows us not to be worried about such stop and start operations within our reconfiguration paths..

Definition 2** ([11, 18])**

The operational semantics of component systems with reconfigurations is defined by the labelled transition system $\mathcal{S}=\langle\mathit{C,C^{0},\mathcal{R}_{\mathit{run}},\rightarrow,l}\rangle$ where $C=\{c,c_{1},c_{2},\ldots\}$ is a set of configurations—or component models—$C^{0}\subseteq C$ is a set of initial configurations, $\mathcal{R}_{\mathit{run}}$ is a finite set of evolution operations, $\rightarrow\;\subseteq C\times\mathcal{R}_{\mathit{run}}\times C$ is the reconfiguration relation, and $l:C\rightarrow\mathit{CP}$ is a total function to label each $c\in C$ with the largest conjunction of $\mathit{cp}\in\mathit{CP}$ evaluated to ‘true’ over $\mathcal{R}_{\mathit{run}}$.

Let us note $c\stackrel{{\scriptstyle\mathit{op}}}{{\rightarrow}}c^{\prime}$ when a target configuration $c^{\prime}$ is reached from a configuration $c$ by an evolution $\mathit{op}\in\mathcal{R}_{\mathit{run}}$. Given the model $S=\langle\mathit{C,C^{0},\mathcal{R}_{\mathit{run}},\rightarrow,l}\rangle$, an evolution path $\sigma$ of $S$ is a (possibly infinite) sequence of component models $c_{0},c_{1},c_{2},\ldots$ such that $\forall i\in\mathbb{N},\exists\mathit{op}\in\mathcal{R}_{\mathit{run}},c_{i}\stackrel{{\scriptstyle\mathit{op}}}{{\rightarrow}}c_{i+1}\in\;\rightarrow$. We write ‘$\sigma[i]$’ to denote the $i$th element of a path $\sigma$, if this element exists. The notation ‘$\sigma_{i}^{\uparrow}$’ denotes the suffix path $\sigma[i],\sigma[i+1],\ldots$ and ‘$\sigma_{i}^{j}$’ ($j\in\mathbb{N}$) denotes the segment path $\sigma[i],\sigma[i+1],\ldots,\sigma[j-1],\sigma[j]$. An example of evolution path allowing Fig. 1 to be reached from a simpler architecture is given in Fig. 2 (Fig. 1’s architecture is labelled by the $c_{4}$ configuration).

2.4 Temporal Logic

ftpl deals with events from reconfiguration operations, trace properties, and temporal properties, respectively denoted by ‘$\mathit{event}$’, ‘$\mathit{trace}$’, and ‘$\mathit{temp}$’ in the following. Hereafter we only give some operators of ftpl, in particular those used in the implementations we describe. For more details about this temporal logic, see [11, 18]. ftpl’s syntax is defined by:

[TABLE]

where ‘$\mathit{cp}$’ is a configuration property and ‘$\mathit{op}$’ a reconfiguration operation. Let $\mathit{cp}$ in $\mathit{CP}$ be a configuration property and $c$ a configuration, $c$ satisfies $\mathit{cp}$, written ‘$c\models\mathit{cp}$’ when $l(c)\Rightarrow\mathit{cp}$. Otherwise, we write ‘$c\not\models\mathit{cp}$’ when $c$ does not satisfy $\mathit{cp}$.

Definition 3** ([11])**

Let $\sigma$ be an evolution path, the ftpl semantics is defined by induction on the form of the formulas as follows888For a complete definition including all the operators, see [11].—in the following, $i\in\mathbb{N}$—:

• •

for the events:

[TABLE]

• •

for the trace properties:

[TABLE]

• •

for the temporal properties:

[TABLE]

Example 4

If we consider the evolution path of Fig. 2 again, we can now express that after calling the AddCacheHandler reconfiguration operation, the CacheHandler component is always connected to the RequestHandler component—CacheConnected is the configuration property defined in Example 1—:

**after AddCacheHandler normal always CacheConnected

Remark 5

About temporal and trace properties, let us notice that if such a property holds on an evolution path, it holds on any prefix of this path.

3 Multiple Reconfiguration Paths

Definition 6

Let $\mathcal{R}_{\mathit{run}}$ be a set of evolution operations, a reconfiguration path is a sequence of elements of $\mathcal{R}_{\mathit{run}}$, and the set $\Omega_{\mathcal{R}_{\mathit{run}}}$ of multiple reconfiguration paths on $\mathcal{R}_{\mathit{run}}$ is the set of regular expressions built over the alphabet $\mathcal{R}_{\mathit{run}}$. Let us recall that the constructs used within regular expressions are ‘|’ for alternatives, ‘?’ for an optional occurrence of an alphabet’s member, ‘**’ (resp. ‘+’) for zero (resp. one) or more occurrences of such a member. Semantically, a multiple reconfiguration path is the set of all the prefixes of all the reconfiguration paths denoted by this regular expression.*

Example 7

*The following multiple reconfiguration path: *

[TABLE]

includes the chain of reconfigurations pictured at Fig. 2.

Remark 8

Let us recall that a reconfiguration path may be infinite. Looking at Ex. 7, we consider that the ‘(…)+’ expression can be iterated a finite number of times, followed by the AddFileServer operation; another possible behaviour is an endless iteration of the ‘(…)+’ expression. We encompass all these possible behaviours by considering prefixes, as mentioned in Def. 6.

It is well-known for many years—since Kleene’s theorem—that a regular expression language can be recognised by a deterministic finite state automaton, whose transitions are labelled by members of this language’s alphabet. Let us recall that such an automaton $\mathcal{A}$ is defined by a set $Q$ of states, a set $L$ of transition labels, and a set $T\subseteq Q\times L\times Q$ of transitions. As in Def. 3 for systems with reconfigurations, there exists a function $l:Q\rightarrow\mathit{CP}$, which labels each $q$ state with the largest conjunction of $\mathit{cp}\in\mathit{CP}$ evaluated to ‘true’ for the $q$ state. As an example, Ex. 7’s language can be recognised by the automaton pictured in Fig. 3 (the states $q_{0},q_{1},q^{\prime}_{1},\ldots,q_{5}$ have been respectively named in connection to the successive component models $c_{0},c_{1},c^{\prime}_{1},\ldots,c_{5}$ of Fig. 2). In addition, let us recall that such an automaton can be build automatically from a regular expression. In the next section, we explain what our states are, and which operations are performed by our transitions.

4 Our Method’s Bases

4.1 Modus Operandi

As mentioned above, our framework’s basis is an automaton modelling the possible evolution paths of a multiple reconfiguration path. A state of such an automaton is a component model, initial or got by means of successive reconfiguration operations—primitive or built by chaining primitive operations—or ‘run’ operations. A transition consists of applying such an evolution operation. Such an automaton has an initial state, given by the initial component model ($q_{0}$ in Fig. 3). Since we aim to recognise all the prefixes of possible reconfiguration paths, any state may be viewed as final. In addition, since some infinite behaviours are accepted (e.g., endlessly cycling from the $q_{5}$ or $q_{6}$ state to the $q_{2}$ state in Fig. 3), there are processes without ‘actual’ final state. In fact, the complete automaton may be viewed as an $\omega$-automaton. Let us go back to states reached several times—e.g., the $q_{2}$ state in Fig. 3, reached after $q_{5}$ and $q_{6}$—: considering that the whole system is back to a previous state may be not exact, because some parameters may have been updated: this is the case in Fig. 3’s example, about the memory’s size and duration validity. As a consequence, some properties related to components’ parameters may not hold. We will go back on this point at the beginning of § 2.2.

Several programming languages are used within our framework. Fig. 4 shows how tasks are organised within our architecture—$(c_{p})_{p\in\mathbb{N}}$ being successive component models. In our implementation, the adl999Architecture Definition Language. we use for our component models is tacos+/xml [14]. This language using xml101010eXtensible Markup Language.-like syntax is comparable with other adls, in particular Fractal/adl [5], but we mention that the organisation of tacos+/xml texts make very easy the programming of primitive reconfiguration operations mentioned in § 2.3, that is why we chose this adl, a short example is given in [15]. Reconfigurations operations are implemented using xslt111111eXtensible Stylesheet Language Transformations, the language of transformations used for xml documents [27]. Let us note that if another adl is used within a project, there exist xslt programs giving equivalent descriptions in tacos/xml [14]. In particular, that is the case for Fractal/adl.: the input and output are tacos+/xml files.

When we model that the software is running, only one component model is in use, so that may be viewed as the identity function applied to a component model. In the programs given below, we compute each component model belonging to a reconfiguration path. For each component model, we may verify topological properties, e.g., checking that a component or binding is present. As in [15], these topological properties are computed by means of XQuery programs [28]. There is no difficulty about the implementation of reconfiguration operations and property checks, so the descriptions put hereafter concern the part implemented by means of automata.

4.2 Types Used

Now we describe our checking functions at a high level. First we make precise the types used, in order to ease the reading of our functions. The formalism we use is close to type definitions in strong typed functional programming languages like Standard ML [24] or Haskell [23]. Of course, we assume that some types used hereafter—e.g., ‘bool’, ‘int’—are predefined. We use the same names than in [15] for identical notions, and new functions introduced are suffixed by ‘*’ or ‘**’.

As mentioned above, an evolution operation is either the identity function, which expresses that the software is running, or a reconfiguration operation, which is implemented by applying an xslt stylesheet to an xml document and getting the result as another xml document. At a higher-level, such an evolution operation may be viewed as a function which applies to a component model and returns a component model. Likewise, checking a property may be viewed as a function which applies to a component model and returns a boolean value. Assuming that the component-model type has already been defined, we introduce these two function types as:

[TABLE]

An event is defined by an evolution operation and a symbol related to this operation’s result (cf. Def. 3):

[TABLE]

This last information is used by a function checking that the component model got by an evolution operation and the previous component model are equal or different, depending on this symbol121212Let us recall (cf. Def. 3) that if this symbol is ‘terminates’, no additional checking is performed.:

function term-check : event $\rightarrow$ (component-model $\times$ component-model $\rightarrow$ bool)

Let state be the type used for a state of our automata, starting from such a state and a configuration131313That is, a component model (see Def. 2). is expressed by the following type:

type path-check = state $\times$ component-model $\rightarrow$ bool

The following function yields all the transitions starting from a state:

function t : state $\rightarrow$ set-of[transition]

the data belonging to a set can be accessed by means of a ‘for’ expression. A transition starts from a state and returns a state, and the label of such a transition is given by the l function:

[TABLE]

In the following, we will focus on the constructs ‘after’ and ‘always’. The path-check type is used within:

[TABLE]

In other words, check-always*($\mathit{check\text{-}p*}$)($q$,$c$) applies the $\mathit{check\text{-}p*}$ function along the $q$ state, the states reached by transitions originating from $q$, and so on, starting from the $c$ component model. The result of this expression is a boolean value. As soon as applying the $\mathit{check\text{-}p*}$ function yields ‘false’, the process stops and the result is ‘false’. Likewise, check-after*($e$,$\mathit{check\text{-}f*}$)($q$,$c$) also starts from the $q$ state and the $c$ component model; it applies the $\mathit{check\text{-}f*}$ function as soon as the $e$ event is detected as a transition of the automata. The property related to the $\mathit{check\text{-}f*}$ function is to be checked for all the component models resulting from the application of the successive transitions. As a more complete example, the translation of the formula ‘after $e$ always $\mathit{cp}$’—where $e$ is an event and $\mathit{cp}$ a configuration property—is check-after*($e$,check-always*($\mathit{cp}$)), which is a function that applies on a path, starting from a state and component model. The process starts from the initial state of the automaton. Of course, there are similar declarations for functions such as check-before* and check-eventually* (cf. § 2.4).

4.3 Ordering States of Automata

In this section, we introduce some notions related to our automata and used in the following. The states of our automata modelling multiple reconfiguration paths can be ordered with respect to the transitions performed before cycling. Let $\mathcal{A}$ be an automaton, $q_{0}$ its initial state, $L$ its set of transition labels, and $T$ its set of transitions, if $q$ and $q^{\prime}$ are two states of $\mathcal{A}$:

[TABLE]

and $q_{0},q_{1},\ldots,q_{n},q,q^{\prime}_{1},\ldots,q^{\prime}_{p},q^{\prime}$ are pairwise-different. The notation ‘$q\leq q^{\prime}$’ stands for ‘$q<q^{\prime}\vee q=q^{\prime}$’. If we consider the $\mathcal{A}_{0}$ automaton pictured at Fig. 3, $q_{0}<q_{1}<q^{\prime}_{1}<q_{2}<q_{3}<q^{\prime}_{3}<q_{4}<q_{5}<q_{6}<q_{8}$ and $q^{\prime}_{3}<q_{7}<q_{5}$. Obviously, our ‘$<$’ relation is a partial order.

Remark 9

In fact, we build a binary relation step by step by exploring all the possible paths from the initial state, until we reach a state previously explored within the same chain, and our ‘<’ function is the transitive closure of this relation. As a consequence, the transitions which do not satisfy this property are those going back to a state already explored.

5 Our Method’s Functions

5.1 Our Markers

Our main idea—already expressed in [15]—is quite comparable to the modus operandi of a model-checker when it checks the successive states of an automaton in the sense that we mark all the successive states of a multiple reconfiguration path’s automata. The possible values of such a mark are:

unchecked

the initial mark for the steps not yet explored within a reconfiguration path;

again

if a universal property (for all the members of a suffix path) is being checked, it must be checked again at this step if it is explored again;

checked

the property has already been checked, and no additional check is needed if this step is explored again.

However, there is a significant difference between [15] and the present work: in [15], one marker was used for a state. This is impossible here since we have to explore several possible transitions from a same state. Let us consider the multiple reconfiguration path ((e | $\mathit{op}_{0}$) $\mathit{op}_{1}$)+—where $\mathsf{e},\mathit{op}_{0},\mathit{op}_{1}\in\mathcal{R}_{\mathit{run}}$ with $\mathit{op}_{0}\neq\mathsf{e}$, $\mathit{op}_{1}\neq\mathsf{e}$—and a property after e always $\mathit{cp}$. When this regular expression is resumed, there are two cases: either the e event has been recognised, in which case we have to check the $\mathit{cp}$ property on all the successive states and cycling is detected after the new application of the e operation, or $\mathit{op}_{0}$ and $\mathit{op}_{1}$ have been performed and we are still waiting for the e event. We cannot use the same markers for these two cases.

The type of the check-after* function is given in § 4.2. In fact, an automaton modelling a multiple reconfiguration path is pre-processed and its states are marked as unchecked, by means of a new mark, mark-for-after. Then a recursive function check-after**—being the same type—is launched, reads and updates this new mark. The check-always* function behaves the same, the recursive function which is launched is check-always** and the new marker is mark-for-always.

The implementation of the functions check-after** and check-always** is given in Fig. 5. We use a high-level functional pseudo-language, except for updating marks, which is done by means of side effects. A more complete implementation is available at [16], including other features of ftpl, with similar programming techniques and similar methods for proving the termination of our functions and the correctness w.r.t. the definitions given in [10, 11].

5.2 Implementations’ Correctness

Concerning the termination of the functions check-after** and check-always**, the proofs are similar to those given in [15]. The correctness is also ensured for idempotent reconfiguration operations, excluding some operations on parameters, but proofs are here more subtle.

5.2.1 Termination

Proposition 10

The function check-after* terminates.*

Let $q_{0}$ be the initial state of our automaton, a principal call of the check-after** function is:

check-after**($e$,$\mathit{check\text{-}f*}$)($q_{0}$,$c$)

where $e$ is an event, $\mathit{check\text{-}f*}$ a check function being path-check type, $c$ a component model. Recursive calls of this function satisfy the invariant $\forall q_{j}:q_{0}\leq q_{j}<q_{i},\text{{mark-for-after}}(q_{j})=\mathtt{again}$ when it is applied to the $q_{i}$ state. The transitions which may be fired from $q_{i}$ are a finite set, so the ‘for’ loop terminates if for each transition, the process terminates. Let $q_{k}$ be a state reached from $q_{i}$. If $q_{i}<q_{k}$, the invariant holds. If $q_{i}\not<q_{k}$, then $q_{k}$ is a state already explored141414See Rem. 9., that is, the next recursive call applies to a state whose the value of mark-for-after is again. Such a call terminates.

Proposition 11

The function check-always* terminates.*

This termination proof is similar: since transitions which may be fired from $q_{i}$ are a finite set, the ‘for’ loop terminates if for each transition, the process terminates. However, let us notice that a process launched by the check-always** function may start after the beginning of a cycle, and the cycle may have to be entered a second time. Globally, two passes may be needed for an expression such that check-after*$(e,\text{{check-always*}}(cp))$, where $e$ is a reconfiguration operation and $\mathit{cp}$ a formula. Before reaching the end of a cycle, the invariant is:

[TABLE]

when the check-always** function is applied to the $q_{i}$ state. Roughly speaking, when a cycle is performed, this mark has been set either to again, in which case the property has to be checked again, or to checked, in which case our function concludes that the temporal property is true. If the mark has been set to again, it means that the checking of the temporal property ‘always $\mathit{cp}$’ had not begun yet; for example, if we were processing the ‘after’ part of ‘after $e$ always $\mathit{cp}$’. If re-entering a cycle is needed, at a $q^{\prime}_{0}$ state already explored, the invariant is $\forall q_{j}:q^{\prime}_{0}\leq q_{j}<q_{i},\text{{mark-for-always}}(q_{j})=\mathtt{checked}$, $q_{i}$ being the current state. Let $q_{k}$ a state reached from $q_{i}$. If $q_{i}<q_{k}$, the invariant holds. If $q_{i}=q^{\prime}_{0}$, this recursive call of check-always** is performed with the situation:

[TABLE]

that is, the check-always function terminates at this next call.

5.2.2 Restrictions on Formulas

Let us recall that in [15], we were able to deal with finite paths and cycles without continuation, that is, the ‘+’ construct of regular expressions was used only at a final position. In other words, there were no alternatives. In this previous work, we also mentioned that our modus operandi is suitable if the cycle of reconfiguration operations is idempotent. Since the composition of two commutative idempotent functions is idempotent, too, some pairs of reconfiguration operations can be commuted, some consists of operations which neutralised each other, and globally, most cycles used are globally idempotent. Concerning our primitive reconfigurations, most of them are idempotent, e.g., a component’s addition or removal, as well as a binding’s addition or removal. Assigning a constant value to a parameter is idempotent, but general changes are not, e.g., incrementing or decrementing a parameter.

Of course, this limitation still holds for our revised algorithms. Another limitation exists for alternative with a common continuation. As a simple counter-example, let us consider the multiple reconfiguration path ($\mathit{op}_{0}$ | $\mathit{op}_{1}$) $\mathit{op}_{2}$. If we process the formula always $\mathit{cp}$—$\mathit{cp}\in\mathit{CP}$—our algorithm checks the $\mathit{cp}$ formula at the initial state, then at the result of $\mathit{op}_{0}$, then at the result of $\mathit{op}_{2}$ after $\mathit{op}_{0}$. The result of $\mathit{op}_{1}$ applied to the initial state is checked, and the process stops because of the mark put at the common state after $\mathit{op}_{0}$ and $\mathit{op}_{1}$. Now let $\mathit{cp}$ be $\mathit{cp}_{0}\vee\mathit{cp}_{1}$—where $\mathit{cp}_{0},\mathit{cp}_{1}\in\mathit{CP}$—and let us assume that $\mathit{cp}_{0}\wedge\neg\mathit{cp}_{1}$ (resp. $\neg\mathit{cp}_{0}\wedge\mathit{cp}_{1}$) holds on the result of $\mathit{op}_{0}$ (resp. $\mathit{op}_{1}$). If $\mathit{cp}_{1}$ is always false after applying $\mathit{op}_{2}$—e.g., $\mathit{cp}_{1}$ may be related to a binding removed by $\mathit{op}_{2}$—, our method results in an erroneous answer along the path $\mathit{op}_{1}$ $\mathit{op}_{2}$, even it is right for the path $\mathit{op}_{0}$ $\mathit{op}_{2}$.

Solutions exist. We could restrict alternatives of regular expressions by allowing them only at the top level. The counter-example above would be rewritten as ($\mathit{op}_{0}$ $\mathit{op}_{2}$ | $\mathit{op}_{1}$ $\mathit{op}_{2}$), the result of $\mathit{op}_{2}$—as a component model—would be checked twice, one time after applying $\mathit{op}_{0}$, the second after applying $\mathit{op}_{1}$. Adopting such a rule would complicate the processing of a multiple reconfiguration path such as ($\mathit{op}_{0}$ | $\mathit{op}_{1}$)+. Another drawback is that a multiple reconfiguration path may contain alternatives for the corresponding automaton even if the ‘|’ operator is not used explicitly. As an example, let us consider the multiple reconfiguration path $\mathit{op}_{0}$ $\mathit{op}_{1}$? $\mathit{op}_{2}$. The alternative syntactically appears if we rewrite it by means of a grammar—$S$ being the axiom, $S^{\prime}$ another non-terminal symbol, and $\varepsilon$ the empty word—:

S $\longrightarrow$ $\mathit{op}_{0}$ S’ $\mathit{op}_{2}$     S’ $\longrightarrow$ $\mathit{op}_{1}$ | $\varepsilon$

and an analogous counter-example, based on a logical disjunction, can be found for such a case. This drawback does not appear if a non-empty cycle is possibly followed by a continuation, that is, in a multiple reconfiguration path like $\mathit{op}_{0}$+ $\mathit{op}_{1}$. If we rewrite this example by means of a grammar:

S $\longrightarrow$ $\mathit{op}_{0}$ S’     S’ $\longrightarrow$ $\mathit{op}_{0}$ S’ | $\mathit{op}_{1}$

we will see that no common part follows the alternative. This is different if the cycle can be empty. As an example, the multiple reconfiguration path $\mathit{op}_{0}$ $\mathit{op}_{1}$* $\mathit{op}_{2}$ can be rewritten using the following grammar:

S $\longrightarrow$ $\mathit{op}_{0}$ S’ $\mathit{op}_{2}$     S’ $\longrightarrow$ $\mathit{op}_{1}$ S’ | $\varepsilon$

and a common part follows the alternative.

From our point of view, the best solution is to restrict formulas to the strict subset $\mathit{CP}^{\flat}$ defined in § 2.2. In other words, the ‘$\vee$’ connector must not be used, the ‘$\forall$’ quantifier—related to that connector—and the ‘$\neg$’ operator must not, either.

5.2.3 Correctness for Restricted Formulas

Adopting these additional conventions, proving the correctness of our function check-always*—other functions’ correctness is analogouss—is tedious but not really difficult. We have to examine all the basic cases of formulas $\mathit{cp}\in\mathit{CP}^{\flat}$)—e.g., the set membership of a binding—and idempotent reconfiguration operations $\mathit{op}_{0},\mathit{op}_{1},\mathit{op}_{2}$ to show the following proposition.

Proposition 12

Starting from the same state and the same component model, if the formula always $\mathit{cp}$—where $\mathit{cp}\in\mathit{CP}^{\flat}$—holds on the two paths $\mathit{op}_{0}$ $\mathit{op}_{2}$ and $\mathit{op}_{1}$—that is, before and after applying $\mathit{op}_{1}$—it also holds on the multiple reconfiguration path ($\mathit{op}_{0}$ | $\mathit{op}_{1}$) $\mathit{op}_{2}$.

By induction, it is easy to prove such a property about longer paths. It is also easy to prove that if this property holds for the two formulas $\mathit{cp}_{0}$ and $\mathit{cp}_{1}$, it also holds for the formula $\mathit{cp}_{0}\wedge\mathit{cp}_{1}$. An analogous proof exists for the ‘$\forall$’ quantifier. By induction on the number of members of a multiple reconfiguration path, we can prove this proposition by considering a grammar associated with this path, as we sketch in § 5.2.2. As a consequence, if a same state is reached along several paths, the property holds and our function check-always** is correct. Studying the correctness of the function check-after** is easier, because the possible futures of each path of an alternative are explored independently.

6 Discussion and Future Work

Within the framework sketched at § 4.1, the new versions of our programs have been implemented using the Java programming language and can be found in [16]. The descriptions of this paper allow us to be more related to a theoretical model, and to emphasise that our method is close to algorithms based on marking tehniques and used in model-checking, e.g., [8, 9, 25].

As mentioned in the introduction, our method takes place at design-time. We do not deal with a language to describe reconfiguration operations and constraints on these operations as an extension of an adl, as in [26], we are mainly interested in developing effective methods for verifying properties. In [15] we were able to deal with a particular case of infinite paths, based on the fact that often the same sequences are repeated: a component may be stopped in some circumstances, restarted in some circumstances, and so on. However, it is true that this situation was restrictive and the initial motivation of the present work was to introduce alternatives within our paths. Such construct would be irrelevant within methods working at run-time [18, 19], since they observe a process in progress, the history of reconfiguration operations being known. At design-time, it may be interesting to plan several possible behaviours, what is new in comparison with [15]. In the present work, we choose to focus on some efficiency for our algorithms, since common parts are explored once and cycles are explored two times at most, that is, our algorithms are linear with respect to the automaton’s state number. In other words, we are able to explore several possible behaviours quite efficiently, but the price to pay is a restriction of the formulas processed. However, if we look at the examples given within [10, 11, 12, 18], we can think that our restriction is not too cumbersome in practice.

As mentioned above, other solutions exist, but we wanted our extension to be close to our original modus operandi. If we consider a ‘simple’ reconfiguration path, that is, only one transition starts from each state of the corresponding automaton, we get exactly the programs given in [15]. Yet another work may consider only alternatives without syntactic common continuation—possibly by applying some transformation rules—or our algorithms could be changed in order to explore more states in such a case, but this second solution might lead to some combinatorial explosion. Another solution could be based on branching-time logic for reconfiguration alternatives, whereas the present work is based on linear-time logic, as in [10, 11, 12, 18]. Other ideas could be based on a connection with the Model Driven Engineering technical space [3], who would provide more expressive power. Likewise, we could plan a bridge between our approach and others, closer to a semantic level: for example, [20] models reconfiguration operations by means of graph rewriting and uses formal verification techniques along graphs to check properties related to reconfigurations.

On another point, we are interested in this work in reconfigurations, but not in reasons for these reconfigurations151515This is the same in [15]., most often expressed by reconfiguration policies [7]. In parallel, we are working on an extension of [15] taking such policies into account [17]. In the future, we plan to integrate reconfiguration policies into our approach based on mutiple reconfiguration paths.

7 Conclusion

In comparison with methods at run-time, ours may appear as too static, unable to cope with unexpected situations. Our plan is to investigate as far as possible properties that can be checked at design-time, in order for a reconfigurable system to be deployed as safely as possible. Our work can be used for simulations, it may help conceptors design policies involving reconfigurations with good properties. Our tool is not ready for testing policies, but can be used for testing possible results of policies. We see that such an approach does not aim to replace works applied at run-time, but to complement them. About examples such as an http server, we succeeded in proving properties. In other words, we think that our method can provide some significant help at design-time.

Acknowledgements

I am grateful to Olga Kouchnarenko and Arnaud Lanoix, who kindly permitted me to use Figs. 1 & 2. Many thanks to the anonymous referees, who pointed out some omissions and suggested me constructive improvement.