AADL is an aerospace standard for model-driven design of complex real-time embedded systems. Currently, behavioral properties of AADL models can be specified inside the system description using AADL concepts or outside it using external textual languages, and verified using schedulability analysis or (Time Petri Net-based) model-checking tools. This paper (1) proposes Visual Timed Scenarios (V T S) as a graphical property specification language for AADL, and (2) devises an effective translation from V T S to Time Petri Nets (TPN) which enables modelchecking properties expressed in V T S over AADL models using TPNbased tools integrated into AADL-compliant IDEs (e.g., TOPCASED).
paper we adopt Visual Timed Scenarios (V T S) [
AADL Model Expected Property of AADL Model
Ocarina
(no flows)
VTS CS [
VTS ES [
TPN Model
TPN Property
TPN
Modelchecker
CS2ES [
ES2TPN
The paper is structured as follows. Sec. 2 recalls V T S by means of an example. Sec. 3 briefly reviews Time Petri Nets (TPN). Sec. 4 presents the translation of V T S into TPN. Sec. 5 proposes a procedure to model-check whether a TPN satisfies a property expressed in V T S. Sec. 6 illustrates the application of these results for verifying different behavioral properties of AADL models: (1) modechange behaviors, and (2) flow specifications. 2 2.1
Visual Timed Scenarios [
The basic elements of V T S graphical notation are points connected by lines
and arrows. Points are labeled by sets of events, meaning that the point stands
for an occurrence of one of the events in an execution. V T S can represent
precedence relations and temporal distances between points; and sets of events which
are forbidden between them. The detailed formalization of V T S and its
thorough comparison with other visual languages is given in [
Consider a system composed of two jobs J ob1 and J ob2 (Fig. 2, based on [
LAUNCH START1
END1
START2
END2 Job1 Points are labeled with events. Triangles below points are used to display optional point names, needed for the formal notation. An arrow between two points specifies a precedence relationship. Arrow labels specify forbidden events between points: for instance, there is no START2 event between START1 and END1. A double forward arrow means “the next” occurrence of the event of the destination point (i.e., shorthand for labeling the arrow with the destination’s label). A double backward arrow meas “the previous” occurrence of the event of the source point (i.e., shorthand for labeling the arrow with the source’s label). A dashed line linking two points expresses a temporal distance between them. Dashed lines can also be labeled with forbidden events. Fig. 4 shows the graphical notation of V T S elements used in this work6.
Verifying conditional scenarios is done by building (using the CS2ES tool
showed in Fig. 1) a set of existential scenarios that stand for all possible
counterexamples of the conditional scenarios [
LAUNCH START1 ¬ END1
LAUNCH START2 ¬ END2 from C. Given a sequence s, |s| is its length (|s| d=ef ∞ when s is infinite) and Π(s) d=ef {i ∈ N / 0 ≤ i < |s|} is the set of positions of s. Given i, j ∈ Π(s), si is the ith element of s; si] is the prefix ending at position i; s[i is the suffix starting at position i and s[i,j] is the sub-sequence from position i to position j (if def i > j, s[i,j] = s[j,i]). Using ‘(’ or ‘)’ instead of ‘[’ or ‘]’ means the corresponding sub-sequence does not include its border(s). We call f irst(s) the first element of s. If s is finite, last(s) is its last element. For X ⊆ C, s ∩ X denotes the set of elements of X appearing in s, i.e., {x ∈ X | ∃i. si = x}.
A temporal sequence is a weakly increasing sequence of timestamps (i.e., non negative real numbers). Given a finite temporal sequence τ we define Δ(τ ) as the time elapsed during τ : Δ(τ ) = last(τ ) − f irst(τ ) or 0 if |τ | = 0. A temporal sequence τ can be shifted by a real number ǫ producing a temporal sequence called τ + ǫ, such that ∀i ∈ Π(τ ); (τ + ǫ)i = τi + ǫ.
A trace over a set C is a pair hs, τ i where s is a sequence over C and τ is a temporal sequence of the same length. Given a trace σ = hs, τ i , we define |σ| d=ef |s| and Π(σ) d=ef Π(s). A trace is time-divergent iff for any real number T there exists a position k such that Δ(τk]) > T .
The semantics of V T S assigns to each scenario a set of traces satisfying it. Labeled points represent events in the traces, they can match a particular position in a trace if the event in that position is among the allowed events associated to the point by the labeling function ℓ.
Intuitively, a matching is a mapping between points in a scenario and positions in a trace, exhibiting how the trace satisfies the scenario. Formally: Definition 2 (V T S semantics). Given a scenario S = hΣS , P, ℓ, 6≡, <, γ, δi , a trace σ = hs, τ i over Σ′ where ΣS ⊆ Σ′, and a mapping ˆ· : P → Π(σ); we say that ˆ· is a matching between S and σ iff for all points p, q ∈ P : M1 sˆp ∈ ℓ(p); the mapping for a point is a position of the trace with an event that labels this point.
M2 if p 6≡ q then pˆ 6= qˆ; two different points cannot map to the same position. M3 if p < q then pˆ < qˆ; the position of the source point must be smaller than the destination’s.
M4 s(ˆp, ˆq) ∩ γ(p, q) = ∅; no forbidden event can appear in the sub-trace defined by corresponding occurrences of the points.
M5 sˆp) ∩ γ(0, p) = s(ˆp ∩ γ(p, ∞) = ∅; no forbidden event specified between begin (resp., a point) and a point (resp., end) can appear before (resp., after) the corresponding occurrence of the point.
M6 Δ(τ[ˆp, ˆq]) ² δ(p, q); the time elapsed between the occurrences of the corresponding points must satisfy the specified time restriction.
M7 Δ(τˆp]) ² δ(0, p); the time elapsed since begin until the occurrence of a point must satisfy the specified time restriction.
Rules M4-5 and M6-7 must be considered only when the domains of the functions γ and δ are defined, respectively.
a scenario S (noted σ ² S) iff there exists at least one matching between them. 3
Time Petri Nets [
Definition 4 (Time Petri Net). A Time Petri Net7 is a tuple N = hS, T, Pre, Post, ΣN , L, Inh, ≻, m0, Isi, where: – S is a finite set of places. – T is a finite set of transitions. – Pre ⊆ T × S is a relation between transitions and input places. – Post ⊆ T × S is a relation between transitions and output places. – ΣN is a finite set of events. – L : T → ΣN ∪ {λ} is a function that labels each transition with an event or with λ 6∈ ΣN . We assume that ∀ e ∈ ΣN , ∃ t ∈ T, s.t. L(t) = e. – Inh ⊆ T × S is a relation that defines inhibitor places for transitions. – ≻ ⊆ T × T is a priority (irreflexive, asymmetric, and transitive) relation between transitions. – m0 ⊆ S is a set of places with initial marking.
– Is : T → I is a function called static interval function. 7 For simplicity, we consider here ordinary (i.e. all arcs have weight 1) TPNs, but the results can be extended to non-ordinary ones. 3.2
Given a TPN N , a state of N is a pair ω = hm, Ii, where m : S → N is a marking and I : T → I is the interval function that associates a temporal interval with every transition enabled at m. The initial state is denoted ω0.
The semantics of TPNs defines the evolution of a TPN state resulting from
the firing of transitions and passage of time. The reader is referred to [
We write ω L−(t→)@θ ω′ to denote that from state ω, transition t is fired after a time θ, resulting in state ω′; and ω −λ@→θ ω′ to denote that from state ω, time can elapse to state ω′. An execution is a time-divergent sequence ρ : ω0 a−0@→θ0 ω1 a−1@→θ1 . . . We write mρi to denote the marking of the i-th state of ρ. The time-divergent trace of ρ is σ = hs, τ i with s = a0, a1 . . . , and τ = ϑ0, ϑ1 . . . , where ϑ0 = θ0 and ϑi = ϑi−1 + θi, for i ≥ 1. 4
The translation algorithm proceeds as follows: for each part of the V T S scenario
that must be matched, it builds a TPN component. So, each point, forbidden
event, time restriction, precedence between points, etc., in the V T S scenario,
generates a TPN. The translation of the whole scenario is obtained by the fusion
(a special composition, see below) of all components. The rules that formally
define this translation can be found in [
Construction of TPN components for matching points. In order to recognize occurrences of events as matchings of points, we construct a TPN as follows. For every point p of the V T S scenario, we add two places to the TPN: notYetp and matchp. The place notYetp has an initial marking and represents that no event labeling point p has occurred yet. The place matchp, if marked, models that a matching event for this point has occurred. Between these places, we add the possible matching transitions: one transition for each event e labeling point p. Each of these is labeled with e, and has a pre-arc from notYetp and a post-arc to matchp. Also, we must consider the case where two (or more) points match the same event. Therefore, we add transitions for all possible combinations of multiple matching points for each event.
To take into account precedence relations among points, for every matching transition into place matchp we add a read-arc from any place matchq, whenever there is a precedence arrow from q to p (this is because place matchq must be marked before marking place matchp).
Finally, this component has special transitions which will be used in the construction of forthcoming components. Transition trape is set with higher priority than any matching transition labeled with event e. Transition trapAll has higher priority than all transitions labeled trape, and therefore higher than all matching transitions (by transitivity). For every point p and event e labeling p, a transition trape¬p is added, with higher priority than any transition matching event e but not matching point p. The purpose of these transitions is to define a priority schema, not to be fired, as they are always disabled by adding a pre-arc from a place called empty which is never marked. Fig. 7 gives an example of the construction of TPN component for matching points.
a q b p
point. To recognize occurrences of events not associated to point matchings, we add a unique place loop, with an initial marking, and loop transitions for each event e of the scenario.
Fig. 8 shows the resulting TPN for a simple example. a q b p
a loop a loop
b loopb
tions. Suppose there is precedence relation from point q to p, and let matchq and matchp be the corresponding matching places of the points. For each forbidden event e on the precedence relation, a forbidden transition, labeled with e, is added with a pre-arc from matchq and an inhibitor-arc from matchp.
In order for this transition to capture all possible occurrences of the forbidden event e, if e is labeling p, a priority relation is added to transition trape, otherwise is added to transition trape¬p. As we have seen, trape has higher priority than any matching transition for event e, and trape¬p, has higher priority than any matching transition for event e not related with p.
Also, the corresponding loop transition for event e is disallowed whenever the forbidden transition is enabled, by setting a priority relation. Therefore, the loop transition is enabled only when point q has occurred but not yet point p, avoiding any occurrence of event e not corresponding to the matching point p.
At last, a post-arc with an inhibitor-arc is added to place invalidMatch. This place, as we will show later, if not empty, avoids reaching the acceptance condition for matching the whole V T S scenario. The purpose of this inhibitor-arc is to ensure the boundedness of the TPN.
Fig. 9 illustrates the construction of TPN components for forbidden events on precedence relations.
b
dence relations. In V T S, temporal restrictions over a precedence relation can involve two cases: (1) when the time elapsed between the source and destination points has a maximum allowed value, and (2) when it has a minimum allowed value. Note that V T S time restrictions allow both cases to be combined in an interval constraint.
In case of an upper limit β, we add a transition tooLateq·p with a lower bound of β. This transition has a read-arc from place matchq, an inhibitor-arc from place matchp, and a post-arc with an inhibitor-arc to place invalidMatch. We add a priority relation from this transition to trapAll to avoid matching points when it is enabled. Therefore, this transition will avoid point p to match after a time β since point q has occurred. Fig. 10(a) and 10(b) illustrates this construction.
In case of a lower limit α, we use two transitions. One transition, called onT imeq·p, will delay at least α after point q matches, leaving a token at a new place notEarlyq·p. The other transition, called tooEarlyq·p, has a pre-arc from place matchp, an inhibitor-arc from place notEarlyq·p, and a post-arc with an inhibitor-arc to place invalidMatch. Therefore, this transition will prevent a scenario matching if point p occurs, but not transition onT imeq·p which only becomes enabled after a time α since point q’s occurrence. Fig. 10(c) and 10(d) illustrates this construction.
tions. Consider two points q and p, such that p 6≡ q. By definition these points have different matching, then necessarily, either q occurs before p, or p occurs before q. Therefore, both cases must be considered. For this, we apply the rules explained above for taking care of precedence relations. (a) V T S scenario 1 a q a q <10 >=2 a q b p b p b p matchq
Scenario matching We add a place, namely, validMatch, and two transitions, namely, accept and reject. Transition accept, immediately fires if all points have been matched, and only if place invalidMatch is empty, putting a token in validMatch. Transition reject, fires as soon as invalidMatch is reached, removing all tokens (if any) from validMatch. This transition is needed to wait for occurrences of forbidden events in the future. Fig. 11 illustrates this construction.
Fusion of TPNs. Now, we introduce the fusion operation, to obtain a TPN by combining two or more TPNs. This operation is based on set union; so if two combined TPNs share places and transitions, these will appear once in the final construction. The fusion operation between two TPNs, N1 and N2, is denoted as N1 ⊕ N2. Fig. 12 illustrate fusion operation. Resulting fusion of TPNs Fig. 12(a) and Fig. 12(b) is presented in Fig. 12(c). matchp1 notYetp4 p4START2 Definition 5. Given a scenario S, we define the TPN of S, denoted TS , as the fusion of the component TPNs constructed as explained above.
Example. Fig. 13 shows the resulting TPN for the V T S scenario initially presented at Fig. 5(e)8. For this scenario, the TPN results from the fusion of the following components: – Matching points: for points p4 (Fig. 12(a)) and p1. – Unmatched event: for events ST ART 2 and LAU N CH. – Forbidden events: for the forbidden event of ST ART 2 labeling the precedence relation from point p1 to p4. – Temporal restrictions: for time restriction of < 14 labeling the precedence relation from point p1 to p4 (Fig. 12(b)). – Scenario Matching. < 1 4 LAUNCH p1 START2
p4 (a) V T S empty notYetp1 8 In Fig. 13(b) transition names have been omitted in order to keep the figure small and readable. 5
The problem of checking whether a system under analysis (SUA) modeled as a TPN N satisfies a V T S scenario S is solved in the following way. The algorithm presented in Sec. 4 translates S into a TPN (observer) TS which recognizes matching traces. TS is composed with the SUA N to check whether a matching execution exists, by using available model checking tools for TPNs. Specifically, the model-checking problem consists in verifying whether there exists an execution that reaches a state where place validMatch of TS is marked, and remains marked thereafter.
Property 6. Given N and S then: N kTS is bounded iff N is bounded. Property 7. Given N , S with ΣS ⊆ ΣN , and a trace σ over ΣN ∪ {λ} then: σ is a trace of N kTS iff σ is trace of N .
Therefore, we are sure that the composition of N with the TPN TS of the scenario preserves the traces of the SUA.
N ² S iff there exists a time-divergent execution sequence ρ of N kTS such that, ∃k ∈ N. ∀k′ ≥ k. mρk′ (validMatch) = 1. 6
To carry out our tests, we resort to a tool chain that allows us to link the
V T S scenarios with AADL models. Based on a property expressed as a V T S
conditional scenario, we use the tool presented in [
In AADL systems, components can operate in different modes, where each of
them is associated with a configuration of the component. Changes between
modes are triggered by events. A more detailed description can be found in [
SOM1
p1 eventTr_a t1 [0,0]
LeavingSOM1 p2
hyperLeavingSOM1 t2 [0,0]
SOM1to2Transition p3
hyperEnterSOM2 t3 [
1
T2_disp1atch
AADL flow specifications are used to describe externally observable sequences
of connections through component ports. Flow specifications can be annotated
with properties, such as latency, whose verification depend on the properties of
the involved components, ports, etc., such as execution times, periods, deadlines,
communication delays, etc. Quantitative analysis of flow properties is addressed
in [
Ds_period [50,50] [0,0] T2_dispatch [0,0] T3_conn T1_run 1 1
T11_ou1tput T11_co1nn
Ds_output
[
[0,0]
T2_output
[
Ds_output
D1s_co1nn <=48 This paper proposes an approach for checking complex properties on AADL specifications by relying on the visual language V T S for expressing them. To make it practical, we devised a procedure for generating TPNs from V T S to enable its connection with available IDEs for AADL, such as OSATE and TOPCASED, which integrate TPN-based verification tools.
V T S scenarios proved to be adequate to intuitively express complex
properties of AADL models. We also incorporate the idea of using them to describe
flows in a more general and independent way. Besides its concrete practical
application to AADL-centric system design, the translation presented in this work
provides an alternative way to verifying V T S requirements in addition to the
one based upon timed automata reachability analysis [
Several future research directions are envisaged. First, we plan to generate
TOPCASED tool-independent intermediate modeling language FIACRE [