Towards a Calculus for Dynamic Architectures

Abstract

The architecture of a system describes the system’s overall organization into components and connections between those components. With the emergence of mobile computing, dynamic architectures have become increasingly important. In such architectures, components may appear or disappear, and connections may change over time. The dynamic nature of such architectures makes reasoning about their behavior difficult. Since components can be activated and deactivated over time, their behavioral specifications depend on their state of activation. To address this problem, we introduce a calculus for dynamic architectures in a natural deduction style. Therefore, we provide introduction and elimination rules for several operators traditionally employed to specify component behavior. Finally, we show soundness and relative completeness of these rules. The calculus can be used to reason about component behavior in a dynamic environment. This is demonstrated by applying it to verify a property of dynamic blackboard architectures.

1 Introduction

A system’s architecture provides a set of components and connections between their ports. With the emergence of mobile computing, dynamic architectures have become more and more important [2, 8, 16]. In such architectures, components can appear and disappear, and connections can change, both over time. Dynamic architectures can be modeled in terms of configuration traces [14, 15]. Consider, for example, the execution trace of a dynamic architecture depicted in Fig. 1. The figure shows the first three configurations of one possible execution of a dynamic architecture composed of three components $c_1$, $c_2$, and $c_3$. To facilitate the specification of such architectures, they can be separated into behavioral specifications for components, activation specifications, and connection specifications [15]. Thereby, behavior of components is often specified by means of temporal logic formulæ [13] over the components interface. Consider, for example, a component $c_3$ with output port $o_1$ whose behavior is given by the temporal specification “$\bigcirc (o_1=8)$”, meaning that it outputs an 8 on its port $o_1$ at time point 1 (assuming that time starts at 0).

For static architectures, the original specification of temporal properties of single components remain valid even when deployed to the architecture. The original specification of component $c_3$, for example, is still valid when deployed to a static architecture, i.e., $c_3$ will still output an 8 on its port $o_1$ at time point 1, even if deployed to the architecture. For dynamic architectures, on the other hand, the traditional interpretation of temporal specifications of the behavior of components is not valid anymore. For example, it is not clear whether the trace depicted in Fig. 1 actually fulfills the original specification of component $c_3$, since $c_3$ is not active at time point 1 ($n=1$).

So, how can we reason about the behavior of components deployed to dynamic architectures? To answer this question, in the following we provide a calculus for dynamic architectures. It formalizes reasoning about the behavior of a component when it can be activated and deactivated. In the spirit of natural deduction, we provide introduction and elimination rules for each temporal operator. Finally, we show soundness and relative completeness of the calculus. As a practical implication, our calculus can be used to support the verification of properties for dynamic architectures. This is demonstrated by means of the blackboard pattern for dynamic architectures. To this end, we apply the calculus to verify a characteristic property of the pattern.

The remainder of the paper is structured as follows: First, we introduce our model for dynamic architectures in Sect. 2. In Sect. 3, we then provide the notion of behavior assertions and behavior trace assertions as means to specify the behavior of components. In Sect. 4, we introduce our calculus, which allows us to reason about component behavior in a dynamic context. Sect. 5 then demonstrates the practical usability of the calculus by applying it to verify a property of dynamic blackboard architectures. Finally, we conclude our discussion with a review of related work in Sect. 6 and a brief summary of the major contributions of this paper in Sect. 7.

Fig. 1.

Execution trace of a dynamic architecture.

2 A Model of Dynamic Architectures

In [15], we introduce a model for dynamic architectures based on the notion of configuration traces. Our model is based on Broy’s Focus theory [3] and an adaptation of its dynamic extension [4]. In this section, we briefly summarize the main concepts of the model and extend it with the notion of behavior traces to model the behavior of single components.

2.1 Foundations: Ports, Valuations, and Components

In our model, components communicate by exchanging messages over ports. Thus, we assume the existence of sets $\mathsf {M}$ and $\mathsf {P}$ containing all messages and ports, respectively.

Port Valuations. Ports can be valuated by messages. Roughly speaking, a valuation for a set of ports is an assignment of messages to each port.

Definition 1

(Port Valuation). For a set of ports $P\subseteq \mathsf {P}$, we denote by $\overline{P}$ the set of all possible PVs, formally:

$$\begin{aligned} \overline{P}\overset{\text {def}}{\quad =\quad }(P\rightarrow \wp {\left( \mathsf {M}\right) }). \end{aligned}$$

