Formal Specification and Verification of Dynamic Parametrized Architectures
Abstract
We propose a novel approach to the formal specification and verification of dynamic architectures that are at the core of adaptive systems such as critical infrastructure protection. Key features include runtime reconfiguration based on adding and removing components and connections, resulting in systems with unbounded number of components. We provide a logicbased specification of a Dynamic Parametrized Architecture (DPA), where parameters represent the infinitestate space of possible configurations, and firstorder formulas represent the sets of initial configurations and reconfiguration transitions. We encode information flow properties as reachability problems of such DPAs, define a translation into an arraybased transition system, and use a Satisfiability Modulo Theories (SMT)based model checker to tackle a number of case studies.
1 Introduction
In many applications, safetycritical systems are becoming more and more networked and open. For example, many critical infrastructures such as energy distribution, air traffic management, transport infrastructures, and industrial control nowadays employ remote communication and control. Critical infrastructure protection is becoming of paramount importance as witnessed for example by related European and US frameworks [1, 2] which promote actions to make critical infrastructures more resilient.
In order to be resilient, a system must be adaptive, changing its architectural configuration at runtime, due to new requirements, component failures or attacks. A reconfiguration means adding and removing components and connections, so that the resulting system has an infinite state space where each state is an architectural configuration. In this context, simple reachability properties such as the existence of information flow paths become very challenging due to the interplay between communications and reconfigurations. The design, implementation, and certification of a system with such properties are the challenges of the European project CITADEL [3].
While the literature about the formal specification of dynamic software architectures is abundant [5, 7, 8, 9, 10, 21, 24, 25, 26, 31, 32, 33], very few works consider their formal verification and none of them provided a concrete evaluation showing the feasibility of the proposed analysis.
If the number of components is bounded, formal verification can be reduced to static verification by encoding in the state if the component is active or not with possibly an additional component to control the (de)activation (see, for example, [9]). If, instead, new components can be added, the encoding is less trivial. In principle, parametrized verification, by verifying a system considering any number of replicas of components, seems a good candidate, but we need the capability to encode in the state the activation of an unbounded number of components.
In this paper, we propose Dynamic Parametrized Architectures (DPAs), which extend a standard architecture description of components and connections with (1) parameters and symbolic constraints to define a set of configurations, (2) symbolic constraints to define the sets of initial configurations and reconfigurations. In particular, the architectural topology is represented by indexed sets of components and symbolic variables that can enable/disable the connections, while the constraints are specified with firstorder formulas with quantifiers over the set of indices.
We propose to use Satisfiability Modulo Theories (SMT)based model checking for arraybased transition systems [13, 19], a syntactically restricted class of parametrized transition systems with states represented as arrays indexed by an arbitrary number of processes. We define carefully the fragment of firstorder logic used in the architecture description so that we can provide a translation into arraybased transition systems.
In this paper, we focus on simple information “canflow” properties over DPAs: we check if information can pass from one component to another one through a sequence of communications between connected components and reconfigurations. We automatically translate the DPA and the properties into an arraybased transition system and we verify the properties with Model Checker Modulo Theories (MCMT) [19].
Summarizing, the contributions of the paper are: (1) to define a new formal specification of dynamic architectures; (2) to translate the reachability problem of dynamic architectures into reachability problems for infinitestate arraybased transition systems; (3) to provide a prototype implementation and an experimental evaluation of the feasibility of the approach.
The rest of the paper is structured as follows: Sect. 2 gives an account of related work; Sect. 3 exemplifies the problem using a concrete language; Sect. 4 defines the abstract syntax and semantics of DPAs; Sect. 5 describes arraybased transition systems and the translation from DPAs; Sect. 6 presents some benchmarks and experimental results; and, finally, in Sect. 7, we draw some conclusions and directions for future works.
2 Related Work
The approach closest to the one presented below is proposed in [31] as extension of the BIP (Behavior, Interaction, Priority) framework [6]. BIP has been extended for dynamic and parametrized connections in [7, 23], and to allow spawning new components and interactions in [9]. The work in [31] proposes a secondorder logic to specify constraints on the evolution of the architecture including creation/removal of components. However, no model checking procedure is provided to verify such dynamic architectures. In this paper, we restrict the logic, for example avoiding secondorder quantification, so that the language is still suitable to describe interesting dynamics but can be translated into arraybased transition systems for model checking.
Since a system architecture can be seen as a graph of connections, graph grammars [29] are a good candidate for specification of dynamic architectures. In fact, in [21, 26, 32, 33], the authors propose to model dynamic architectures in terms of graph transformation systems: the initial configuration is represented by a graph (or hypergraph) and reconfigurations as graph production rules, which are based on subgraph matching. In [21, 26, 32], there is no attempt at formal verification, while in [33] it is limited to finitestate model checking. Moreover, compared to our language, reconfigurations are limited to matching a finite subgraph which does not allow to express transition guards based on negation or updates that change sets of components. These limitations can be partly lifted considering infinitestate attributed graph grammars and related verification techniques [22]. After a first attempt to use these techniques as backends for DPAs, we concluded that in practice they do not scale very well on our benchmarks.
\(\pi \)calculus [27] is another clear candidate to represent the semantics of dynamic architectures, since it has the ability to describe the creation of processes and their dynamic synchronizations. As is, it does not clearly define the topology of the network, but works such as [10, 24] use it as underlying semantics for dynamic extensions of architecture specification languages. Also in this context, no previous work provided a concrete proposal for model checking showing the feasibility of the approach.
The analysis of how information can flow from one component to another is addressed in many contexts such as program analysis, process modeling, access control, and flow latency analysis. The novel challenge addressed by this paper is posed by the complexity of the adaptive systems’ architectures, for which design and verification is an open problem. We propose a very rich system specification and we provide verification techniques for simple information flow properties formalized as reachability problems.
In this paper, we consider information flow as reachability, which is well studied for standard state machine models. More complex information flow properties extensively studied in the literature on security are related to the notion of noninterference. In the seminal work of Goguen and Meseguer [20], the simple information flow property is extended to make sure that components at different levels of security do not interfere. The verification of noninterference on DPAs is an open problem left for future work.
3 An Example of a Dynamic Parametrized Architecture
In this section, we describe an example of a dynamic architecture in an extended version of the Architecture Analysis and Design Language (AADL) [16], which is an industrial language standardized by SAE International [30]. The concrete language extension is under definition [12] within the CITADEL project, while in this paper we focus on the underlying formal specification and semantics of DPAs.
 1.
