The scope of this paper is collaborative, distributed safety critical systems which build up a larger scale system of systems (SoS). Systems in this context are independently designed and can operate autonomously following both global SoS goals and individual goals. A major aspect of SoSs is the evolution over time, i.e. the change of its architecture as a result of changes in the context of the SoS or the changes of individual or global goals. The aim of this paper is to define a modeling concept for evolution specifying all possible changes of the SoS over time. This evolution model is used to generate and analyze future architectures enabling the prediction of future violations of static specifications. We derive so called dynamicity contracts and restrict the evolution model in such a manner, that false architectures are not reached.
SoS. The main characteristic we are interest in is the evolutionary development,
i.e. the change of the architecture of an SoS during its lifetime. A model for the
evolutionary development can be created based on prognosis on possible future
evolutions of the SoS. As an example, statistical data could be used to do a
prognosis on the future traffic density in a district of a city. We propose graph
grammars to model the possible evolutions of an SoS. These transformations
could also be specified via temporal logics as we proposed in [
Graph grammars describe the adaption to a context change in form of
transformation rules. With these transformation rules the inter-connections of the
constituent systems and thereby their roles and interaction protocols are changed.
The trigger of such transformation rules are the constituent systems itself: When
systems adapt or change their local goals and thus affect their local behavior,
change their services offered to the environment, or need some services from their
local environment, a request to change some parts of the SoS architecture are
triggered from the corresponding constituent systems. In [
Besides the evolution model, we will consider static specifications of SoSs by
contracts defining invariants and constraints on the architecture of the SoS. An
example for a static contract is that systems applying inconsistent roles should
not co-operate. The set of static contracts of an SoS defines all legal
architectures of this SoS. Beginning with an initial SoS architecture, the evolution model
successively generates a set of successor architectures. Transformations are
applied locally resulting in sequences of transformations which could lead to an
architecture violating the static contracts. In this paper, we derive so called
dynamicity contracts which restrict the dynamics of the evolution model of the SoS
to prevent the SoS entering an architecture which violates its static specification.
We extend this approach by tolerating a finite set of intermediate architectures,
which violate the static specifications. These intermediate architectures have to
be left finally and a safe architecture has to be reached within a specified
number of changes. The idea to allow temporarily intermediate faulty architectures
is inspired by the fault tolerance time intervals defined in the ISO 26262 [
To model the static architecural part of an SoS we use the UPDM framework
[
In [
Automatic verification of the real-time behavior including the reconfiguration
is supported by CHARON [
The following section introduces the fundamentals of our work, i.e. the considered modeling formalism called UPDM, the contract-based specification formalism, and the formalisms needed to express transformations. Section 3 illustrates our approach to derivate dynamicity contracts in order to prevent the SoS to evolve in architectures which violate its static specification. In Section 4 we illustrate our implementation and give some example scenarios. Finally, Section 5 concludes the paper and discusses some further work. 2
The basic modeling elements of our approach are components as structural elements, and graph grammars. Our components are enriched by so called contracts, specifying the allowed context of a component and its guaranteed behaviour. Components and contracts are detailed in the following section. 2.1
We use Heterogenous Rich Components (HRCs) [
Having a formal specification for the component and its sub-components the
so called Virtual Integration Test (VIT) [
An architecture of an SoS is a composition of CSs at a specific time, where roles and inter-connections of all systems are specified. Changes of an architecture of the SoS are defined by a set of rewriting rules. Rewriting rules consist of a left hand side and a right hand side corresponding to architectures of the SoS. In this work, rewriting rules restructure the architecture of an SoS by composing or separating system instances in a well-defined way, and applying the right roles to the corresponding systems. So, a single transformation affects a subset of participating system instances, their inter-connections, roles, and modes. In the following, we will formalize the concept of graphs and rewriting rules.
A graph is defined as a tuple G = (V; E; s; t) where V is a set of vertices, E is a set of edges and s; t are a source and a target function defined as fs; tg : E ! V: Let L; R be two graphs. A rewriting rule r : L ! R is defined in such a way, that whenever an instance of L, called match, is found in a graph G, this instance can be replaced through an instance of R leading to the transformed graph G0: For two graphs H; G let h : H ! G be a graph homomorphism, mapping nodes and edges of H to G: The homomorphism consists of two functions hV : VH ! VG and hE : EH ! EG; such that G hE = hV H ; with = fs; tg: A rule r : L ! R can be applied to a graph G leading to a changed graph G0; in short d : G !r G0; if there exist two homomorphisms h1; h2; such that h1 : L ! G and h2 : R ! G0: In Section 3 we will apply a set of rewriting rules specifying the dynamic behaviour of an SoS. 2.3
System of systems (SoS) consist of several constituent systems (CS) which are
instances of systems or even SoSs themselves. To distinguish between complex
systems and SoSs Maier proposed five criteria for the "SoS-ness" of a complex
system, which are introduced in the following [
System dynamics are covered by the UML/SysML behavioral models and diagrams, e.g. state charts. We use contracts to specify the assumed and guaranteed behavior of each CS.
We address the evolutionary development and extend the milestone-based representation of SoSs in UPDM. A milestone represents an architecture of the SoS at a specific point in time. We will focus on the system view which basically represents systems itself, their resource roles and inter-connections. The SV-1 allows to characterize the inter-connections of the CSs for a single architecture. The milestone plan (AV-2) is the planed evolution of the SoS taking the entire life-cycle of the CS into account. This plan is created manually and explicitly since each milestone consists of an entire SoS architecture.
The problem we address is that the owners or managers of the CSs follow their own goals, and change or influence changes of their CSs independently from a central authority. We define goal as an optimization metric which represents how good (or bad) a CS (or an SoS) performs. These values can be statically computed for an architecture of the SoS, or depend on the system dynamics and are measured during execution. The owners of a CS are assumed to monitor this values and decide to change the behavior or connectivity of their CS to improve their goals. This change might take place on the CS level by switching into another mode or on the SoS level by changing the inter-connections to other CSs. In the first case this behavior is part of the CS specification and covered by the contracts of the CS. In the second case the change is beyond the system borders of the CS and therefore not in the scope of the specification of the system dynamics. The evolution behavior of the SoS is based on changes which might impact the dynamics of the SoS. 3
A model for an SoS consists of an initial architecture, a static specification and
an evolution behaviour. As said before, evolution behaviors define the possibility
of re-configuring a given architecture as a result of e. g. changing
environmental conditions, or some adaption of cooperations between a set of systems. We
will apply graph grammars to model such a behaviour. The benefit of the usage
of evolution models is the possibility to generate and analyze future
architectures enabling the prediction of future violations of specifications. Changes of a
given SoS can be explored before they occur in reality in order to prevent
invalid architectures of the SoS. Typically an infinite number of architectures will
be generated by graph grammars. In our concept, we will apply the concept of
bounded model-checking, i.e. we will only consider a finite number of
architectures reached by a grammar specification. This also has a practical relevance,
as in general the evolution model shall only predict the possible behaviour for a
finite time frame instead of an infinite time frame. To obtain a finite set of
architectures, we could apply abstraction techniques like the Partner Abstraction
introduced in [
G0 r0,...,rn,rm,rk
Gh r0,...,rk r0,...,rn
Gk Gn ...
Gn rm rj Gn+3 ... Gm+2
G0 rk
... rj ..
r0,...,rk r0,...,rn
Gh
Gk Gn
...
r0,...,rn,rm,rk cnew: (A: Gn+1 /\ (r0,...,rm) , G: !rk)
...
Gn+1 rm rj Gn+3 rj . .
The concept of dynamicity contracts complements the static contracts for the SoS and constituent systems. The static contracts restrict the allowed behaviour of the overall SoS and each system, whereas the dynamicity contracts restrict the dynamics of the evolution model of the SoS.
Starting from an initial architecture each reached architecture is analyzed if it is valid. If invalid architectures are reached, a dynamicity contract is derived in such a way, that the evolution model is prevented to generate this architecture. Thereby, the assumption part of a dynamicity contract encapsulates the architecture, from which a violating one can be reached by the application of a rule defined in the evolution model. The guarantee part then consists of the negation of the corresponding identifier of the rule. Further, we extend this approach by allowing intermediate architectures, which violate the static specifications, if a valid architecture is reached after “some time”. In this work, we require that a specified number of successive invalid architectures may be tolerated, and after this number a valid architecture has to be reached. In future work, we will extend this approach by specifying some allowed time frames.
Consider the example of Figure 1, where the initial architecture G0 can evolve to different future architectures by applying an evolution model consisting of a set of rewriting rules r: Assume that we allow that during the evolution maximal a single architecture may be reached which violates the static contracts. On the left part of the figure the initial situation is depicted, where no restrictions exist so far for our evolution model. If the sequence of rules r0; :::rn; rm is applied, we can reach the architecture Gn+1 which violates the static specification. If we would now apply rule rk we would again get an architecture violating the static specification. In order to restrict our evolution model we derive the contract illustrated in the right part of Figure 1. The contract states, that whenever we are in an architecture isomorph to Gn+1 and we previously applied the sequence of rules r0; :::; rm; the rule rk will not be applied. Note, that we need the architecture within the assumption part, as rewriting rules are non-deterministic. The sequence of rules r0; :::; rm can also lead to some architectures not violating the static contracts as illustrated in Figure 1.
Next, we define our applied graph grammar formalism, and formalize the derivation of dynamicity contracts.
Graph Grammars Let w = r0; :::; rn; ::: be a word over an alphabet ; pre(w; n) = r0; :::; rn be its prefix consisting of n+1 symbols, and w(n) = rn 2 the (n + 1) th symbol. A dynamicity contract is a contract talking about graphs and prefixed of words: The assumption (A) part of a dynamicity contract c consists of a (possibly empty) finite prefix of a word w and a graph G; its guarantee (G) consists of a symbol in ; in short c : (A : pre(w; i 1) ^ Gi; G: ! ) for some i 2 N with 2 : The intuition is that whenever a finite sequence of symbols pre(w; i 1) is received and the graph Gi is reached, the next symbol shall not be : With these dynamicity contracts we will restrict graph grammars in such a way, that through the successive application of rules it always holds, that no graph can be reached violating some static specifications.
A graph grammar is a tuple G = (G0; R; CD) where G0 is a start graph, R = fr0; :::; rkg is the set of rewriting rules (each with an unique identifier), and CD is the set of dynamicity contracts, which may be empty at design time. In the next section we detail the iterative extension of this set. A graph grammar can be translated to a finite ! automaton TE = (S; so; ; !); where S is a set of graphs corresponding to the set of states, s0 the initial state, an alphabet consisting of the identifiers of the rules in R, and ! S S the transition relation. All states are considered to be accepting ones.
A run of TE over an infinite word w = r0; :::; rn; ::: is an infinite sequence of graphs G0 !r0 ::: !rn Gn; !rn+1 ::: such that G0 is the initial graph and (Gi; ri; Gi+1) 2! for all i; j 2 N; for which holds that (A : pre(w; i 1) ^ Gi; G : !w(i)) 2= CD: The language of a graph grammar is defined as the set of words accepted by its finite automaton.
Derivation of Dynamicity Contracts A specification for an SoS is given by the tuple SoS = (G; Cs) where G is a graph grammar specifying the evolution model, and Cs a set of static contracts defining the allowed SoS behaviour. In general, the evolution model specified through the concept of graph grammars is not initially consistent with the static specification specified as a set of contracts, as rewriting rules are applied locally resulting in sequences of rules which could lead to a graph violating the static contracts. This can happen because the application of a rule does not check whether the reached graph harms a static contract. In order to make the evolution model consistent with respect to the contract specification, such paths have to be removed from the evolution model. For this we derive new dynamicity contracts from these paths.
The easiest case is given, when a direct application of a rule violates a static contract and no intermediate architectures violating contracts are allowed. For such cases we can derive a dynamicity contract consisting of the current architecture G as the assumption part, and the negation of the identifier of the corresponding rule for the guarantee part. That is, we extend our dynamicity contract set CD of G with the contract f(A : G; G : )g; if there exists a rule : L ! R in G; and G ! G0 could be applied, such that G0 6j= Cs:
With this extension the graph grammar will be prevented by firing rule when an isomorphic graph to G is present. If violating graphs are accepted temporarily, e.g. a finite amount of time, or a finite number of violating graphs, we need to extend such dynamicity contracts with the history which lead to a corresponding architecture. In this work, we will only consider the maximal successive number of incorrect intermediate architectures, i.e. architectures violating the static specification.
Let 2 N be the maximal number of successive graphs violating the static specification, which is defined to be tolerable. Let pre(w; n) = r0; :::; rn be a prefix of a word, for which there exists a run = G0 !r0 ::: !ri Gi::: !rn Gn of the automaton of G; such that Gi; :::; Gn 6j= Cs and jfGi; :::; Gngj > : Then we derive the following dynamicity contract and extend the set CD as follows: CD [ f(A : Gn 1 ^ pre(w; n 1); G : !w(n))g: (1) Note that a word w could result in a set of runs instead a single run. In this case our new dynamicity contracts are correct in the sense, that no legal evolutions resulting in graphs which all fulfill the static contracts are excluded. This is because the assumption part exactly states, that a rule shall not be applied if a specific architecture is given. 4
To illustrate our approach we consider an emergency response scenario, consisting of a set of constituent systems like fire stations and fire brigades. All CSs participating in this SoS shall behave cooperative in order to minimize the needed time for an operation in case of an emergency.
We use a new custom diagram via an additional profile which allows to model
rewriting rules graphically in IBM Rational Rhapsody c . These diagrams allow
to add placeholders which refer to model elements of the Rhapsody UPDM
model. This reference mechanism ensures that the model itself and the rewriting
rules are clearly separated. The rules contain four different kinds of graphical
elements for each CSs and their inter-connections, i.e. Reader, Creator, Eraser
and Embargo. Reader elements are unchanged elements of a corresponding rule.
Creator elements represent newly generated elements on the right hand side of
the rule. Eraser elements address elements of the left hand side which are
removed via the rule application. Embargo elements restrict the applicability of
the rule if the match can be extended by these elements. The Rhapsody model
including its rules are exported to GXL[
In the left part of Figure 4 a network of reachable architectures is illustrated. In the right part of Figure 4 a (simplified) network of architectures is presented. For this network the invalid architectures are marked in red. From this network global constraints are derived which restrict the application of rules. These conditions are the previous architectures of any edge ending in an invalid architecture. The evolution contract takes this condition as assumption and the negated invalid architecture as guarantee. 5
We presented a modeling concept for evolution specifying all possible changes
of the SoS over time as an extension of the UPDM framework. We introduced
a novel approach for deriving dynamicity contracts restricting such evolution
models in order to prevent reaching invalid architectures with respect to the
static specification of an SoS. Our prototype implementation offers so far an
export mechanism from UPDM models created with Rhapsody to GROOVE, and
feed back the generated architecture alternatives to Rhapsody. For the
generated models we can apply our previously introduced virtual integration checker
[