Moreover, we denote by $[p_1,p_2,\ldots \mapsto \{m_1\},\{m_2\},\ldots ]$ the valuation of ports $p_1, p_2, \ldots$ with sets $\{m_1\},\{m_2\},\ldots$, respectively. For singleton sets we shall sometimes omit the set parentheses and simply write $[p_1, p_2, \ldots \mapsto m_1,m_2,\ldots ]$.

Note that in our model, ports can be valuated by a set of messages, meaning that a component can send/receive no message, a single message, or multiple messages at each point in time.

Components. In our model, the basic unit of computation is a component. It consists of an identifier and a set of input and output ports. Thus, we assume the existence of set $\mathsf {C}_{id}$ containing all component identifiers.

Definition 2

(Component). A component is a triple $( id ,I,O)$ consisting of:

• a component identifier $id \in \mathsf {C}_{id}$ and

• two disjoint sets of input and output ports $I,O\subseteq \mathsf {P}$.

The set of all components is denoted by $\mathcal {C}$. For a set of components $C\subseteq \mathcal {C}$, we denote by:

• $\mathsf {in}(C)\overset{\text {def}}{\quad =\quad }\bigcup _{( id ,I,O)\in C} (\{ id \}\times I)$ the set of component input ports,

• $\mathsf {out}(C)\overset{\text {def}}{\quad =\quad }\bigcup _{( id ,I,O)\in C} (\{ id \}\times O)$ the set of component output ports,

• $\mathsf {port}(C)\overset{\text {def}}{\quad =\quad }\mathsf {in}(C)\cup \mathsf {out}(C)$ the set of all component ports, and

• $\mathsf {id}(C)\overset{\text {def}}{\quad =\quad }\bigcup _{( id ,I,O)\in C} \{ id \}$ the set of all component identifiers.

A set of components $C\subseteq \mathcal {C}$ is called healthy iff a component is uniquely determined by its name:

(1)

Similar to Definition 1, we define the set of all possible component port valuations (CPVs) for a set of component $P\subseteq \mathsf {C}_{id}\times \mathsf {P}$.

2.2 Modeling Component Behavior

A component’s behavior is modeled by a set of execution traces over the component’s interface. In the following, we denote with $(E)^+$ the set of all finite sequences over elements of a given set E, by $(E)^\infty$ the set of all infinite sequences over E, and by $(E)^*$ the set of all finite and infinite sequences over E.

Definition 3

(Behavior Trace). A behavior trace for a component $( id ,I,O)$ is an infinite sequence $(\overline{I\times O})^\infty$. The set of all BTs for component c is denoted by $\mathcal {B}(c)$.

Note that a component’s behavior is actually modeled as a set of behavior traces, rather than just a single trace. This is to handle non-determinism for inputs to, as well as outputs from components.

Example 1

(Behavior Trace). In the following, we provide a possible BT for a component $c_3$ with two input ports $i_0$ and $i_1$, and two output ports $o_0$ and $o_1$: $[i_0,i_1,o_0,o_1\mapsto X,5,9,\{8,4\}]$, $[i_0,i_1,o_0,o_1\mapsto \{T,B\},\{2,4\},7,\{3,9\}], \cdots$.

2.3 Modeling Dynamic Architectures

Dynamic architectures are modeled as sets of configuration traces which are sequences over architecture configurations.

Architecture Configurations. In our model, an architecture configuration connects ports of active components.

Definition 4

(Architecture Configuration). An architecture configuration (AC) over a healthy set of components $C\subseteq \mathcal {C}$ is a triple $(C',N,\mu )$, consisting of:

• a set of active components $C'\subseteq C$,

• a connection $N:\mathsf {in}(C')\rightarrow \wp {\left( \mathsf {out}(C')\right) }$, and