Parametrized Architecture: the subcomponents can now be indexed sets (e.g., Open image in new window is a set indexed by Open image in new window ) and connections are specified iterating over the indices (e.g., there is a connection from Open image in new window to Open image in new window for each Open image in new window in Open image in new window , Open image in new window in Open image in new window ); besides the sets of indices, the architecture is parametrized by other parameters that can be used in expressions that guard the connections (e.g., there exists a connection from Open image in new window to Open image in new window only if Open image in new window ); notice that also parameters may be indexed sets.
 2.
Dynamic Parametrized Architecture: an Open image in new window formula defines the set of initial configurations; a set of Open image in new window defines the possible changes in the values of the parameters.
The version of the example with the highlighted parts is safe because it introduces two phases (represented by the Open image in new window parameter) and it allows connection to the database only in the protected mode, while reconfigurations downgrading the servers are allowed only in the unprotected mode. Proving automatically that this system is safe is quite challenging.
4 Formal Specification of Dynamic Parametrized Architectures
4.1 Definitions
In the following, let N be a countable set of indexes (in practice, we set \(N=\mathbb Z\)). An index set is a finite subset of N. Given a set S and an index set I, S is indexed by I iff there exists a bijective mapping from I to S. If S is indexed by I, we write \(S=\{s_i\}_{i\in I}\). An index set parameter is a variable whose domain is the set of finite subsets of N.
Definition 1
An architectural configuration is a pair (C, E), where C is a set of components and \(E \subseteq C \times C\) is a set of connections between components.
We now define a more structured version of architecture, still flat but in which components are grouped into sets. We use indexed sets of components. For example, \(I=\{1,2,3\}\) is a set of indexes and \(C=\{c_1,c_2,c_3\}\) and \(C'=\{c'_1,c'_2,c'_3\}\) are two sets of components indexed by I.
Definition 2

\(\mathcal {C}\) is a finite set of disjoint sets of components indexed by some index sets;

\(E \subseteq \bigcup _{C\in \mathcal {C}} \times \bigcup _{C\in \mathcal {C}}\) is a set of connections between components.
If \(c\in C\) and \(C\in \mathcal {C}\) we write simply (abusing notation) \(c\in \mathcal {C}\).
For example, consider index sets \(I_1,I_2\), where \(I_1=\{1,2,3\}\), \(I_2=\{2\}\), \(\mathcal {C}=\{C_1,C_2, C_3\}\), \(C_1=\{c_{1i}\}_{i\in I_1}\), \(C_2=\{c_{2i}\}_{i\in I_1}\), \(C_3=\{c_{3i}\}_{i\in I_2}=\{c_{32}\}\), \(E=\{\langle c_{1i},c_{2i}\rangle \mid i\in I_1\}\).
Definition 3
A system of parameters is a pair \((\mathcal {I}, \mathcal {V})\) where \(\mathcal {I}\) is a finite set of symbols for index set parameters and \(\mathcal {V}\) is a finite set of symbols for indexed sets of parameters, where each \(V \in \mathcal {V}\) is associated with an index set parameter symbol \(I_V \in \mathcal {I}\) and with a sort \(\texttt {sort} _V\) (in practice, \(\texttt {sort} _V \in \{\texttt {bool} , \texttt {int} \}\)).
Definition 4

\(\mu _\mathcal {I}: \mathcal {I} \rightarrow \{S \subset N: S \text {finite}\}\);

For \(V\in \mathcal {V}\), \(\mu _V: \mu _\mathcal {I}(I_V) \rightarrow R(sort_V)\) (in practice, \(R(\texttt {bool} ) = \mathbb {B} = \{\top , \bot \}\) and \(R(\texttt {int} ) = \mathbb {Z}\)).
The following definitions refer to formulas of the logic for systems of parameters and the evaluation (under an assignment \(\mu \)) \(\llbracket \mathord {\cdot }\rrbracket _\mu \) of its expressions and formulas. These are defined later in Sect. 4.2.
Definition 5

\((\mathcal {I}, \mathcal {V})\) is a system of parameters;

\(\mathcal {P}\) is a finite set of parametrized indexed sets of components; each set \(P\in \mathcal {P}\) is associated with an index set \(I_P\in \mathcal {I}\);

\(\varPsi =\{\psi _P(x)\}_{P\in \mathcal {P}}\) is a set of formulas (component guards) over \((\mathcal {I}, \mathcal {V})\) and a free variable x;

\(\varPhi =\{\phi _{PQ}(x,y)\}_{P,Q\in \mathcal {P}}\) is a set of formulas (connection guards) over \((\mathcal {I}, \mathcal {V})\) and free variables x, y.

\(\mathcal {C} = \{C_{\mu P}: P \in \mathcal {P}\}\). For all \(C_{\mu P}\in \mathcal {C}\), for all indexes i, \(c_{Pi} \in C_{\mu P}\) iff \(i\in \mu _{\mathcal {I}}(I_P)\) and \(\llbracket \psi _P(i/x)\rrbracket _\mu = \top \).

for all \(C_{\mu P},C_{\mu Q}\in \mathcal {C}\), for all component instances \(c_{Pi}\in C_{\mu P}\), \(c_{Qj}\in C_{\mu Q}\), \((c_{Pi},c_{Qj})\in E\) iff \(\llbracket \phi _{PQ}(i/x,j/y)\rrbracket _\mu = \top \).
Syntactic restrictions: formulas in \(\varPsi \) and \(\varPhi \) are quantifierfree and do not contain index set predicates \(=\), \(\subseteq \).
Example: For \(\mathcal {I}=\{I_1,I_2\}\), \(\mathcal {V}=\{V\}\), V a set of Boolean variables, with \(I_V=I_1\), \(\mathcal {P}=\{P_1,P_2,P_3\}\), \(I_{P_1}=I_1\), \(I_{P_2}=I_1\), \(I_{P_3}=I_2\), \(\psi _{P_1}(x) = \psi _{P_2}(x) = \psi _{P_3}(x):=\top \), \(\phi _{P_1P_2}(x,y):=x=y\wedge x\in I_V\wedge V[x]\), \(\phi _{P_1P_3}(x,y):=x\in I_V\wedge \lnot V[x]\), \(\phi _{P_2P_3}(x,y)=\phi _{P_2P_1}(x,y)=\phi _{P_3P_1}(x,y)=\phi _{P_3P_2}(x,y):=\bot \). By assigning \(\mu _\mathcal {I}(I_1)=\{1,2,3\}\), \(\mu _\mathcal {I}(I_2)=\{2\}\), \(\mu _V(1)=\mu _V(2)=\mu _V(3)=\top \), we get the configuration in the previous example.
Definition 6

