MoDELS'08 ACES-MB Workshop Proceedings V T S-based Specification and Verification of Behavioral Properties of AADL Models⋆ D. Monteverde1,3 , A. Olivero1 , S. Yovine2⋆⋆ , and V. Braberman3⋆ ⋆ ⋆ 1 Inst. de Tecnologı́a, UADE, Argentina. {damonteverde|aolivero}@uade.edu.ar 2 VERIMAG-CNRS, France. Sergio.Yovine@imag.fr 3 Departamento de Computación, FCEyN, UBA, Argentina. vbraber@dc.uba.ar Abstract. 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 model- checking properties expressed in V T S over AADL models using TPN- based tools integrated into AADL-compliant IDEs (e.g., TOPCASED). 1 Introduction The Architecture Analysis and Design Language (AADL) [13] is an aerospace standard released by the Society of Automotive Engineers (SAE) for model-based specification and analysis of complex real-time embedded systems. AADL has been designed to support model-based and formal analyses of critical properties. For this, AADL provides modeling concepts for the description of application system architectures in terms of suitable abstractions of software and hardware components and the interactions between them. The definition of AADL moti- vated the development of AADL-centric tools such as OSATE4 and Ocarina [10], as well as the integration of AADL into domain-specific model-driven software engineering environments, such as TOPCASED5 . This enabled different kinds of formal analyses, including schedulability, e.g., with Cheddar [14], and model- checking, e.g., with Time Petri Net-based tools like Tina [4] and Romeo [9]. A way of enhancing the usability of formal techniques in model-driven sys- tem design and flows analysis consists in resorting to visual languages capable of representing and visually presenting application semantics in a clear, precise way, specially in the context of event-based systems. Following this idea, in this ⋆ Partially supported by ANPCyT projects PICT 32440 and PICTO-CRUP 31352, STIC-AmSud project TAPIOCA and UBACyT X021 ⋆⋆ Currently visiting UBA and UADE. ⋆⋆⋆ Conicet 4 http://www.aadl.info/ 5 http://www.topcased.org Toulouse, France, September 29, 2008 23 MoDELS'08 ACES-MB Workshop Proceedings paper we adopt Visual Timed Scenarios (V T S) [1] as a language for specifying behavioral properties of models of systems described in AADL. In order to make possible the verification of these properties using available tools integrated into AADL-complaint IDEs, we devise a translation from V T S to Time Petri Nets. This allows to use existing model checking tools for verifying if operational de- scriptions encompassed by AADL model satisfy the translated property. Fig. 1 exhibits the integration of the AADL models with V T S scenarios in a tool chain. The part concerning V T S (enclosed in gray) will be explained in detail along this work. Ocarina AADL Model TPN Model (no flows) TPN Expected Modelchecker Property of VTS CS [7] VTS ES [1] TPN Property AADL Model CS2ES [11] ES2TPN Fig. 1. Tool chain integrating AADL and V T S The paper is structured as follows. Sec. 2 recalls V T S by means of an exam- ple. 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) mode- change behaviors, and (2) flow specifications. 2 Visual Timed Scenarios (V T S) 2.1 Informal presentation Visual Timed Scenarios [1, 7] language is used to describe event patterns, which can be regarded as simple, graphical depictions of predicates over traces (time- stamped executions), constraining expected behavior. It basically features anno- tated partial order of relevant events, denoting a (possibly infinite) set of match- ing traces. Violation of verification goals for models such as freshness, bounded response or event correlation can naturally be expressed using the notation. 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 prece- dence relations and temporal distances between points; and sets of events which are forbidden between them. The detailed formalization of V T S and its thor- ough comparison with other visual languages is given in [7]. Here, we informally introduce V T S through a simple, yet illustrative, example. Consider a system composed of two jobs Job1 and Job2 (Fig. 2, based on [2]). The behavior of the system is as follows: (1) Job1 if started, always terminates; (2) Job2 if started, always terminates; (3) Job2 can not start while Job1 is in Toulouse, France, September 29, 2008 24 MoDELS'08 ACES-MB Workshop Proceedings execution; (4) Job1 must terminate in at most 12; (5) Job2 must wait at least 14 to start; (6) The temporal distance between both jobs’ ends is at most 10. LAUNCH START1 END 1 START2 END2 Job1 Job2 time Fig. 2. Example of two jobs Fig. 3 illustrates these requirements expressed in V T S as conditional sce- narios [7]. Conditional scenarios allow to state that whenever an antecedent sub-scenario (depicted in black) happens, a consequent sub-scenario (depicted in gray) must happen too. START1 END1 ¬ START2 1 1 1 1 1 p2 p3 LAUNCH <=10 <=12 START2 END2 p1 >=14 1 1 1 1 1 p4 p5 Fig. 3. V T S Conditional scenarios for requirements of two jobs example 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 coun- terexamples of the conditional scenarios [7, 11]. These scenarios, a.k.a. anti- scenarios, model all the ways in which a conditional scenario may be violated by the system. This work only relies on how to model-check existential scenar- ios, and therefore, hereinafter, existential scenarios are referred as “scenarios”. Fig. 5 illustrates all the V T S anti-scenarios of the conditional scenario of Fig. 3. 6 V T S has more primitives, that increase its expressive power, which are omitted here for the sake of simplicity. The interested reader is referred to [7]. Toulouse, France, September 29, 2008 25 MoDELS'08 ACES-MB Workshop Proceedings begin end point p precedes q q matches the next b-event after p events a b a b forbidden events forbidden events (min, max] (min, max] point name p q p q p and q must match different events p matches the a-event previous to q p and q are consecutive a and b events a forbidden events b a b a b (min, max] forbidden events forbidden events (min, max] (min, max] p q p q p q Fig. 4. V T S graphical notation A big full circle stands for the begin of the execution, and two concentric circles correspond to its end. LAUNCH START1 END1 LAUNCH START1 LAUNCH START2 START2 ¬ END1 ¬ END2 (a) Job1 starts, but does (b) Job2 starts, but does (c) Job2 starts while Job1 not terminate (1) not terminate (2) is in execution (3) START1 END1 START1 END1 LAUNCH >10 LAUNCH LAUNCH START2 START2 END2 >12 <14 (d) Job1 terminates after (e) Job2 starts before (f) More than 10 passes 12. (4) 14. (5) between jobs ends. (6) Fig. 5. Anti-scenarios (existential scenarios). 2.2 Formal presentation Definition 1 (V T S syntax). A scenario is a tuple hΣ, P, ℓ, 6≡, <, γ, δi , where: – Σ is a finite set of events; – P is a finite set of points; – ℓ : P → 2Σ is labels each point with a non-empty set of events; – 6≡ ⊆ P × P is an asymmetric relation ( inequality) between points (graphi- cally represented by dotted lines); – < ⊆ (P ⊎ {0} × P ⊎ {∞}) r {h0, ∞i} is a precedence relation between points (graphically represented by arrows), where 0 and ∞ represent the begin and the end of an execution, resp.; – γ : (6≡ ∪ <) → 2Σ assigns to each pair of points, related by inequality or precedence, the set of events forbidden between them; – δ : (6≡ ∪ (< r (P × {∞}))) → I assigns to each inequality or precedence relation an integer-bounded or upper-unbounded interval of non-negative real- numbers restricting the time elapsed between the two points. Given a set C, a sequence over C is a (possibly infinite) sequence of elements def from C. Given a sequence s, |s| is its length (|s| = ∞ when s is infinite) and Toulouse, France, September 29, 2008 26 MoDELS'08 ACES-MB Workshop Proceedings def Π(s) = {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 def def |σ| = |s| and Π(σ) = Π(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 posi- tions 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 sp̂ ∈ ℓ(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 sp̂) ∩ γ(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. Definition 3 (Existential V T S Semantics). We say that a trace σ satisfies a scenario S (noted σ ² S) iff there exists at least one matching between them. Toulouse, France, September 29, 2008 27 MoDELS'08 ACES-MB Workshop Proceedings 3 Time Petri Nets (TPNs) Time Petri Nets [5] are a widely used formalism for timed systems. They are supported by several tools (e.g. TINA [4], Romeo [9]). TPNs extend Petri nets with temporal intervals associated with transitions: assuming transition t, with an interval [α, β], became last enabled at time τ , then t cannot fire earlier than time τ + α and must fire no later than τ + β, unless disabled by firing some other transition. Firing a transition takes no time. 3.1 TPNs Formal Syntax Definition 4 (Time Petri Net). A Time Petri Net7 is a tuple N = hS, T, Pre, Post, ΣN , L, Inh, ≻, m0 , I s i, 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. – I s : T → I is a function called static interval function. Fig. 6 summarizes the graphical notation for TPNs used in this work. place place transition transitions priority place event event is Ȝ when is transition in initial not explicit t1 is higher marking [min,max] interval is [0, ) priority place name place name transition name when is not explicit t1 t2 than t2 transition pre-arc transition post-arc read arc inhibitor arc place with pre-arc and post-arc to same transition l0 t1 t1 l0 l0 t1 l0 t1 Fig. 6. TPN graphical notation Parallel Composition. This operation combines two TPNs in one TPN where transitions with the same label (different from λ) are merged. The parallel com- position between two TPNs, N1 and N2 , is denoted as N1 kN2 . See [5] for more details. 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. Toulouse, France, September 29, 2008 28 MoDELS'08 ACES-MB Workshop Proceedings 3.2 TPNs Semantics 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 [5] for the detailed semantics. L(t)@θ We write ω −→ ω ′ to denote that from state ω, transition t is fired after λ@θ a time θ, resulting in state ω ′ ; and ω −→ ω ′ to denote that from state ω, time a0 @θ0 can elapse to state ω ′ . An execution is a time-divergent sequence ρ : ω0 −→ a1 @θ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 Translating V T S into TPN 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 [12]. The ES2TPN tool (Fig. 1) performs this whole process. 4.1 Construction of TPN components Construction of TPN components for matching points. In order to rec- ognize 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 pri- ority than any matching transition labeled with event e. Transition trapAll has higher priority than all transitions labeled trape , and therefore higher than all Toulouse, France, September 29, 2008 29 MoDELS'08 ACES-MB Workshop Proceedings 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. b trap b¬p a b notYet p match p trapAll empty q p matchq pb trap b (a) V T S scenario (b) TPN component for point p Fig. 7. TPN component construction for matching points. Construction of TPN components for events not matched by any 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 b a b loop a loop b q p loop (a) V T S scenario (b) TPN of unmatched occurrences of events a and b Fig. 8. TPN component construction for unmatched events. Construction of components for forbidden events on precedence rela- 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 forbid- den 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. Toulouse, France, September 29, 2008 30 MoDELS'08 ACES-MB Workshop Proceedings 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 condi- tion 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 c match q matchp matchq matchp trap b ¬p trap c a b ¬ b, c b c invalidMatch forbidden bq.p invalidMatch q p loop b loopc forbidden cq.p (a) V T S scenario (b) TPN for forb. event b (c) TPN for forb. event c Fig. 9. TPN components for forbidden events over precedence relations. Construction of TPN components for temporal restrictions on prece- 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 tooEarly q·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. Construction of TPN components for restrictions over inequality rela- 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. Toulouse, France, September 29, 2008 31 MoDELS'08 ACES-MB Workshop Proceedings a b match q match p <10 [10,’) q p trapAll tooLate q.p invalidMatch (a) V T S scenario 1 (b) TPN 1 a b matchq [2, matchp notEarly q.p onTime q.p >=2 [0,0] q p tooEarly q.p invalidMatch (c) V T S scenario 2 (d) TPN 2 Fig. 10. TPN components for time restrictions over precedence relations 4.2 Construction of the TPN for the whole scenario 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, remov- ing all tokens (if any) from validMatch. This transition is needed to wait for occurrences of forbidden events in the future. Fig. 11 illustrates this construc- tion. a b q p (a) V T S scenario (b) TPN Fig. 11. TPN component for scenario matching. 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). Toulouse, France, September 29, 2008 32 MoDELS'08 ACES-MB Workshop Proceedings START2 START2 match p1 match p1 matchp1 match p4 match p4 match p4 notYetp4 p4 START2 notYetp4 p4 START2 trapAll trapAll trapSTART2 trapAll trapSTART2 [14, [14, tooLatep1.p4 invalidMatch tooLatep1.p4 invalidMatch (a) TPN N1 (b) TPN N2 (c) TPN N1 ⊕ N2 Fig. 12. TPNs’ fusion sample 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 pre- sented 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 re- lation from point p1 to p4 (Fig. 12(b)). – Scenario Matching. START2 START2 LAUNCH LAUNCH LAUNCH loop START2 p1 notYet p1 < 14 START2 matchp1 [0,0] invalid notYet p4 matchp4 Match p4 empty [14, [0,0] validMatch (a) V T S (b) TPN Fig. 13. TPN for scenario: Job2 starts before 14. 8 In Fig. 13(b) transition names have been omitted in order to keep the figure small and readable. Toulouse, France, September 29, 2008 33 MoDELS'08 ACES-MB Workshop Proceedings 5 Model Checking V T S 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 algo- rithm 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 execu- tion 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. Theorem 8 (Model checking V T S). Given N and S with ΣS ⊆ ΣN , then: N ² S iff there exists a time-divergent execution sequence ρ of N kTS such that, ∃k ∈ N. ∀k ′ ≥ k. mρk′ (validMatch) = 1. 6 Case studies 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 [11] to generate the related V T S existential scenarios, that are then translated into TPNs. For this last step, we have developed a tool that implements the translation algorithm described in Sec. 4. On the other hand, the TPN representing the AADL models have been constructed manually9 . Finally we use the composition of both resulting TPNs as input to the tool Tina, which generates the reachability graph preserving LTL. To check whether the model satisfies the property, we encode Thm. 8 as an LTL model-checking problem and use the selt application of the Tina tool-box. For the case studies we analyzed, because selt is unable to determine whether an execution is time-divergent, we either relied on the strongly non- Zeno [15] hypothesis of the SUA or performed semi-automatic verification. We discuss in the conclusions an approach for automatizing the procedure derived from Thm. 8. 6.1 AADL Mode Change Protocol 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 [6]. 9 In the future we plan to use OCARINA [10] or TOPCASED (through FIACRE [3]) to generate them automatically. Toulouse, France, September 29, 2008 34 MoDELS'08 ACES-MB Workshop Proceedings p1 p0 SystemStop hyperEnterSOM1 SOM1 t6 [10,10] c2p1 clock2_p1 [0,0] t0 SystemStart p6 SOM2to1Transition eventTr_a t1 [0,0] clock1_p1 c1p1 hyperLeavingSOM2 t5 [0,0] LeavingSOM1 p2 [5,5] c2t1 hyper2 hyper1 c1t1 [10,10] LeavingSOM2 p5 hyperLeavingSOM1 t2 [0,0] c2p2 colck2_p2 c1p2 colck1_p2 [0,0] t4 eventTr_b SOM1to2Transition p3 [0,0] c2t2 clock2_t2 clock1_t2 c1t2 [0,0] dismiss_a hyperEnterSOM2 t3 [5,5] A event_a event_a prodA dismiss_b p4 B clock3_p1 c3p1 SOM2 event_b event_b prodB eventTr_c dismiss_c hyper3 c3t1 [5,5] [0,0] t7 C event_c event_c prodC LeavingSOM2 c3p2 p7 colck3_p2 [0,0] SOM2to3Transition [15,15] SOM3 t8 t9 clock3_t2 c3t2 [0,0] hyperLeavingSOM2 p8 hyperEnterSOM3 p9 Fig. 14. TPN of the model driver Fig. 14 shows the TPN of a driver system (extracted from [6]). V T S can be used to analyze and verify different kinds of properties. The mode-change protocol should ensure that the maximum delay between a mode-change request and the entry in the new mode is lower than a specified value. Fig. 15(a) shows a conditional scenario for the verification of this property at the request of event a. Fig. 15(b) expresses the correlation between the driver events with the environ- ment ones. For example, part of this conditional scenario establishes that if a change to mode SOM2 occurs, a corresponding input event event a triggering the mode-change must have occurred. Fig. 15(c) presents a conditional scenario where the antecedent defines an environment behavior by which a certain driver property (the consequent) must be verified. It is important to notice that with V T S we avoid modelling the environment as a (hand-coded) TPN composed with the driver model as proposed at [6], by including its behavior in the sce- nario as its antecedent. All these scenarios were verified to hold. event_a event_c eventTr_a hyperLeavingSOM1 hyperEnterSOM2 1 1 eventTr_a, hyperEnterSOM2 1 hyperEnterSOM3 eventTr_b, [0, 10] 1 1 1 eventTr_ceventTr_c ¬ eventTr_a, eventTr_b, 1 1 1 ¬ eventTr_b 1 [5, 15] (a) Requirement 1 (b) Requirement 2 event_a event_c ¬ event_b ¬ event_b ¬ event_b [0 , [0 20 eventTr_a hyperEnterSOM2 eventTr_c hyperEnterSOM3 , ] 10 ] 1 1 [5, 15] 1 1 [15, 20] 1 1 1 1 1 (c) Requirement 3 Fig. 15. V T S Conditional Scenarios for verifying Mode-Change example Toulouse, France, September 29, 2008 35 MoDELS'08 ACES-MB Workshop Proceedings 6.2 AADL Flows Specification 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 [8] and implemented in OSATE. The proposed technique, is based on case- by-case analysis according to the architecture of the sub-components. Here, we propose using V T S scenarios for checking flow latency. We believe the advantages of our approach are twofold. First, it is independent of the architecture of the SUA. Second, it allows specifying non-linear flows, currently not available in AADL. As a case study, we use the example provided in [8]. The TPN of the 3-task system with a periodic sensor and aperiodic tasks and actuator is shown in Fig. 16(a). The V T S scenario for the flow specification is shown in Fig. 16(b). This scenario asserts two properties at once: whenever the sensor produces an output, then (1) the flow is realized, and (2) its latency is less than or equal to 48. Notice that our approach gives a tighter latency than the one in [8]. Ds_period Ds_output Ds_conn [50,50] [0,0] [1,2] T1_conn T1_output T1_run T1_dispatch <=48 Da_output 1 1 Ds_output Ds_conn 1 1 1 [0,0] [6,10] [0,0] [0,0] T2_dispatch T2_run T2_output T2_conn T1_dispatch T1_run T1_output T1_conn 1 1 1 1 1 [0,0] [0,0] [15,23] [0,0] 1 1 1 T3_conn T3_output T3_run T3_dispatch T2_dispatch T2_run T2_output T2_conn 1 1 1 1 1 1 1 1 [0,0] [6,10] [0,0] [0,0] T3_dispatch T3_run T3_output T3_conn 1 1 1 1 Da_output [1,3] 1 1 1 1 (a) TPN of aperiodic tasks (b) V T S scenario of flow latency Fig. 16. Flow latency example (taken from [8]) 7 Conclusions and Future Works This paper proposes an approach for checking complex properties on AADL spec- ifications 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 prop- erties 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 ap- plication 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 [1]. Toulouse, France, September 29, 2008 36 MoDELS'08 ACES-MB Workshop Proceedings Several future research directions are envisaged. First, we plan to generate TOPCASED tool-independent intermediate modeling language FIACRE [3] in- stead of TPN directly. This will allow model-checking V T S with a larger number of tools integrated by the TOPCASED consortium. Second, we will explore more deeply the connection between V T S and AADL flows. The purpose of this is to investigate whether AADL flow specifications could be extended to cope with non-linear flows. Last but not least, to fully automatize the approach resulting from Thm. 8, a verification procedure which takes into account time-divergence should be implemented for TPNs, adapting, for instance, the algorithms pro- posed in [15] for timed Büchi automata. References 1. A. Alfonso, V. Braberman, N. Kicillof, and A. Olivero. Visual Timed Event Sce- narios. In Proc. of the 26th ACM/IEEE ICSE ’04. ACM Press, 2004. 2. K. Altisen, G. Gossler, A. Pnueli, J. Sifakis, S. Tripakis, and S. Yovine. A frame- work for scheduler synthesis. In Proc. RTSS ’99. IEEE Comp. Soc. Press, 1999. 3. B. Berthomieu, J.-P. Bodeveix, P. Farail, M. Filali, H. Garavel, P. Gaufillet, F. Lang, and F. Vernadat. Fiacre: An intermediate language for model verification in the topcased environment. In 4th European Conf. ERTS, January 2008. 4. B. Berthomieu and F. Vernadat. Time Petri Nets Analysis with TINA. In 3rd Int. Conf. on the Quantitative Evaluation of Systems - (QEST’06), 2006. 5. B. Berthomieu and F. Vernadat. State Space Abstractions for Time Petri Nets. In Handbook of Real-Time and Embedded Systems, Crc Computer & Information Science Series. Chapman & Hall, July 2007. 6. D. Bertrand, A.-M. Déplanche, S. Faucou, and O. H. Roux. A Study of the AADL Mode Change Protocol. In 13th IEEE International Conference on Engineering of Complex Computer Systems. IEEE, 2008. 7. V. Braberman, N. Kicillof, and A. Olivero. A Scenario-Matching Approach to the Description and Model Checking of Real-Time Properties. IEEE Transactions on software Engineering, 31(12), 2005. 8. P. Feiler and J. Hansson. Flow Latency Analysis with the Architecture Analysis and Design Language (AADL). Technical Note CMU/SEI-2007-TN-010, Carnegie Mellon University, June 2007. 9. G. Gardey, D. Lime, M. Magnin, and O. H. Roux. Romeo: A Tool for Analyzing Time Petri Nets. In Computer Aided Verification, pages 418–423. Lecture Notes in Computer Science, 2005. 10. J. Hugues, B. Zalila, L. Pautet, and F. Kordon. From the Prototype to the Final Embedded System Using the Ocarina AADL Tool Suite. ACM Transactions in Embedded Computing Systems, Oct. 2008. 11. D. Monteverde. Verificación Automática de Escenarios Condicionales. Master’s thesis, FCEyN. Univ. de Buenos Aires, 2007. 12. D. Monteverde, A. Olivero, S. Yovine, and V. Braberman. VTS-based specification and verification of behavioral properties of AADL models. Technical report, DC. FCEN. UBA. http://www.dc.uba.ar/people/exclusivos/vbraber, 2008. 13. SAE. Architecture Analysis and Design Language. SAE Standard AS5506, 2004. 14. F. Singhoff, A. Plantec, and P. Dissaux. Can We Increase the Usability of Real Time Scheduling Theory? The Cheddar Project. In Ada-Europe 2008, 2008. 15. S. Tripakis, S. Yovine, and A. Bouajjani. Checking timed buchi automata empti- ness efficiently. Formal Methods in System Design, 26(3), May 2005. Toulouse, France, September 29, 2008 37