• a CPV $\mu \in \overline{\mathsf {port}(C')}$.

We require connected ports to be consistent in their valuation, that is, if a component provides messages at its output port, these messages are transferred to the corresponding, connected input ports:

$$\begin{aligned} \forall p_i\in \mathsf {in}(C') :N(p_i)\ne \emptyset \implies \mu (p_i)=\bigcup _{p_o\in N(p_i)} \mu (p_o). \end{aligned}$$

(2)

The set of all possible ACs over a healthy set of components $C\subseteq \mathcal {C}$ is denoted by $\mathcal {K}(C)$.

Note that connection $N$ is modeled as a set-valued function from component input ports to component output ports, meaning that: (i) input/output ports can be connected to several output/input ports, respectively, and (ii) not every input/output port needs to be connected to an output/input port (in which case the connection returns the empty set).

Configuration Traces. A configuration Traces consists of a series of configuration snapshots of an architecture during system execution.

Definition 5

(Configuration Trace). A configuration trace (CT) over a healthy set of components $C\subseteq \mathcal {C}$ is an infinite sequence $(\mathcal {K}(C))^\infty$. The set of all CTs over C is denoted by $\mathcal {R}(C)$.

Example 2

(Configuration Trace). Fig. 1 shows the first three ACs of a possible CT. The first AC, $t(0)=(C',N,\mu )$, e.g., consists of:

• components $C'=\{C_1,C_2,C_3\}$, with $C_1=(c_1,\{i_0\},\{o_0,o_1,o_2\})$, $C_2=(c_2,\{i_0,i_1,i_2\},\{o_0\})$, and $C_3=(c_3,\{i_0,i_1\},\{o_0,o_1\})$;

• connection $N$, with $N((c_2,i_1))=\{(c_1,o_1)\}$, $N((c_3,i_1))=\{(c_1,o_2)\}$, and $N((c_2,i_2))=\{(c_3,o_1)\}$; and

• valuation $\mu =[(c_1,i_0),(c_1,o_0),(c_2,i_2),\cdots \mapsto 5,9,\{8,4\},\cdots ]$.

Note that a dynamic architecture is modeled as a set of CTs rather than just one single trace. Again, this allows for non-determinism in inputs to an architecture as well as its reaction. Moreover, note that our notion of architecture is dynamic in the following sense: (i) components may appear and disappear over time and (ii) connections may change over time.

In the following, we introduce an operator to denote the number of activations of a component in a (possible finite) configuration trace. Thereby, we denote by $\left[ c\right] ^i=c_i$ the i-th component (where $i\ge 1$ and $i\le n$) of a tuple $c=(c_1, \dots , c_n)$.

Definition 6

(Number of Activations). With $\langle c~\mathop {\#}\limits ^{n}~t\rangle$, we denote the number of activations of component c in a (possibly finite) configuration trace t up to (excluding) point in time n:

$$\begin{aligned} \langle c~\mathop {\#}\limits ^{0}~t\rangle&\overset{\text {def}}{\quad =\quad }0, \\ c\in \left[ t(n)\right] ^1\implies \langle c~\mathop {\#}\limits ^{n+1}~t\rangle&\overset{\text {def}}{\quad =\quad }\langle c~\mathop {\#}\limits ^{n}~t\rangle + 1, \\ c\notin \left[ t(n)\right] ^1\implies \langle c~\mathop {\#}\limits ^{n+1}~t\rangle&\overset{\text {def}}{\quad =\quad }\langle c~\mathop {\#}\limits ^{n}~t\rangle . \end{aligned}$$

Moreover, we introduce an operator to return the last activation of a component in a configuration trace.

Definition 7

(Last Activation). With $last (t,c)$, we denote the greatest $i\in \mathbb {N}$, such that .

Note that $last (t,c)$ is well-defined iff $\exists i\in \mathbb {N}:c\in \left[ t(i)\right] ^1$ and $\exists n\in \mathbb {N}:\forall n'\ge n:c\notin \left[ t(n')\right] ^1$.

Finally, we introduce an operator which for a given point in time returns the least earlier point in time where a certain component was not yet active.

Definition 8

(Least Not Active). With $\langle c\mathop {\vee }\limits ^{n}t\rangle$, we denote the least $n'\in \mathbb {N}$, such that .

Note that $\langle c\mathop {\vee }\limits ^{n}t\rangle$ is always well-defined and for the case in which $c\in \left[ t(n)\right] ^1$, it returns n itself.

2.4 From Configuration Traces to Behavior Traces

In the following, we introduce the notion of projection to extract the behavior of a certain component out of a given CT.

Definition 9

(Projection). Given a (finite or infinite) ${CT} t\in (\mathcal {K}(C))^*$ over a healthy set of components $C\subseteq \mathcal {C}$. The projection to component $c=( id ,I,O)\in C$ is denoted by $\varPi _{c}(t)\in (\mathcal {B}(c))^*$ and defined as the greatest relation satisfying the following equations:

$$\begin{aligned} \varPi _{c}(t\mid _{0})&\overset{\text {def}}{\quad =\quad }\langle \rangle , \\ c\in \left[ t(n)\right] ^1\implies \varPi _{c}(t\mid _{n+1})&\overset{\text {def}}{\quad =\quad }\varPi _{c}(t\mid _{n})~\widehat{~}~\big (\lambda p\in I\cup O:\left[ t(n)\right] ^3( id ,p)\big ), \\ c\notin \left[ t(n)\right] ^1\implies \varPi _{c}(t\mid _{n+1})&\overset{\text {def}}{\quad =\quad }\varPi _{c}(t\mid _{n}), \end{aligned}$$

where denotes the sequence resulting from appending element e to sequence s.

Example 3

(Projection). Applying projection of component $c_3$ to the CT given by Example 2 results in a BT starting as described by Example 1.

Note that for systems in which a component is activated only finitely many times, the projection to this component results in only a finite behavior trace.

3 Specifying Component Behavior

In the following, we introduce the notion of behavior trace assertions, a language to specify component behavior over a given interface specification. We provide its syntax as well as a formal semantics thereof in terms of behavior traces. Finally, we introduce a satisfaction relation for configuration traces which serves as a foundation for the calculus presented in the next section.

3.1 Behavior Trace Assertions

Component behavior can be specified by means of behavior trace assertions, i.e., temporal logic [13] formulæ over behavior assertions. Behavior assertions, on the other hand, are used to specify a component’s state at a certain point in time. They are specified over a given interface specification.

Interface Specifications. Interfaces declare a set of port identifiers and associate a sort with each port. Thus, in the following, we postulate the existence of the set of all port identifiers $\mathsf {P}_{id}$. Moreover, interfaces are specified over a given signature $\varSigma =(S,F,B)$ consisting of a set of sorts $S$, function symbols $F$, and predicate symbols $B$.

Definition 10

(Interface Specification). An interface specification (IS) over a signature $\varSigma =(S,F,B)$ is a triple $(P_{ in },P_{ out },t^p)$, consisting of:

• two disjoint sets of input and output port identifiers $P_{ in },P_{ out }\subseteq \mathsf {P}_{id}$,

• a mapping $t^p:P_{ in }\cup P_{ out }\rightarrow S$ assigning a sort to each port identifier.

The set of all interface specifications over signature $\varSigma$ is denoted by $\mathcal {S}_I(\varSigma )$.

Behavior Assertions. Behavior assertions specify a component’s state (i.e.: valuations of its ports with messages) at a certain point in time. In the following, we do not go into the details of how to specify such assertions, rather, we assume the existence of a set containing all type-compatible behavior assertions over a given interface specification.

Definition 11

(Behavior Assertions). Given ${IS}\ S_i=(P_{ in },P_{ out },t^p)$ over signature $\varSigma =(S,F,B)$ and family of variables $V=(V_s)_{s\in S}$ with variables $V_s$ for each sort $s\in S$. With $\varphi ^{V}_{\varSigma }(S_i)$, we denote the set of all type-compatible (with regard to $t^p$) behavior assertions (BAs) for $S_i$, $\varSigma$, and $V$.

Algebras and Variable Assignments. A BA is always interpreted over a given algebra for the signature used in the corresponding IS. Thus, in the following, we denote by $\mathcal {A}(\varSigma )$ the set of all algebras $(S',F',B',\alpha ,\beta ,\gamma )$ for signature $\varSigma =(S,F,B)$, consisting of sets $S'$, functions $F'$, predicates $B'$, and corresponding interpretations $\alpha :S\rightarrow S'$, $\beta :F\rightarrow F'$, and $\gamma :B\rightarrow B'$. Moreover, with $\mathcal {I}^{V}_{A}$, we denote the set of all variable assignments (VAs) $\iota =(\iota _s)_{s\in S}$ (with $\iota _s:V_s\rightarrow \alpha (s)$ for each $s\in S$) for a family of variables $V=(V_s)_{s\in S}$ in an algebra A.

Semantics of Behavior Assertions. The semantics of behavior assertions is described in terms of component port valuations satisfying a certain behavior assertion. In the following, we denote with $A\leftrightarrow B$ a bijective function from set A to set B.

Definition 12

(Behavior Assertions: Semantics). Given interface specification $S_i=(P_{ in },P_{ out },t^p)\in \mathcal {S}_I(\varSigma )$, a healthy set of components $C\subseteq \mathcal {C}$, component $c=( id ,I,O)\in C$, algebra $A\in \mathcal {A}(\varSigma )$, and $VA \iota =(\iota _s)_{s\in S}\in \mathcal {I}^{V}_{A}$. We denote with that $\mu \in \overline{I\cup O}$ satisfies BA $\gamma \in \varphi ^{V}_{\varSigma }(S_i)$ for port interpretations (PIs) $\delta ^i:I \leftrightarrow P_{ in }$ and $\delta ^o:O \leftrightarrow P_{ out }$.

Behavior Trace Assertions. Behavior trace assertions are a means to specify a component’s behavior in terms of temporal specifications over behavior assertions.

Fig. 2.

Inductive definition of behavior trace assertions.

Definition 13

(Behavior Trace Assertions). For a family of variables $V=(V_s)_{s\in S}$, rigid (fixed for the whole execution) variables $V'=(V'_s)_{s\in S}$, the set of all behavior trace assertions (BTAs) for $IS S_i\in \mathcal {S}_I(\varSigma )$ is given by $\varGamma ^{(V,V')}_{\varSigma }(S_i)$ and defined inductively by the equations provided in Fig. 2.

3.2 Semantics: Behavior Traces

In the following, we define what it means for a behavior trace to satisfy a corresponding behavior trace assertion.

Definition 14

(Semantics BTs). Given algebra A and corresponding VAs $\iota '=(\iota '_s)_{s\in S}\in \mathcal {I}^{V'}_{A}$ for variables $V'$. With , defined recursively by the equations listed in Fig. 3, we denote that BT $t\in \mathcal {B}(c)$ satisfies BA $\gamma \in \varGamma ^{(V,V')}_{\varSigma }(S_i)$ at time $n\in \mathbb {N}$. A BT $t\in \mathcal {B}(c)$ satisfies BA $\gamma \in \varGamma ^{(V,V')}_{\varSigma }(S_i)$, denoted iff .

Fig. 3.

Recursive definition of satisfaction relation for behavior traces.

3.3 Semantics: Configuration Traces

In the following, we define what it means for a configuration trace to satisfy a behavior assertion.

Definition 15

(Semantics CTs). Given algebra A, corresponding VAs $\iota '=(\iota '_s)_{s\in S}\in \mathcal {I}^{V'}_{A}$ for variables $V'$, and behavior trace $t'\in \mathcal {B}(c)$. With

(3)

(4)

(5)

we denote that CT $t\in \mathcal {R}(C)$ satisfies BA $\gamma \in \varGamma ^{(V,V')}_{\varSigma }(S_i)$ at time $n\in \mathbb {N}$ for a given continuation $t'$. Again, a CT $t\in \mathcal {B}(c)$ satisfies BA $\gamma \in \varGamma ^{(V,V')}_{\varSigma }(S_i)$, denoted iff .

To satisfy a given behavior assertion $\gamma$ for a component c at a certain point in time n under a given continuation $t'$, a configuration trace t is required to fulfill one of the following conditions:

• By Eq. (3): Component c is again activated (after time point n) and the projection to c for t fulfills $\gamma$ at the point in time given by the current number of activations of c.

• By Eq. (4): Component c is activated at least once but not again in the future and the continuation fulfills $\gamma$ at the point in time resulting from the difference of the current point in time and the last activation of c.

• By Eq. (5): Component c is never activated and the continuation fulfills $\gamma$ at point in time n.

For the sake of readability, from now on, we omit symbols for algebras and port/variable interpretations for satisfaction relations. An algebra and corresponding interpretations are, however, assumed to be fixed for each property.

The following property ensures correctness of Definition 15:

Proposition 1

(Soundness of Definition 15 ). A CT $t\in \mathcal {R}(c)$ satisfies BA $\gamma \in \varGamma ^{(V,V')}_{\varSigma }(S_i)$ for a given continuation $t'\in \mathcal {B}(c)$ iff the corresponding projection satisfies $\gamma$:

where $s\circ s'$ denotes the sequence resulting from concatenating sequences s and $s'$.

Remember that for architectures in which a component is activated only finitely many times, the projection to this component results in only a finite behavior trace. This is why we actually check for a valid continuation $t' \in \mathcal {B}(c)$.

4 A Calculus for Dynamic Architectures

Until now, is only implicitly defined in terms of . While this mirrors our intuition about , it is not very useful to reason about it. Thus, in the following section, we provide an explicit characterization of in terms of a calculus for dynamic architectures. Then, we show soundness and relative completeness of the calculus with regard to Definition 15. Using a natural deduction style, we provide introduction and elimination rules for each temporal operator.

4.1 Introduction Rules

We provide 8 rules which can be used to introduce temporal operators in a dynamic context.

Behavior Assertions. The first rules characterize introduction for basic behavior assertions. Therefore, we distinguish between three cases: First, the following case in which a component is guaranteed to be eventually activated in the future:

For this case, in order to show that a BA $\phi$ holds at time point n, we have to show that $\phi$ holds at the very next point in time at which component c is active.

For the case in which a component was sometimes active, but is not activated again in the future, we get the following rule:

In order to show that BA $\phi$ holds at a certain point in time n, we have to show that $\phi$ holds for the continuation $t'$. Note that the corresponding time point is calculated as the difference from n to the last point in time at which component c was active in t.

Finally, we have another rule for the case in which component is never activated:

For such cases, BA $\phi$ holds at a certain point in time n when $\phi$ holds for $t'$ at time point n.

Next. The next rule characterizes introduction for the next operator. For this operator as well, we distinguish two cases: The first case is again the one in which a component is guaranteed to be eventually activated in the future:

For this case, in order to show that a BTA $\bigcirc \gamma$ holds at a certain point in time n, we have to show that it holds after the very next activation of c in t.

For the case in which a component is not activated again in the future, we get the following rule for the next operator:

In this case, the dynamic interpretation of the operator resembles its traditional one. Thus, it suffices to show that BTA $\gamma$ holds for the next point in time $n+1$, in order to conclude that $\bigcirc \gamma$ holds at n.

Eventually. Introduction for the eventually operator can be described with a single rule:

It states that in order to show that $\diamondsuit \gamma$ holds for a component c at some point in time n, we only have to show that $\gamma$ holds at some time point later than the last activation (before n) of c.

Globally. Similarly, we provide a single introduction rule for the globally operator:

It allows us to conclude $\Box \gamma$ for time point n whenever we can show that $\gamma$ holds for an arbitrary $n'\ge n$.

Until. Finally, we provide a single rule for introducing the until operator:

In order to show that $\gamma '~\mathcal {U}~\gamma$ holds for a component c at some point in time n, the rule requires to show that $\gamma$ holds at some point $n'$ later than the last activation (before n) of c and that for every time point up to the last activation of component c before $n'$ (or the last time point $n''<n'$ for the case component c is not activated anymore), $\gamma '$ holds.

4.2 Elimination Rules

In contrast to introduction, we provide 10 rules for the elimination of the different temporal operators.

Behavior Assertions. Again, we first provide rules characterizing elimination for basic behavior assertions. Similar to introduction, we distinguish between three cases: The first case describes elimination for situations in which a component is guaranteed to be activated sometimes in the future:

The rule for such cases allows us to eliminate a basic BA $\phi$ and conclude that $\phi$ holds at the very next point in time where component c is active.

The next rule deals with the case in which a component was sometimes active, but is not activated again in the future.

The rule for this case allows us to conclude that a BA $\phi$ holds at a certain point in time for continuation $t'$. Again, the corresponding time point is calculated as the difference of n and the last time component c was activated.

Finally, we have another rule for the case in which component is never activated:

For such cases, we may eliminate $\phi$ and conclude that $\phi$ holds at n for continuation $t'$.

Next. Similar to introduction, we provide two rules to eliminate a next operator: The first rule deals again with the case in which a component is guaranteed to be activated sometimes in the future:

Similar to the corresponding introduction rule, this rule allows us to conclude BTA $\gamma$ for a certain point in time $i+1$, whenever $\bigcirc \gamma$ holds at an earlier point in time n and i is the very next activation of component c.

If a component is not activated again, we get the following rule for eliminating a next operator:

Again, the rule resembles the traditional interpretation of next, which allows us to conclude that BTA $\gamma$ holds for a certain point in time $n+1$, whenever $\bigcirc \gamma$ holds at n.

Eventually. We provide two rules to eliminate an eventually operator:

When eliminating a $\diamondsuit \gamma$ for a component c at time point n, the rule allows us to conclude that BTA $\gamma$ holds sometimes after the last activation (before n) of component c.

A similar rule applies for the case in which c is not activated again (). For this case (denoted $\mathrm {EvtE_n}$), however, we can conclude that the corresponding point in time $n'$ is actually greater than n instead of $\langle c\mathop {\vee }\limits ^{n}t\rangle$.

Globally. Similar to introduction, we have a single rule for the elimination of a globally operator:

The rule allows us to eliminate $\Box \gamma$ for component c at time point n and conclude that $\gamma$ holds at an arbitrary point later than the last activation of c before n.

Until. Finally, we provide two rules to eliminate until operators:

Assuming that $\gamma '~\mathcal {U}~\gamma$ holds at some time point n, the rule allows us to conclude that there exists a time point in the future $n'$, such that BTA $\gamma$ holds and that up to the last activation of component c earlier to $n'$ (or the last time point $n''<n'$ for the case component c is not activated anymore), BTA $\gamma '$ holds.

Again, a similar rule applies for the case in which c is not activated again (). For this case (denoted $\mathrm {UntilE_n}$), however, we can conclude that the corresponding point in time $n'$ is actually greater than n instead of $\langle c\mathop {\vee }\limits ^{n}t\rangle$.

4.3 Soundness and Completeness

In the following, we show soundness and relative completeness of the calculus. Thereby, we denote with that it is possible to derive with the rules introduced in Sect. 4. With , on the other hand, we denote that configuration trace t indeed satisfies BTA $\gamma$ at time point n.

Theorem 1

(Soundness). The calculus presented in Sects. 4.1 and 4.2 is sound:

Proof

(Sketch). For each rule, we assume its premises and prove its conclusions from Definitions 14 and 15.

Theorem 2

(Completeness). The calculus presented in Sects. 4.1 and 4.2 is complete (relative to the completeness of ):

Proof

(Sketch). The validity of each BTA can be derived by applying the corresponding introduction rules.

5 Verifying Properties of Dynamic Architectures

In the following, we demonstrate the practical usability of the calculus presented in Sect. 4. Therefore, we specify a dynamic version of the blackboard architecture pattern and apply our calculus to verify a simple property of such architectures.

5.1 Dynamic Blackboard Architectures: Specification

In the following, we introduce a simplified version of the blackboard pattern as described, for example, by Shaw and Garlan [18], Buschmann et al. [5], and Taylor et al. [19]. Therefore, we first specify the involved datatypes, the components interfaces, and constraints regarding the activation/deactivation of components as well as connections between their ports. Then we provide a specification of component behavior in terms of BTAs.

Fig. 4.

Specification of the blackboard pattern.

Datatypes. Blackboard architectures work with problems and solutions for them. Figure 4a provides the corresponding datatype specification (DTS) in terms of an algebraic specification [21]. We denote by $\mathtt {PROB}$ the set of all problems and by $\mathtt {SOL}$ the set of all solutions. To relate a problem with a corresponding solution, we assume the existence of a function $s :\mathtt {PROB}\rightarrow \mathtt {SOL}$ which assigns the correct solution to each problem.

Interfaces. In our example, a blackboard architecture consists of a blackboard (BB) component and a knowledgesource (KS) component. The configuration diagram (CD) [14] in Fig. 4c shows the specification of the corresponding interfaces. In our simple example, the BB component merely forwards messages to and from the KS component. Thus, it has an input port $i_p$ which receives a problem and an output port $o_s$ which returns the corresponding solution. Moreover, it has an output port $p_p$ to forward a problem to a KS and a corresponding input port $p_s$ to receive its solution. A KS, in our example, gets a problem on its input port $p_p$ and provides a corresponding solution on its output port $p_s$.

Activation Constraints. Activation constraints restrict the activation or deactivation of components. They are introduced by CDs and refined by activation assertions (AAs).

In our example, the “$bb : BB$” and “$ks : KS$” annotations for a BB and KS interface, respectively, denote the condition that there are unique BB and KS components denoted $bb$ and $ks$, respectively. Moreover, we require three more activation constraints formulated as AAs in Fig. 5:

Fig. 5.

Specification of activation constraints for blackboard architectures.

• By Eq. (6) we require $ks$ to be active whenever $bb$ posts a problem.

• By Eq. (7) we require a fairness condition for the activation of an already activated $ks$.

• By Eq. (8) we require that $bb$ is always active.

Connection Constraints. Connection constraints restrict the connection between components. They are introduced by CDs and refined by connection assertions CAs.

In our example, connection constraints are also specified graphically by the CD in Fig. 4c. The solid connections between the ports denote a constraint requiring that the ports of a KS component are connected with the corresponding ports of a BB component as depicted, whenever both components are active.

Behavior Specifications. Behavior is specified in terms of BTAs as introduced in Sect. 3. Note that we do not consider activation and deactivation of a component when specifying its behavior. Rather, this is done in a separate specification and our calculus can then be used to reason about such behavior, in a dynamic environment as well.

Fig. 6.

Specification of behavior for blackboard components.

Fig. 7.

Specification of behavior for knowledgesource components.

In Fig. 6, we specify two simple properties for BB components. They merely require messages from their input ports to be forwarded to the corresponding output ports. Figure 7 provides a specification of the KS’s behavior. The property requires that whenever a problem is received it is guaranteed to be eventually solved.

5.2 Dynamic Blackboard Architectures: Verification

In the following, we demonstrate how the calculus proposed in Sect. 4 can be used to verify a simple property of blackboard architectures as specified above.

A simple property of a blackboard architecture as specified above is that a problem is always solved. Expressed in terms of a behavior assertion over a blackboard interface, it looks as follows:

(12)

It actually resembles the behavior property of KS components. Its proof is split into 4 parts.

First, we apply introduction for the globally and eventually operators to our goal. Thereby we use Hilbert’s $\varepsilon$-operator to denote an arbitrary but fixed element satisfying a certain property. Moreover, we use Ass to abbreviate the assumption for later reference.

We are now left with the goal of showing that the solution to the original problem p is provided by the blackboard at port $o_s$ at some point in time later than the last activation of the blackboard. To discharge the proof obligation, we apply elimination for the globally operator and the behavior specification of blackboards. In the following, we abbreviate $\varepsilon n'.~n'\ge \langle bb \mathop {\vee }\limits ^{n}t\rangle$ with $n^*$.

We are left with the goal of showing that the solution for p is indeed received by the blackboard. To this end, we apply connection constraints from the CD as well as elimination rules for eventually and globally.

Finally it remains to show that the knowledgesource indeed receives the original problem. To discharge this obligation, we simply again apply the constraints induced by the CD as well as the behavioral specification of the blackboard component.

Note that one of the premises is closed by reference to the assumption $Ass$ obtained at the beginning of the proof.

6 Related Work

Related work can be found in two different areas: work on the specification of dynamic architectures in general and calculi about dynamic systems specifically.

Over the last years, some approaches to the specification of dynamic architectures in general have emerged. One related approach comes from Le Métayer [12], who applies graph theory to specify architectural evolution. Similar to our work, the author proposed to model dynamic architectures as a sequence of graphs and to employ graph grammars as a technique to specify architectural evolution. A similar approach comes from Hirsch and Montanari [11], who employ hypergraphs as a formal model to represent styles and their reconfigurations. Another, closely related approach is the one used by Wermlinger et al. [20]. The authors combine behavior and structure to model dynamic reconfigurations. Recently, categorical approaches to dynamic architecture reconfiguration have appeared, such as the work of Castro et al. [7] and Fiadeiro and Lopes [9]. While they all introduce models for dynamic architectures similar to ours, they do not provide a calculus to reason about such architectures. Thus, we complement their work by providing rules to reason about such architectures.

A second area of work concerns approaches to reason about dynamic systems in general: Pioneering work in this area goes back to Milner in his well-known work on the $\pi$-calculus [17]. Here, the author provides a set of rules to reason about reconfigurable systems in general. The main idea behind the underlying model is that channels can be passed as messages between processes, which can then exchange messages over these channels. Another foundational model of dynamic systems which provides rules to reason about such systems is the Chemical Abstract Machine (CHAM) [1]. It is built upon the chemical metaphor and models a system as multi-set transformers. Thereby it also provides a set of general laws to reason about such systems. Finally, the ambient calculus [6] can be seen as an advancement of the CHAM. In contrast to membranes in CHAM, ambients provide stronger protection and provide mobility for sub-solutions as well. While all these approaches provide rules to reason about dynamic systems in general, their underlying model of dynamic systems is different from our model of dynamic architectures. Thus, we actually complement their work by providing rules to reason about different types of systems.

7 Conclusion

In this paper, we introduce a framework to reason about the behavior of components deployed to a dynamic environment. The major contributions of the paper can be summarized as follows: (i) We extend our model of dynamic architectures introduced in [15] with the notion of behavior traces to model behavior of single components. Thereby we also characterize an operator to extract the behavior of single components out of a given configuration trace. (ii) We introduce the notion of behavior trace assertions to specify behavior of single components and provide its formal semantics in terms of behavior traces. (iii) We provide a calculus to reason about the behavior of components in dynamic architectures. It is in a natural deduction style and provides introduction and elimination rules for each operator of behavior trace assertions. (iv) We show soundness and relative completeness of the calculus.

Our results can be used to support the verification of dynamic architectures. This was demonstrated by applying our calculus to verify a property for a dynamic version of the blackboard architecture pattern. Our overall research is directed towards a unified framework for the specification and verification of patterns for dynamic architectures. By introducing the calculus, we provide an important step towards this overall goal. However, future work is still required in three major directions: (i) To better support verification, we are aiming at integrating the calculus in Isabelle/HOL. Very much in the spirit of LCF [10], we are currently working on a mechanized proof of the rules of the calculus from first principles. (ii) Moreover, the calculus should be extended to better integrate port connections. (iii) We are currently looking for ways to leverage the hierarchical nature of patterns for their verification. Thus, we are interested in theoretical results of how results for one pattern can be reused for the verification of other, related patterns.