\(A = (\mathcal {I},\mathcal {V},\mathcal {P},\varPsi ,\varPhi )\) is a parametrized architecture;

\(\iota \) is a formula over \((\mathcal {I}, \mathcal {V})\), specifying the set of initial assignments;

\(\kappa \) is a formula over \((\mathcal {I}, \mathcal {V})\), specifying the invariant;

\(\tau \) is a transition formula over \((\mathcal {I}, \mathcal {V})\), specifying the reconfiguration transitions.

\(\iota \) is of the form \(\forall _{\underline{I}_1}\underline{i}_1\forall _{\underline{I}_2^C}\underline{i}_2\ \alpha \), where \(\alpha \) is a quantifierfree formula in which index set predicates \(=\), \(\subseteq \) do not appear under negation.

\(\kappa \) is a quantifierfree formula without index set predicates \(=\), \(\subseteq \).
 \(\tau \) is a disjunction of transition formulas of the form \(\exists _{\underline{I}_1}\underline{i}_1\exists _{\underline{I}_2^C} \underline{i}_2 \left( \alpha \wedge \beta \wedge \gamma _\beta \right) \) where \(\underline{I}_1,\underline{I}_2 \subseteq \mathcal I\), \(\alpha \) is a quantifierfree formula, \(\beta \) is a conjunction of transition formulas of the forms 1) \(I' = I \cup \{t_k\}_k\), 2) \(I' = I \setminus \{t_k\}_k\), 3) \(t \in I'\), 4) \(V'[t] = e\), 5) \(\forall _{I'_{V'}} j\ V'[j] = e\), where \(I\in \mathcal I,I'\in \mathcal I'\) are variables of sort is (each variable \(I'\in \mathcal I'\) may appear at most once), \(t,t_k\) are terms over \((\mathcal {I}, \mathcal {V})\) of sort idx, \(V'\in \mathcal {V'}\) is a variable of one of the sorts \(\texttt {vs} _k\) (for each \(V'\), either atoms of the form 4 appear in \(\beta \), or at most a single atom of the form 5 appears: atoms of forms 4, 5 never appear together), e are terms over \((\mathcal {I}, \mathcal {V})\) of sorts \(\texttt {el} _k\), and j is a variable of sort idx; furthermore, value \(V'[t_k]\) of every introduced (by an atom of form 1,with \(I' = I'_{V'}\) and \(I = I_V\)) parameter must be set in \(\beta \) with an atom of form 4 or 5; finally, the frame condition \(\gamma _\beta \) is a conjunction of

transition formulas \(\forall _{I'_{V'}} j \left( \left( \bigwedge _{t\in t_{ V'}}(j\ne t)\right) \rightarrow V'[j]=V[j]\right) \) for all \(V' \in \mathcal {V}\) which do not appear in a conjunct of form 5 in \(\beta \), where \(t_{V'}\) is the (possibly empty) set of all terms which appear as indexes of \(V'\) in \(\beta \), and

transition formulas \(I' = I\) for all \(I' \in \mathcal {I}'\) which do not appear in conjuncts of forms 1, 2 in \(\beta \).

Example: Consider the parametrized architecture from the previous example, with \(\iota :=I_1=\{1,2,3\}\wedge I_2=\{2\}\wedge V[1]\wedge V[2]\wedge V[3]\); , \(\kappa :=\top \) and \(\tau :=\tau _1\vee \tau _2\), where \(\tau _1:=\exists _{I_1^C}i\left( I_1'=I_1\cup \{i\}\wedge V'[i]\right) \) and \(\tau _2:=\exists _{I_1} i\left( \lnot V'[i]\right) \). This defines the set of initial architectures which contains only the single architecture from the previous example and two transitions. The transition \(\tau _1\) adds a new index \(i\in I_1^C\) into the index set \(I_1\), adding two new components \(C_{1i}\) and \(C_{2i}\) and a new parameter V[i] and sets the value of the newly added parameter V[i] to \(\top \), adding a connection between the two new components \(C_{1i}\) and \(C_{2i}\). The transition \(\tau _2\) changes the value of some V[i] to \(\bot \), removing the connection between components \(C_{1i}\) and \(C_{2i}\) and adding connections between component \(C_{1i}\) and each of the components \(C_{3j},j\in I_2\).
Definition 7
Given a dynamic parametrized architecture \((A, \iota , \kappa , \tau )\), where \(A = (\mathcal {I}, \mathcal {V},\mathcal {P}, \varPsi ,\varPhi )\), a configuration is an assignment to the system of parameters \((\mathcal {I}, \mathcal {V})\). For a configuration \(\mu (A) = (\mathcal {C}, E)\), a communication event is a connection \(e \in E\).

\(e_1 = \mu _1\) is a configuration such that \(\mu _1(A)\) is in the set of initial configurations.

The subsequence \(e_{k_1}, e_{k_2}, \ldots \) of all configurations in the trace is such that for all \(k_i\), \(e_{k_{i+1}}(A)\) (if it exists) is directly reachable from \(e_{k_i}(A)\).

For all communication events \(e_k = (c_k, c_k')\) in the trace, \((c_k, c_k') \in E_{e_{r(k)}}\), where \(e_{r(k)}\), \(r(k) := \max \{n \in \mathbb {N}: n < k, e_n \text {is a configuration}\}\), is the last configuration prior to \(e_k\).
Definition 8

\(D=(A,\iota ,\kappa ,\tau )\) is a dynamic parametrized architecture;

\(P_{src}\in \mathcal P_A\) and \(P_{dst}\in \mathcal P_A\) are (source and destination) parametrized indexed sets of components;

\(\rho _{src}(x)\) and \(\rho _{dst}(x)\) (source and destination guard) are formulas over \((\mathcal I_A,\mathcal V_A)\).

\(c_{k_1}=c_{P_{src}i_{src}}\in C_{e_{r(k_1)}P_{src}}\) for some \(i_{src}\), and \(\llbracket \rho _{src}( i_{src}/x)\rrbracket _{e_{r(k_1)}}=\top \) (the information originates in a source component);

\(c_{k_m}'=c_{P_{dst}i_{dst}}\in C_{e_{r(k_m)}P_{dst}}\) for some \(i_{dst}\), and \(\llbracket \rho _{dst}( i_{dst}/x)\rrbracket _{e_{r(k_m)}}=\top \) (the information is received by a destination component);

for all n such that \(1 \le n < m\), \(c_{k_n}' = c_{k_{n+1}}\) (the intermediate components form a chain over which the information propagates);

for all n, \(1 \le n < m\), for all configurations \(e_{k'}\) such that \(k_n< k' < k_{n+1}\), \(c_{k_{n+1}} \in \mathcal {C}_{e_{k'}}\) (after an intermediate component receives the information and before it passes it on, it is not replaced by a fresh component with the same index).
If such a trace exists, we say that information may flow from a source component which satisfies the source condition given by \(P_{src},\rho _{src}\) to a destination component which satisfies the destination condition given by \(P_{dst},\rho _{dst}\).
Syntactic restrictions: \(\rho _{src}\) and \(\rho _{dst}\) are quantifierfree formulas, without index set predicates \(=\), \(\subseteq \).
4.2 Logic for Systems of Parameters
In the following, we define a manysorted firstorder logic [15]. Signatures contain no quantifier symbols except those explicitly mentioned.
Syntax. Theory \(T_{IDX} = (\varSigma _{IDX}, \mathcal C_{IDX})\) of indexes with a single sort idx (in practice, we are using the theory of integers with sort int and with standard operators).
A finite number K of theories \(T_{EL_k} = (\varSigma _{EL_k}, \mathcal C_{EL_k})\) of elements, each with a single sort \(\texttt {el} _k\) with a distinguished constant symbol \(d_{\texttt {el} _k}\) (a default value) (in practice, we consider the theory of booleans with sort bool and the theory of integers, the same as the theory \(T_{IDX}\)).
The theory \(SP^{EL_1,\ldots ,EL_K}_{IDX}\) (or simply \(SP^{EL}_{IDX}\)) of systems of parameters with indexes in \(T_{IDX}\) and elements in \(EL_1,\ldots ,EL_K\) is a combination of the above theories. Its sort symbols are idx, is, \(\texttt {el} _1,\ldots ,\texttt {el} _K\), \(\texttt {vs} _1,\ldots ,\texttt {vs} _K\), where is is a sort for index sets and \(\texttt {vs} _k\) is a sort for indexed sets of parameters of sort \(\texttt {el} _k\). The set of variable symbols for each sort \(\texttt {vs} _k\) contains a countable set of variables \(\{V^I_{k,n}\}_{n\in \mathbb {N}}\) for each variable symbol I of sort is (we omit the superscript and subscripts when they are clear from the context). The signature is the union of the signatures of the above theories, \(\varSigma _{IDX}\cup \bigcup _{k=1}^K\varSigma _{EL_k}\), with the addition of: for sort idx, quantifier symbols \(\forall \), \(\exists \), and \(\forall _I\), \(\forall _{I^C}\), \(\exists _I\), \(\exists _{I^C}\) for all variables I of the sort is; predicate symbol \(\in \) of sort \((\texttt {idx} ,\texttt {is} )\); predicate symbols \(=, \subseteq \) of sort \((\texttt {is} ,\texttt {is} )\); function symbols \(\cup , \cap , \setminus \) of sort \((\texttt {is} ,\texttt {is} ,\texttt {is} )\); for every \(n\in \mathbb N\), nary function symbol \(\{\mathord {\cdot },\ldots ,\mathord {\cdot }\}^{(n)}\) (we write simply \(\{\mathord {\cdot },\ldots ,\mathord {\cdot }\}\)) of sort \((\texttt {idx} ,\ldots ,\texttt {idx} ,\texttt {is} )\); function symbols \(\mathord {\cdot }[\mathord {\cdot }]_k,k=1,\ldots ,K\) (we write simply \(\mathord {\cdot }[\mathord {\cdot }]\)) of sorts \((\texttt {vs} _k,\texttt {idx} ,\texttt {el} _k)\).

\(\texttt {is} ^\mathcal M\) is the power set of \(\texttt {idx} ^\mathcal M\);

each \(\texttt {vs} _k^\mathcal M\) is the set of all (total and partial) functions from \(\texttt {idx} ^\mathcal {M}\) to \(\texttt {el} _k^\mathcal {M}\);

\(\in \) is interpreted as the standard set membership predicate;

\(=\), \(\subseteq \) are interpreted as the standard set equality and subset predicates;

\(\cup \), \(\cap \), \(\setminus \) are interpreted as the standard set union, intersection and difference on \(\texttt {is} ^\mathcal M\), respectively;

for every \(n\in \mathbb N\), \(\mathcal I_\mathcal M (\{\mathord {\cdot },\ldots ,\mathord {\cdot }\}^{(n)})\) is the function that maps the ntuple of its arguments to the set of indexes containing exactly the arguments, i.e. it maps every \((x_1,\ldots ,x_n) \in (\texttt {idx} ^\mathcal M)^n\) to \(\{x_1,\ldots ,x_n\} \in \texttt {is} ^\mathcal M\);

\(\mathord {\cdot }[\mathord {\cdot }]_k, k=1,\ldots ,K\) are interpreted as function applications: Open image in new window .
The structure \(\mathcal {M}\) is a model of Open image in new window iff it satisfies the above restrictions and Open image in new window , Open image in new window are models of Open image in new window , \(T_{EL_1}, \ldots ,T_{EL_K}\), respectively.
Definition 9
A formula (resp. term) over a system of parameters \((\mathcal I, \mathcal V)\) is a formula (resp. term) of the logic \(SP^{EL}_{IDX}\) in which the only occurring symbols of sort idx are from \(\mathcal I\) and the only occurring symbols of sort \(\texttt {vs} _k\) are from the set \(\{V \in \mathcal V: \texttt {sort} _V = \texttt {el} _k\}\), for \(k=1,\ldots ,K\). Furthermore, in the formula all accesses \(V[\mathord {\cdot }]\) to parameters \(V\in \mathcal V\) are guarded parameter accesses, i.e. each atom \(\alpha (V[t])\) that contains a term of the form V[t] must occur in conjunction with a guard which ensures that index term t is present in the corresponding index set: \(t\in I_V\wedge \alpha (V[t])\).
Definition 10
A transition formula over the system of parameters \((\mathcal I, \mathcal V)\) is a formula of the logic \(SP^{EL}_{IDX}\) in which the only occurring symbols of sort idx are from \(\mathcal I \cup \mathcal I'\) and the only occurring symbols of sort \(\texttt {vs} _k\) are from the set \(\{W \in \mathcal V\cup \mathcal V': \texttt {sort} _W = \texttt {el} _k\}\), for \(k=1,\ldots ,K\). Furthermore, all accesses \(W[\mathord {\cdot }]\) to parameters \(W\in \mathcal V\cup \mathcal V'\) are guarded parameter accesses (as defined in Definition 9).
The subscripted quantifier symbols are a syntactic sugar for quantification over index sets and their complements: all occurrences of the quantifiers \(\forall _I i\ \phi \), \(\forall _{I^C} i\ \phi \), \(\exists _I i\ \phi \), \(\exists _{I^C} i\ \phi \)—where I is a variable of sort is, i is a variable of sort idx, and \(\phi \) is a formula—are rewritten to \(\forall i\ (i \in I \rightarrow \phi )\), \(\forall i\ (i \not \in I \rightarrow \phi )\), \(\exists i\ (i \in I \wedge \phi )\), \(\exists i\ (i \not \in I \wedge \phi )\), respectively, after which the formula is evaluated in the standard manner.
Definition 11
Evaluation \(\llbracket \phi \rrbracket _\mu \) with respect to an assignment \(\mu \) to a system of parameters \((\mathcal I, \mathcal V)\), of a formula (or a term) \(\phi \) over \((\mathcal I, \mathcal V)\) is defined by interpreting I with \(I^\mathcal M = \mu _\mathcal I(I)\) for every \(I \in \mathcal I\) and interpreting V[x] as follows for every \(V \in \mathcal {V}\): \((V[x])^\mathcal {M} = \mu _V(x^\mathcal {M})\) if \(x^\mathcal {M} \in \mu (I_V)\), and \((V[x])^\mathcal {M} = d_{\texttt {sort} _V}^\mathcal M\) otherwise. The evaluation \(\llbracket \phi \rrbracket _{\mu \mu '}\) of a transition formula with respect to two assignments \(\mu \), \(\mu '\) is defined by interpreting, in the above manner, \((\mathcal {I},\mathcal {V})\) with \(\mu \) and \((\mathcal {I}',\mathcal {V}')\) with \(\mu '\).
5 Analysis with SMTBased Model Checking
5.1 Background Notions on SMTBased Model Checking
Manysorted firstorder logic of arrays. The target logic for the translation is the manysorted firstorder logic [15] with theories for indexes, elements and arrays as defined in [18]. Following that paper, we fix a theory \(T_I = (\varSigma _I, \mathcal C_I)\) for indexes whose only sort symbol is index and we fix theories \(T_{E_k} = (\varSigma _{E_k}, \mathcal C_{E_k}), k = 1, \ldots , K\) whose only sort symbols are \(\texttt {elem} _k\), respectively. The theory \(A_I^{E_1, \ldots , E_{K}}\) (or simply \(A_I^E\)) of arrays with indexes in \(T_I\) and elements in \(E_1,\ldots ,E_K\) is defined as the combination of theories \(T_I, T_{E_1}, \ldots , T_{E_K}\) as follows. The sort symbols of \(A_I^E\) are \(\texttt {index} \), \(\texttt {elem} _1, \ldots , \texttt {elem} _K\), \(\texttt {array} _1,\ldots ,\texttt {array} _K\), the signature is \(\varSigma := \varSigma _I \cup \bigcup _{k=1}^K \varSigma _{E_i} \cup \bigcup _{k=1}^K \{\mathord {\cdot }[\mathord {\cdot }]_k\}\) where \(\mathord {\cdot }[\mathord {\cdot }]_k\) are function symbols of sorts \((\texttt {array} _k, \texttt {index} , \texttt {elem} _k)\). A structure \(\mathcal M = (\texttt {index} ^\mathcal M, \texttt {elem} _1^\mathcal M, \ldots , \texttt {elem} _K^\mathcal M, \texttt {array} _1^\mathcal M,\ldots , \texttt {array} _K^\mathcal M, \mathcal {I})\) is a model of \(A_I^E\) iff \(\texttt {array} _k^\mathcal {M}\) are sets of all functions from \(\texttt {index} ^\mathcal M\) to \(\texttt {elem} _k^\mathcal {M}\), respectively, the function symbols \(\mathord {\cdot }[\mathord {\cdot }]_k\) are interpreted as function applications, and Open image in new window , Open image in new window are models of \(T_{I}\), \(T_{E_k},k=1,\ldots ,K\), respectively.
ArrayBased Transition Systems. In the following, i, j denote variables of the sort index, \(\underline{i}\) denotes a set of such variables, a denotes a variable of one of the \(\texttt {array} \) sorts, \(\underline{a}\) denotes a set of such variables, notation \(\underline{a}[\underline{i}]\) denotes the set of terms \(\{a[i]: a \in \underline{a}, i \in \underline{i}\}\), and \(\phi (x), \psi (x)\) denote quantifier free \(\varSigma (x)\) formulas.

\(\underline{a} = \{a_1, \ldots , a_n\}\) is a set of state variables of the sorts \(\texttt {array} _1, \ldots , \texttt {array} _K\).
 \(Init(\underline{a})\) is the initial \(\varSigma (\underline{a})\)formula of the form$$\begin{aligned} \forall \underline{i}.\phi (\underline{i}, \underline{a}[\underline{i}]). \end{aligned}$$(1)
 \(Tr(\underline{a}, \underline{a}')\) is the transition \(\varSigma (\underline{a}, \underline{a}')\)formula and is a disjunction of formulas of the form$$\begin{aligned} \exists \underline{i}\left( \psi (\underline{i}, \underline{a}[\underline{i}]) \wedge \bigwedge _{k=1}^n \forall j\ a_k'[j] = t_k(\underline{i}, \underline{a}[\underline{i}], j, \underline{a}[j])\right) \end{aligned}$$(2)
Decidability of the ArrayBased Safety Problem. The arraybased safety problem is in general undecidable (Thm. 4.1. in [18]), but it becomes decidable under 1) the following assumptions on the theory \(T_I\) of indexes: local finiteness, closedness under substructures, decidability of SMT(\(T_I\)), 2) assumptions of local finiteness of \(T_E\) and of decidability of SMT(\(T_E\)), and 3) further assumptions on the arraybased transition system under analysis (for details see Theorem 3.3. and Theorem 4.6. in [18]).
5.2 Encoding into SMTBased Model Checking
Translation of Formulas. We recursively define the translation \(\mathord {\cdot }^\mathcal A\) of formulas and transition formulas of \(SP_{IDX}^{EL}\) to formulas of \(A_I^E\). We set the index and element sorts to correspond, i.e. \(\texttt {index} :=\texttt {idx} \) and \(\texttt {elem} _k := \texttt {el} _k, k=1,\ldots ,K\). In practice, we set \(T_I\) to be the theory of integers (with sort \(\texttt {index} =\texttt {int} \)), number of element theories to \(K = 2\), and we set \(E_1 = T_I\) and \(E_2\) to be the theory of Booleans (with sort \(\texttt {elem} _2 = \texttt {bool} \)).

Symbols of the sorts idx and \(\texttt {el} _k,k=1,\ldots ,K\) are treated as symbols of the sorts index, \(\texttt {elem} _k,k=1,\ldots ,K\), respectively.

For a variable I of sort is, \(I^\mathcal A:=a_I\), where \(a_I\) is of the sort \(\texttt {array} _\texttt {bool} \).

For a variable V of sort \(\texttt {vs} _k\), \(V^\mathcal A:=a_V\), where \(a_V\) is of the sort \(\texttt {array} _{\texttt {elem} _k}\).

For a term t of sort idx and term T of sort is, \((t\in T)^\mathcal A:=T^{\mathcal A_t}\).

For terms \(T_1,T_2\) of sort is, \((T_1\cap T_2)^{\mathcal A_t}:=T_1^{\mathcal A_t}\wedge T_2^{\mathcal A_t}\); analogously for \(\cup \) and \(\setminus \).

For a variable I of sort is, \(I^{\mathcal A_t}:=I^\mathcal A[t^\mathcal A]\).

\((\{e_1,\ldots ,e_n\})^{\mathcal A_t}:= \bigvee _{k=1}^n \left( t^\mathcal A=e_k^{\mathcal A}\right) \).

For terms \(T_1,T_2\) of sort is, \((T_1=T_2)^\mathcal A:=\forall i\ (T_1^{\mathcal A_i}= T_2^{\mathcal A_i})\), where i is a fresh variable of sort idx; analogously for \(\subseteq \) which is translated using \(\rightarrow \).

For a variable V of sort \(\texttt {vs} _k\) and a term t of sort idx, \((V[t])^\mathcal A := V^\mathcal A[t^\mathcal A]\).

Other logical connectives, quantifiers and operators are present in both logics and are translated directly, e.g. \((e_1 \le e_2)^\mathcal A:=e_1^\mathcal A \le e_2^\mathcal A\) and \((\phi _1 \wedge \phi _2)^\mathcal A := \phi _1^\mathcal A \wedge \phi _2^\mathcal A\).

\(\tau _k^{=}:=\exists _{\underline{I}_1}\underline{i}_1 \exists _{\underline{I}_2^C} \underline{i}_2 \left( \alpha _k^=\wedge \beta _k^=\wedge \gamma _{\beta _k^=}\right) \) where \(\alpha _k^=:=\alpha _k\wedge (t_1=t_2)\wedge (e_1=e_2)\), and \(\beta _k^=\) is obtained from \(\beta _k\) by removing the conjunct \(V'[t_2] = e_2\);

\(\tau _k^{\ne }:=\exists _{\underline{I}_1}\underline{i}_1 \exists _{\underline{I}_2^C} \underline{i}_2 \left( \alpha _k^{\ne }\wedge \beta _k\wedge \gamma _{\beta _k}\right) \) where \(\alpha _k^{\ne }:=\alpha _k\wedge (t_1\ne t_2)\).
It is easy to verify that the formulas \(\tau _k\) and \(\tau _k^{=}\vee \tau _k^{\ne }\) are equivalent. By continuing the rewriting recursively, \(\tau \) can be transformed into a disjunction of formulas with differentiated accesses to primed parameters.
For a symbol \(I'\in \mathcal I'\), there is exactly one conjunct in \(\tau _k\) in which \(I'\) appears in the equality, and it is one of \(I' = I \cup \{t_k\}_k\), \(I' = I \setminus \{t_k\}_k\), or \(I' = I\). In all three cases, value of \(I'\) is a function of the value of I and some terms over \((\mathcal I, \mathcal V)\), and therefore the conjunct can be rewritten as \(\forall j\left( j \in I'\leftrightarrow Update_I(j)\right) \) where \(Update_I\) is a term of sort bool over \((\mathcal I, \mathcal V)\) and a free variable. For example, for the first case we have \(Update_I(j) = (j \in I\vee \bigvee _k (j=t_k))\). The conjuncts in \(\tau _k\) of the form \(t\in I'\) can be rewritten as \(Update_I(t)\). From \(\tau _k\) we obtain \(\tau '_k\) by performing the above rewriting of conjuncts which contain \(I'\), for all \(I'\in \mathcal I'\). It is easy to verify that \(\tau '_k\) and \(\tau _k\) are equivalent formulas.
The following theorems state that the information flow problem can be reduced to the arraybased safety problem, using the above translation. The detailed proofs can be found in the extended version of the paper at https://es.fbk.eu/people/stojic/papers/fm18.
Theorem 1
Problem \((\mathcal S,U)\), \(\mathcal S=(\underline{a},Init,Tr)\), which is obtained by translation from an arbitrary information flow problem, where \(\underline{a}\) is given by (4), Init is given by (5), Tr is given by (6), (7), (8), and U is given by (9), is an arraybased safety problem.
The proof amounts to the inspection of the obtained formulas, to confirm that they are indeed in the required fragment.
Theorem 2
Let \(DIFP=(D,P_{src},\rho _{src},P_{dst},\rho _{dst})\) be an arbitrary instance of the dynamic information flow problem, and \(ASP=(\mathcal S, U)\) the arraybased safety problem obtained by translation from DIFP. There is an information flow witness trace for DIFP if and only if ASP is unsafe.
The proof involves constructing, for an information flow witness trace for DIFP, a counterexample (unsafe) trace of the problem ASP, and viceversa.
Decidability. The dynamic information flow problem is undecidable in general (it is straightforward to model Minsky 2counter machines [28]), but it is decidable under certain assumptions inherited from the arraybased transition systems (see the remark on decidability at the end of Sect. 5.1).
6 Experimental Evaluation
6.1 Setup
BackEnd Solver. We use MCMT [4] version 2.5.2 to solve arraybased safety problems. MCMT is a model checker for arraybased systems, based on the SMT solver Yices^{1}. We run MCMT with the default settings. The timeout for testing is set to 1000 seconds.

The initial formula can contain at most two universally quantified variables.

The transitions can contain at most two existentially quantified variables.

The maximum number of transitions (the disjuncts in the transition formula) is 50.

The unsafe formula can contain at most four existentially quantified variables.

A term can contain at most ten index variables.
Our translator inherits the above restrictions on the formulas specified in the extended AADL model. While these restrictions do not severely limit the expressivity of the language, the limitation on the maximum number of transitions limits the size of the examples that can be handled by the present version of the tool.
Hardware. We have used a desktop PC based on an Intel^{®} Core™ i7 CPU 870 clocked at 2.93GHz, with 8 GB of main memory and running Ubuntu 14.04.5 LTS.
Distribution Tarball. The translator, tested models, scripts which automatically perform the translation from extended AADL to MCMT input language and run MCMT, as well as setup and usage instructions can be found at https://es.fbk.eu/people/stojic/papers/fm18/.
6.2 Benchmarks and Results
In the following diagrams, arrows between (sets of) components represent connections from all components in the source set to all components in the destination set, unless further restricted in the model description. All sets of components are dynamic, allowing addition/removal of components.
Messenger Model. In this model, for \(n=1\) there are two sets of components, a and b, and a singleton component \(m_0\). \(m_0\) models a messenger which is intended to allow components within the same set to communicate; \(m_0\) can connect in turn to any single component in a or in b, but not at the same time. We test for information flow from set a to set b. The system as described is unsafe because \(m_0\) can connect to some a[i], disconnect, and then connect to some b[j], therefore establishing a path for flow of information. The safe model removes such paths by using Boolean parameters to record whether \(m_0\) has previously connected to components in a and b. If it has previously connected to one of these sets, then it is not allowed to connect to the other set before it is scrubbed (which is modeled by removing and readding it). For \(n=2\) (Fig. 4), the system is extended with another set of components c and another messenger \(m_1\) which is shared by b and c, and we check for information flow between a and c. Results are shown in Fig. 5.
Network Model. This is the model whose safe version is specified in Fig. 2, while the highlighted parts are omitted in the unsafe version. Results are shown in Fig. 5.
7 Conclusions and Future Work
We propose a new logicbased specification of dynamic architectures where the architectural topology is represented by a set of parameters, while firstorder formulas over such parameters define the sets of initial configurations and reconfigurations. The Dynamic Parametrized Architectures so defined can be translated into arraybased transition systems, which are amenable to SMTbased model checking. We provide an initial experimental evaluation of various DPAs proving safe and unsafe cases with the MCMT model checker. The results show that the approach is feasible and promising.
As future work, we aim at trying other SMTbased model checkers such as Cubicle [13] and nuXmv [11]. We will investigate new algorithms that directly exploit the topology of the architecture. We will extend the specification to incorporate component behavior and more complex interactions, as well as more general properties. Finally, we are interested in generating certifying proofs for the safe DPAs, possibly exploiting the existing automatic generation of proofs for arraybased transition systems [14].
Footnotes
References
 1.European Programme for Critical Infrastructure Protection (EPCIP). http://eurlex.europa.eu/LexUriServ/LexUriServ.do?uri=COM:2006:0786:FIN:EN:PDF. Accessed 15 Jan 2018
 2.NIST Cybersecurity Framework. http://www.nist.gov/cyberframework. Accessed 15 Jan 2018
 3.The CITADEL Project (Critical Infrastructure Protection using Adaptive MILS). http://www.citadelproject.org/. Accessed 15 Jan 2018
 4.Alberti, F., Ghilardi, S., Sharygina, N.: A framework for the verification of parameterized infinitestate systems. In: CEUR Workshop Proceedings, vol. 1195, pp. 302–308 (2014)Google Scholar
 5.Allen, R., Douence, R., Garlan, D.: Specifying and analyzing dynamic software architectures. In: Astesiano, E. (ed.) FASE 1998. LNCS, vol. 1382, pp. 21–37. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0053581CrossRefGoogle Scholar
 6.Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous realtime components in BIP. In: Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006), Pune, India, pp. 3–12, 11–15 September 2006Google Scholar
 7.Bozga, M., Jaber, M., Maris, N., Sifakis, J.: Modeling dynamic architectures using DyBIP. In: Gschwind, T., De Paoli, F., Gruhn, V., Book, M. (eds.) SC 2012. LNCS, vol. 7306, pp. 1–16. Springer, Heidelberg (2012). https://doi.org/10.1007/9783642305641_1CrossRefGoogle Scholar
 8.Bradbury, J.S., Cordy, J.R., Dingel, J., Wermelinger, M.: A survey of selfmanagement in dynamic software architecture specifications. In: Proceedings of the 1st ACM SIGSOFT Workshop on SelfManaged Systems WOSS 2004, Newport Beach, California, USA, pp. 28–33, 31 October  1 November 2004Google Scholar
 9.Bruni, R., Melgratti, H., Montanari, U.: Behaviour, interaction and dynamics. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software. LNCS, vol. 8373, pp. 382–401. Springer, Heidelberg (2014). https://doi.org/10.1007/9783642546242_19CrossRefMATHGoogle Scholar
 10.Canal, C., Pimentel, E., Troya, J.M.: Specification and refinement of dynamic software architectures. In: Donohoe, P. (ed.) Software Architecture. ITIFIP, vol. 12, pp. 107–125. Springer, Boston, MA (1999). https://doi.org/10.1007/9780387355634_7CrossRefGoogle Scholar
 11.Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334–342. Springer, Cham (2014). https://doi.org/10.1007/9783319088679_22CrossRefGoogle Scholar
 12.CITADEL Modeling and Specification Languages. Technical report D3.1, Version 2.2, CITADEL Project, April 2018Google Scholar
 13.Conchon, S., Goel, A., Krstić, S., Mebsout, A., Zaïdi, F.: Cubicle: a parallel SMTbased model checker for parameterized systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 718–724. Springer, Heidelberg (2012). https://doi.org/10.1007/9783642314247_55CrossRefGoogle Scholar
 14.Conchon, S., Mebsout, A., Zaïdi, F.: Certificates for parameterized model checking. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 126–142. Springer, Cham (2015). https://doi.org/10.1007/9783319192499_9CrossRefGoogle Scholar
 15.Enderton, H.B.: A Mathematical Introduction to Logic, 2nd edn. Academic Press, Boston (2001)MATHGoogle Scholar
 16.Feiler, P.H., Gluch, D.P.: ModelBased Engineering with AADL  An Introduction to the SAE Architecture Analysis and Design Language. AddisonWesley, SEI series in software engineering (2012)Google Scholar
 17.Ghilardi, S.: MCMT v2.5  User Manual (2014). http://users.mat.unimi.it/users/ghilardi/mcmt/UM_MCMT_2.5.pdf. Accessed 15 Jan 2018
 18.Ghilardi, S., Ranise, S.: Backward reachability of arraybased systems by SMT solving: termination and invariant synthesis. Log. Meth. Comput. Sci. 6(4), 1–48 (2010)MathSciNetCrossRefGoogle Scholar
 19.Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 22–29. Springer, Heidelberg (2010). https://doi.org/10.1007/9783642142031_3CrossRefGoogle Scholar
 20.Goguen, J.A., Meseguer, J.: Security policies and security models. In: 1982 IEEE Symposium on Security and Privacy, Oakland, CA, USA, pp. 11–20, 26–28 April 1982Google Scholar
 21.Hirsch, D., Inverardi, P., Montanari, U.: Reconfiguration of software architecture styles with name mobility. In: Porto, A., Roman, G.C. (eds.) COORDINATION 2000. LNCS, vol. 1906, pp. 148–163. Springer, Heidelberg (2000). https://doi.org/10.1007/354045263X_10CrossRefGoogle Scholar
 22.König, B., Kozioura, V.: Towards the verification of attributed graph transformation systems. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 305–320. Springer, Heidelberg (2008). https://doi.org/10.1007/9783540874058_21CrossRefMATHGoogle Scholar
 23.Konnov, I.V., Kotek, T., Wang, Q., Veith, H., Bliudze, S., Sifakis, J.: Parameterized systems in BIP: design and model checking. In: 27th International Conference on Concurrency Theory CONCUR 2016, Québec City, Canada, pp. 30:1–30:16, 23–26 August 2016Google Scholar
 24.Magee, J., Kramer, J.: Dynamic structure in software architectures. In: SIGSOFT 1996 Proceedings of the Fourth ACM SIGSOFT Symposium on Foundations of Software Engineering, San Francisco, California, USA, pp. 3–14, 16–18 October 1996Google Scholar
 25.Medvidovic, N., Taylor, R.N.: A classification and comparison framework for software architecture description languages. IEEE Trans. Softw. Eng. 26(1), 70–93 (2000)CrossRefGoogle Scholar
 26.Métayer, D.L.: Describing software architecture styles using graph grammars. IEEE Trans. Softw. Eng. 24(7), 521–533 (1998)CrossRefGoogle Scholar
 27.Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes I and II. Inf. Comput. 100(1), 1–77 (1992)MathSciNetCrossRefGoogle Scholar
 28.Minsky, M.L.: Computation: Finite and Infinite Machines. PrenticeHall Inc, Upper Saddle River (1967)MATHGoogle Scholar
 29.Rozenberg, G. (ed.): Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations. World Scientific, Singapore (1997)MATHGoogle Scholar
 30.Architecture Analysis & Design Language (AADL) (rev. B). SAE Standard AS5506B, International Society of Automotive Engineers, September 2012Google Scholar
 31.Sifakis, J., Bensalem, S., Bliudze, S., Bozga, M.: A theory agenda for componentbased design. In: De Nicola, R., Hennicker, R. (eds.) Software, Services, and Systems. LNCS, vol. 8950, pp. 409–439. Springer, Cham (2015). https://doi.org/10.1007/9783319155456_24CrossRefGoogle Scholar
 32.Wermelinger, M., Fiadeiro, J.L.: Algebraic software architecture reconfiguration. In: Nierstrasz, O., Lemoine, M. (eds.) ESEC/SIGSOFT FSE 1999. LNCS, vol. 1687, pp. 393–409. Springer, Heidelberg (1999). https://doi.org/10.1007/3540481664_24CrossRefGoogle Scholar
 33.Xu, H., Zeng, G., Chen, B.: Description and verification of dynamic software architectures for distributed systems. JSW 5(7), 721–728 (2010)CrossRefGoogle Scholar
Copyright information
<SimplePara><Emphasis Type="Bold">Open Access</Emphasis> This chapter is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, duplication, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, a link is provided to the Creative Commons license and any changes made are indicated.</SimplePara> <SimplePara>The images or other third party material in this chapter are included in the work's Creative Commons license, unless indicated otherwise in the credit line; if such material is not included in the work's Creative Commons license and the respective action is not permitted by statutory regulation, users will need to obtain permission from the license holder to duplicate, adapt or reproduce the material.</SimplePara>