Model-Based Design for Embedded Systems- P17

Chia sẻ: Cong Thanh | Ngày: | Loại File: PDF | Số trang:30

Thêm vào BST

Báo xấu

68
lượt xem 6
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

Model-Based Design for Embedded Systems- P17:The unparalleled flexibility of computation has been a key driver and feature bonanza in the development of a wide range of products across a broad and diverse spectrum of applications such as in the automotive aerospace, health care, consumer electronics, etc.

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: Model-Based Design for Embedded Systems- P17

456 Model-Based Design for Embedded Systems 14.3.5.1 Derived Functions and Logic Programs 3 3 3 A query reduces some property of a model to a boolean 2 2 3 3 value: Either the property holds (the query is satisfied) or 2 3 1 2 it does not hold. Sometimes this reduction loses informa- 1 3 2 tion that should persist. For example, suppose we want to 0 1 know which states can be reached after one, two, and three transitions of a FSM, as shown in Figure 14.8. This can be done with the queries shown in Figure 14.9. Notice that FIGURE 14.8 the query findTwo, which finds all states after two steps, Calculating must first discover all the states one step away. Similarly, reachable the findThree query must find the states reachable in one states from and two steps, before finding the states reachable in three initial state 0. steps. The Nth find query does all the work of the N − 1 previous queries, which is wasteful and makes the queries unnecessarily ver- bose. This problem can be solved by temporarily storing the results of queries into data structures. These temporary results are created using derived func- tions. A derived function is a function beginning with a lowercase letter. Derived functions are only used to temporarily remember some intermedi- ate results and can never appear in the data elements of an input model.∗ For example: reach1 : ( state : State ). (14.29) declares a derived function for remembering those states reachable from an initial state after one step. Temporary results are created by writing the fol- lowing expression: reach1(y) :−x is Initial, y is State, t is Transition, t.current = x.state, t.next = y. /// Queries searching for reachable states 3. findOne ?: x is Initial, y is State, 4. t is Transition, 5. t.current = x.state, t.next = y. 7. findtwo ?: x is Initial, y is State, 8. t is Transition, s is Transition, 9. t.current = x.state, t.next = s.current, s.next = y. 11. findThree ?: x is Initial, y is State, 12. t is Transition, s is Transition, u is Transition, 13. t.current = x.state, t.next = s.current, 14. s.next = u.current, u.next = y. FIGURE 14.9 Queries for locating reachable states after one, two, and three steps. ∗ The upper/lowercase syntax for functions and derived functions is similar to the notation used in BNF grammars to distinguish terminal from non-terminal elements.
Semantics of Domain-Speciﬁc Modeling Languages 457 Note that this expression has the semantics explained in Section 14.3.2. For example, this rule adds the reach1 term to all relations Rk>0 for some k, when evaluated against the example FSM: reach1(State(“S2”, “”)) The information from reach1 can be used to calculate the states reachable in two steps. First, we introduce another derived function: reach2 : ( state : State ). (14.30) and then the expression: reach2(y) :−x is reach1, y is State, t is Transition, t.current = x.state, t.next = y. Now reach1 is used as a term in the body of this expression. Note that the ordering of expressions ensures that all the reach1 terms were calculated before evaluating this expression. The following set of expressions are recursive and because our formalism requires non-recursiveness, they cannot be expressed in it. reachN(y) :− x is Initial, y is State, t is Transition, (14.31) t.current = x.state, t.next = y. reachN(y) :− x is reachN, y is State, t is Transition, (14.32) t.current = x.state, t.next = y. The rules above calculate all of the reachable states of a FSM. Rule 14.31 cre- ates a reachN instance for each state immediately reachable from an initial state. Rule 14.32 creates a reachN instance for each state that is reachable in one step from a reachN instance. Rule 14.32 depends on Rule 14.31 and on itself, thereby creating a dependency cycle. This example shows that recursive logic programs are useful, but they may also result in an infinite loop of data creation. Furthermore, in general it is impossible to determine whether an infinite loop truly exists or not. In order to support analysis of the specifications, FORMULA disallows all recur- sive logic programs. Note that it is possible to write logic programs that appear recursive, but can be unrolled into non-recursive logic programs. FOR- MULA supports this form of recursion, but it is beyond the scope of this chap- ter. The non-recursive restriction also means there is always a good evalua- tion order for expressions: 1. Evaluate the expression that has not yet been evaluated and depends on no other expressions. 2. For an expression ei that has just been evaluated, remove all dependen- cies on ei from other expressions ej for j > i. 3. Repeat (1) until no more clauses are left to evaluate.
458 Model-Based Design for Embedded Systems We have presented logic expressions as a convenient way to reuse work, which might give the (wrong) impression that they only serve this purpose. Some queries cannot be expressed without using logic expressions. Here is an example: Is there a state x for which no transition goes to a blocking in state? This query must locate a state x and test that every outgoing transition does not end on a state with no outgoing transitions. Neither a single query nor a boolean composition of queries can keep track of all this information. Instead, an expression is needed that calculates those states that reach a blocking state in one step: blocksOne(x, y) :−x is State, y is State, Transition(x, __, y), fail Transition(y, __, __). The query uses this intermediate data to find states that do not go directly to blocking states: :? x is State, fail blocksOne(x, __). 14.3.6 Domains and Compositions of Domains Bringing these concepts together, a domain D is simply a triple: D = ΥP , ΥR , E (14.33) where ΥP is a signature of primitive function symbols ΥR is a signature of derived function symbols E is a nonrecursive stratified logic program defining the conforms query The set models(D) is the set of all models that satisfy the conforms query: models(D) = X ∈ P(TΥP (Σ)) X satisfies conforms , X is finite. (14.34) This simple semantics admits powerful composition operators for build- ing new domains with known properties. Table 14.1 lists these composition operators. Includes. The includes operator is used to import the declarations of one domain into another domain: domain D’ includes D { . . . }. The resulting domain D has ΥP ⊇ ΥP , ΥR ⊇ ΥR , E ⊇ E[conforms/D.conforms] (14.35)
Semantics of Domain-Speciﬁc Modeling Languages 459 TABLE 14.1 Basic Set of Composition Operators Operator Usage Description includes, restricts, D’ includes D, Imports the declarations of D into D extends operators D’ restricts D, while renaming the conforms D’ extends D, query of D to D.conforms. renaming D as X Produces a new domain from D by operator “as” replacing every occurrence of a function symbol f (. . .) with X.f (. . .) and every query name q with X.q. pseudo-product D1 ∗ D2 Produces a new domain D by combining operator “∗” the specifications of D1 and D2 , and then adding the query (conforms :? D1 .conforms &. D2 .conforms). pseudo-coproduct D1 + D2 Produces a new domain D by combining operator “+” the specifications of D1 and D2 , and then adding the query (conforms :? D1 .conforms XOR . D2 .conforms). The notation E[x1 /x1 , . . . , xn /xn ] denotes the expressions formed by replacing every occurrence of xi in E with xi . Thus, domain D has direct access to the declarations in D, but does not necessarily utilize the conformance rules of D because it is renamed to D.conforms. The includes operation is defined if the signatures of D do not contain contradictory function symbol definitions, and the expressions E are non-recursive and stratified. There are several variants of includes that make stronger statements about D . The restricts keyword requires that no new primitives are introduced in D . Additionally, D.conforms is implicitly conjuncted onto the conforms of D . The restricts operator enforces that models(D ) ⊆ models(D). (14.36) The extends variant implicitly disjuncts D.conforms onto the conforms of D , therefore models(D ) ⊇ models(D). (14.37) Renaming. The renaming operator “as” gives new names to the function symbols and queries in a domain. The expression (D as X) produces a domain D with the same signatures and expressions as D, except that every occurrence of a function symbol and query name is prepended by “X.” Pseudo-product. The pseudo-product operator “∗” is a precursor for building the categorical product of domains. The expression
460 Model-Based Design for Embedded Systems (D1 * D2 ) defines a domain D where Υ P = Υ 1 ∪ Υ 2 , ΥR = Υ 1 ∪ Υ 2 , P P R R E = E1 [conforms/D1 .conforms] ∪ (14.38) E2 [conforms/D2 .conforms] ∪ {conforms :? D1 .conforms & D2 .conforms.} The pseudo-product has the property that if D1 and D2 have disjoint signa- tures and query names, then models(D ) ∼ models(D1 ) × models(D2 ). = (14.39) This is called the categorical product; it means that every model X ∈ models(D ) can be uniquely partitioned into two subsets X1 and X2 so that Xi ∈ models(Di ). This construct is important, because it combines two domains into a larger one while guaranteeing no nontrivial interactions. Pseudo-coproduct. The pseudo-coproduct operator “+” is a precursor for building the categorical coproduct of two domains. The expression (D1 + D2 ) defines a domain D where ΥP = Υ 1 ∪ Υ 2 , ΥR = Υ 1 ∪ Υ 2 , P P R R E = E1 [conforms/D1 .conforms] ∪ (14.40) E2 [conforms/D2 .conforms] ∪ {conforms :? D1 .conforms XOR D2 .conforms.} Let the models(Di ) be the set of all finite syntactic instances that satisfy the conforms query of domain Di . The pseudo-product has the property that if D1 and D2 have disjoint signatures and query names, then models(D ) ∼ models(D1 ) = models(D2 ). (14.41) This is called the categorical coproduct; it means that every model X ∈ models(D ) is either in models(D1 ) or models(D2 ), but never both. Again, this construct is important, because it combines two domains into a larger one while guaranteeing no nontrivial interactions. 14.3.6.1 Properties of Compositions Regardless of the approach, complex modeling processes are often plagued by the nonlocal effects of composition. In our framework, compositions may yield unexpected results because of interactions between declarations and logic programs. A minimum requirement to ensure that composition does not introduce inconsistencies is to check non-emptiness of models(D). The
Semantics of Domain-Speciﬁc Modeling Languages 461 model finding procedure of FORMULA is suited for this task: Perform model finding on the conforms query to check non-emptiness. However, checking non-emptiness of models is only one of the tools available in FORMULA. Many of the composition operators guarantee relation- ships between domains. For example, the composition operators can also be combined to guarantee relationships by construction. For example, given a family of domains (Di )i∈I and an one-to-one renaming function r : I → Σ, the categorical product can always be built by the construction: D1 as r(1) ∗ D2 as r(2) ∗ . . . ∗ Dn as r(n) (14.42) where renaming is used to ensure disjointness of declarations. The categori- cal coproduct can be formed by a similar construction. Figure 14.10 shows the specification of the deterministic finite automaton (DFA) abstraction by restricting the NFA domain. Line 2 declares DFA as a restriction of NFA. Lines 3–6 define the isNonDeter query that is satisfied if there exists a state with two distinct outgoing transitions triggered by the same event. The conforms query is satisfied if isNonDeter is not satisfied. Note that the restricts keyword implicitly conjuncts NFA.conforms onto the conforms query of DFA. 14.3.7 Summary The structural semantics of DSMLs serve as interfaces to the users of model- ing languages and to underlying tool flows. Beyond this, structural semantics facilitate reuse and composition of DSMLs, as we describe in the next sec- tion. Therefore, it is important to formally specify and to provide tool sup- port for analysis of structural semantics. In this section, we have provided a general framework for understanding the relationship between structural semantics (domains), DSMLs, and metamodels. We have also described a concretization of this framework using structured LP with carefully chosen composition operators. This approach allows formal analysis and correct-by- construction of structural semantics. Please see [25] for a complete example, including formal analysis. /// Deterministic Finite Automaton Domain 2. domain DFA restricts (NFA){ 3. isNonDeter :? 4. s is State, t1 is Transition, t2 is Transition, 5. t1.current = s, t2.current = s, t1.trigger = t2.trigger, 6. t1.next != t2.next. 7. conforms :? !isNonDeter. 8. } FIGURE 14.10 DFA as a restriction of NFA.
462 Model-Based Design for Embedded Systems 14.4 Specification of Behavioral Semantics of DSMLs As defined by their structural semantics, models are well-formed struc- tures that can represent domains (in metamodeling) or specific points in domains. While structural semantics of DSMLs are important, they are not sufficient for expressing all essential meanings associated with models. The most important semantic category that needs to dealt with is behavior. For example, in the simplified design flow of embedded controllers (see Fig- ure 14.1), the model of a proportional/integral/derivative (PID) controller [34] would be represented in Simulink R [21] as a structure of simple differen- tiator, integrator, adder, and multiplier nodes that form a point in the domain of all well-formed Simulink(R) Models. At the same time the PID controller has a well-defined dynamics that can be described using different mathe- matical formalisms such as differential equations, an impulse response, or a function in the Laplace domain [34]. In general, behavioral semantics need to be represented as an interpretation of the model in a mathematical domain that is sufficiently rich for capturing essential aspects of the behavior (such as dynamics). Explicit representation of structural and behavioral semantics in DSMLs conforms well to all engineering disciplines where the relationship between structure and behavior is extensively studied. Formalization of these two closely related aspects of modeling enables the exploration of fundamental issues in modeling: 1. DSML composition: Given two DSMLs L1 and L2 with behavioral semantics X and Y and a composition operator ⊕, create a composite DSML with structural semantics (L1 ⊕ L2 ) such that the constraint sys- tem of the composed domain is consistent (the domain of the composed DSML is not empty) and the composed DSML exhibits both X and Y behavioral semantics (there are two behavioral interpretations of the models in the composed DSML). 2. Orthogonality: Given a DSML L = (Υ, RΥ , C, ( struc , X , Y )) with behavioral semantics X and Y and two sets of structural operators opX ∈ OPX and opY ∈ OPY that are structure preserving (whenever a model r is well-formed, the transformed models opX (r) = r and opY (r) = r are also well-formed): ∀r ∈ D(Υ, C) ⇒ (opX (r) ∈ D(Υ, C)), (opY (r) ∈ D(Υ, C)) (14.43) The operators are orthogonal to the behavioral semantics X and Y, respectively, if ∀r ∈ D(Υ, C)) ⇒ ( r X = opX (r) X ), ( r Y = opY (r) Y ) (14.44) 3. Structural/behavioral invariants: The design and verification tasks can be significantly simplified if behavioral properties can be guaranteed
Semantics of Domain-Speciﬁc Modeling Languages 463 by structural characteristics. Discovering and testing these invari- ants requires the precise representation of structural and behavioral semantics. In this section, we describe a method for formalizing behavioral seman- tics based on transformational interpretation. As we discussed before, an inter- pretation is a mapping from the model realizations of one domain to the model realizations of another domain: : RΥ → RΥ (14.45) Assuming that the RΥ target domain has well-defined behavioral seman- tics, the specification of the mapping assigns semantics to RΥ if the mapping is well-defined. In other words, the behavioral interpretation of models in a DSML L requires two distinct components: • A mathematical domain and a formal language for specifying behaviors • A formal language for specifying transformation between domains Selection of the first component largely depends on the goal of the formal specification. If the models represent behaviors that need to be simulated by computers or implemented on computers, selection of operational semantics is the right choice. In programming languages, operational semantics describe how a syntactically correct program is interpreted as sequences of abstract computational steps [17]. These sequences form the meaning of the program. Adopting this definition for the behavioral semantics of modeling languages, operational semantics of a DSML is defined by a model interpretation pro- cess formed by a sequence of abstract computational steps [10,12]. The model interpreter generates behavior from models. While primitive behaviors are described as sequences of computational steps, complex behaviors need to be defined compositionally as the interaction of behaviors of primitive com- ponents. Detailed treatment of this topic is out of scope for this chapter, we refer interested readers to the literature [5,11]. Another relevant method for specifying behavior is denotational semantics. Denotational semantics of pro- gramming languages provide mathematical objects for representing what programs do (as opposed to how they do it) [35]. For example, the Tagged Signal Model (TSM) provides a denotational framework representing sets of possible behaviors as a collection of events [29]. The primary goal of TSM is comparing models of computation and not simulation or code generation. The second component is the specification of transformations between domains. Since these transformations are syntactic operations, their for- mal specifications can be expressed using a logic-based structural semantics foundation [23] or graph transformations [26]. We choose graph transforma- tion specifications because of the availability of high-performance tools [27]. In this chapter, we describe one formalization of behavioral seman- tics based on Abstract State Machines (ASM) [7] and model transforma- tions. We use ASMs for the formal specification of model interpreters and
464 Model-Based Design for Embedded Systems graph transformations to map models specified in various DSMLs into their ASM representation. This process, called semantic anchoring, is supported by an integrated tool suite including the Model Integrated Computing (MIC) tools [27] and the ASML tool suite [18]. We will use a simple example for demonstrating the method. 14.4.1 Overview of Semantic Anchoring The outline above suggests that given a DSML L = Υ, RΥ , C, struc , i i∈I we need to specify for each i ∈ I behavioral interpretation the following: 1. The : RΥ → RΥASML mapping between the RΥ domain of L and the RΥASML domain of an ASM language ASML 2. A model interpreter in ASML While this is certainly possible, the required effort would be significant and in direct conflict with the ultimate goal of DSMLs: rapid formulation and evolution of semantically precise, highly domain specific abstractions. The difficulties are further exacerbated by the fact that specification of the map- ping between the two domains (DSMLs and ASML) requires model transfor- mations that use different formalisms on each side. To mitigate these problems, we have developed a more practical approach to semantic anchoring that enables the reuse of specifications. The approach is based on the recognition that although DSMLs use many dif- ferent modeling abstractions, model composition principles, and notations for accommodating needs of domains and user communities, the funda- mental types of behaviors are more limited. Broad categories of compo- nent behaviors can be represented by behavioral abstractions, such as FSM, Timed Automaton, and Hybrid Automaton. This observation led us to pro- pose a semantic anchoring infrastructure that includes the following ele- ments [12]: 1. Specification of a LSU j set of modeling languages for the basic j∈J behavioral abstractions. We use the term semantic units to describe these languages. The role of the semantic units is to provide a common behav- ioral foundation for a variety of DSMLs (or aspects of DSMLs) that are syntactically different, but semantically equivalent. For example, a number of modeling languages such as IF [37], UPPAAL [4], and Kronos [14] (and many others) have Timed Automata semantics. By specifying a Timed Automata Semantic Unit (TASU) using ASML, we can define semantics for IF, UPPAAL, and Kronos by specifying the transformation between them and TASU (see details in [9]). The clear advantage of this method is that the common semantic domain enables the semantically precise comparison of the different models. 2. Specification of the transformational interpretation T : RΥ → RΥASML between the domains of a DSML L and a selected semantic unit LSU j . j∈J
Semantics of Domain-Speciﬁc Modeling Languages 465 The T transformation “anchors” the semantics of L to the semantic unit LSU . j 3. Since the domain of LSU is a subset of the domain of ASML, we j can exploit this for a further significant simplification. As we discussed in Section 14.2, a domain is defined by a metamodel expressed in a Lmeta metamodeling language. Accordingly, the domain of LSU canj be defined in two alternative forms: (a) using the metamodeling lan- guage that we use for defining domains for DSMLs, or (b) as an Abstract Data Model expressed using the type language of ASML. The conversion between the two representation forms is a simple syntactic transfor- mation. This approach allows us to specify the model transformation T between the DSML and the selected semantic unit such that their domains are specified using the same formalism provided by Lmeta . Figure 14.11 shows our tool suite for semantic anchoring. It comprises (1) the ASM-based common semantic framework for specifying semantic units and (2) the MIC modeling and model transformation tool suites, the Generic Modeling Environment (GME), and Graph Rewriting and Transfor- mation Tool (GReAT), respectively, which support the specification of the transformation between the DSML metamodels and the Abstract Data Mod- els (ADM) of the semantic units. As we discussed above, we selected ASMs, formerly called Evolving Algebras [17], as a formal framework for the specification of semantic units. The ASML tool suite [18] provides a specification language, simulator, test- case generation, and model checking tools for ASMs. GME [27] is employed for defining the metamodels for DSMLs using the Unified Modeling Lan- guage (UML)/OCL-based MetaGME metamodeling language [32,33]. The Model Semantic DSML transform. unit Abstract metamodel specification metamodel data Interpreter model Dr T:Dr DSUj r' DSUj γ' Instance of Generated by Instance Instance of of Semantic Simulator DSML Transf. unit Data model engine model model r Є Dr Model T (r) r' Є DSUj r' checker MIC Tool Suite : GME, GReAT, UDM ASML tool suite FIGURE 14.11 Tool suite for semantic anchoring.
466 Model-Based Design for Embedded Systems semantic anchoring is defined by model transformation rules expressed in the UMT (Unified Model Transformation) language of the GReAT tool suite [26]. In UMT, model transformations are expressed as graph transformations that can be executed (in interpreted and/or compiled form) by the GReAT tool. In summary, semantic anchoring specifies DSML behavioral semantics by the operational semantics of selected semantic units (defined in ASML) and by the transformation rules (defined in UMT). The integrated tool suite enables the simulation of domain models defined in a DSML according to their “reference semantics” by automatically translating them into ASML data models using the transformation rules. In the rest of this section, we show the process of semantic anchoring using a simple example. Readers can refer for detailed discussion about the use of the semantic anchoring tool suite in specifying a TASU in [9], and for specifying semantics for a complex DSML by composing several semantic units in [11]. 14.4.2 Semantic Anchoring Example: Timed Automata Timed Automata [2,3] model the behavior of real-time systems over the pro- gression of time. This formalism extends the definition of state-based transi- tion systems to include a finite set of real-valued clocks that synchronously progress time. The enabling of transitions is further restricted using con- straints over the clock valuations, and transitions can specify a set of clocks to reset to zero upon firing. Timed automata have previously been defined within the semantic anchoring framework [9]; however, the semantic unit included many fea- tures to provide semantic equivalences to other versions of timed automata modeling languages (e.g., UPPAAL [4] and IF [37]). The proposed TASU specified here is intended to be simple while capturing all the basic facili- ties of the original timed automata model. In the AsmL semantic definition, the structures mimic the abstract constructs of the behavioral formalism. The first two sections provide the Abstract Data Model (ADM) and operational semantics that govern a single automaton. The ADM describes the data struc- tures of the semantic unit, and the operational semantics provide a model interpretation over an instance of the ADM, the data model. The succeed- ing sections will explain how automata are composed to form more com- plex systems and then define the modeling language of the semantic unit, Ls , required for semantic anchoring. 14.4.2.1 Timed Automata Overview Structurally, a timed automaton is a mathematical 5-tuple < L, l0 , C, E, Pre > with an event alphabet Σ: 1. L is a finite set of locations. 2. l0 is an initial location, l0 ∈ L.
Semantics of Domain-Speciﬁc Modeling Languages 467 3. C is a finite set of clock variables. 4. E ⊆ L × Σ × 2C × L is a set of edges. An edge < l, α, φ, λ, ω, l > is a transition from l to l on a set of input events α ⊂ Σ and the satisfaction of the guard φ(v) over the valuation function v of the clocks c ∈ C, v : c → N. Upon the firing of a transition, the clocks λ ⊆ C are reset to 0, and the set of output events ω ∈ Σ are generated. 5. Pre : E×Nn → N is a map that assigns to each edge a nonnegative integer priority with respect to a given clock evaluation v, so that Pre (e, v) is the priority of edge e at clock valuation v. Transitions are assigned a priority to model the dynamics of many com- mon real-time systems. This mechanism allows for dynamic priority assign- ment throughout the execution of a model. Following the model of [9], the progression of time is modeled as a transition; therefore, it too must be assigned a priority, the lowest priority in the specification. This supports the notion of urgent transitions; however, unlike [9], this semantic unit does not provide mechanisms for blocking time or most urgent transitions (i.e., the time transition is always enabled). The semantics for a timed automaton fitting the structure above defines the state of a timed automaton as a pair of (l, v) where l is a location in L and v is a valuation of the clocks C. The possible state changes are enabled over the union of location-switching transitions and the progression of time defined respectively as α (l, v) − (l , v[λ := 0]) ⇔ ∃e =< l, α, φ, λ, ω, l >∈ E → such that φ(v) = true and (14.46) ∀e =< l, α, φ , λ , ω , l >∈ E ∧ φ(v) = true ⇒ Pre (e, v) Pre (e , v) t (l, v) − (l , v + ε) ⇒ Pre (e, v + ε) = 0 → (14.47) In the following, we will use AsmL syntax in the specifications. The advantage of this approach is that these specifications are directly executable using the freely available AsmL tools [18] that can be used with the latest Microsoft Visual Studio distributions. 14.4.2.2 Semantic Unit Abstract Data Model In ASML, Events and Clocks (shown in Figure 14.12) are enumerated stores for the defined events (∈ Σ) and clock variables (C) of the automaton. The TimedAutomaton class captures the mathematical model described above for the semantic unit. The id field, present in all following class definitions, pro- vides a naming construct to identify objects, but it has no semantic implica- tions. The initial field holds the initial location of the automaton, and it must
468 Model-Based Design for Embedded Systems 1. enum Clocks 2. enum Events 3. class TimedAutomaton 4. const id as String 5. const locations as Set of Location 6. const initial as Location 7. const transitions as Set of Transition 8. const local_clocks as Set of Clockss 9. var v as Set of Clocks of Clocks to Integer = {− >} 10. var cur as (Location, Set of Events) = ( null, {}) FIGURE 14.12 Structures: Clocks, events, and timed automata. be a predefined location of the system, member of the field locations, or an error will occur. The transitions field holds the set of all defined transitions between the locations of this automaton. The variable v is the valuation of the clock variables in local_clocks. The valuation is a partial function specified as a mapping from the clock domain, C, to the domain of natural numbers, N. Natural numbers were chosen for discrete time steps for clarity. Domain models from a DSML that uses variable discrete time steps can be scaled as required, complicating the operational code. The variable field cur is a 2-tuple indicating the location and set of active events in the current execut- ing step of the simulation. Location and Transition are defined as first-class types (Figure 14.13). Loca- tions contain only the unique identifier, id. Transition defines a move from a location src to a location dst, given the appropriate input events, trigger, and the satisfaction of the time guard condition, φ(v). The variable time_guard is a partial function that maps clock valuations to a Boolean. The time guard must be defined as a variable since the valuation of the clocks v(C) is variable over the progression of time. Upon taking a transition, the event set outputs is added to the set of currently active events. The resets field holds the clocks to 1. class Location 2. const id as String 4. class Transition 5. const id as String 6. const src as Location 7. const dst as Location 8. const trigger as Set of Events 9. const output as Set of Events 10. const resets as Set of Clocks 11. var time_guard as Map of (Map of Clocks to Integer) to Boolean 13. const time = new Transition(“time”, null, null, {}, {time_ev}, {}, {->}) FIGURE 14.13 Structures: Locations, transitions, and time.
Semantics of Domain-Speciﬁc Modeling Languages 469 be reset to zero upon taking the transition. According to the original model, the progression of time is enabled in every state of a timed automaton; there- fore, the time transition is defined as a constant. If the time transition is taken, all clocks in the timed automaton will be incremented by some value ∈ N that must be defined for the model. Note that the time transition has an out- put event, time_ev. This event must be included in the data model definition. 14.4.2.3 Operational Semantics As is the case for all MIC semantic units, the operational semantics of the timed automaton semantic unit are specified as a set of ASML rules that exe- cute over models instantiated using the ADM data structures. A global function InputEvents provides an interface to continue the execu- tion of a model within the AsmL tools, that is, it provides a means to drive the simulation. This method receives an input parameter set of TimedAutoma- ton objects, and should return a set of Events to serve as input to the current simulation step. It must be provided by the consumer of the semantic unit (i.e., the simulation environment). The InitializeTA method (shown in Figure 14.16) first initializes the cur variable to the initial location and an empty active event set, and then sets the valuation of all local clock variables to zero. The set of currently enabled transitions returned by the EnabledTransitionsTA method is the time transition added to the set of transitions that meet the enabling conditions: the source location of the transition is the current location, the triggering events of the transition are a subset or equal to the set of currently active input events, et.trigger 0 | clki in (tr.resets intersect local_clocks) } 6. union {clki − > v(clki) | 7. in local_clocks -(tr.resets intersect local_clocks) } FIGURE 14.14 Execution: Stepping a timed automaton.
470 Model-Based Design for Embedded Systems and must set the time_ev event as the only active event for the given automa- ton. The UpdateEvents and GetEvents methods are self-explanatory. The Prior- ityTA and UpdateTimeGaurdTA methods are not predefined functions as they are model dependent. Each must be specified when simulating an instance model of a DSML. The PriorityTA method returns a nonnegative integer value for each tran- sition in the system with the base priority being 0, that of the time transition. Returning identical priorities for multiple transitions allows for nondeter- minism in the data models. The UpdateTimeGuardTA method reevaluates the guard condition of every transition given the current valuation of the clocks. The time tran- sition’s time guard is never included in this method since it is always an enabled transition. 14.4.2.4 Composition of Timed Automata The timed automaton semantic unit presented thus far describes the behav- ioral semantics and data structures of a single automaton. To model larger, more complex systems and behaviors, the semantic unit needs to be extended to model concurrently executing automata. Here, we show the synchronous parallel execution semantics for multiple automata and provide the appro- priate metamodel for the TASU. The modeling of concurrent automata was previously approached in [9]; however, the resulting semantic unit appeared overly complex and insufficiently expressive. These issues motivated this new specification that is intended to be simpler and extensible to a wider variety of execution semantics. The set of globally scoped clocks, global_clocks, is a set of clocks that all automata can read and possibly reset. Conversely, the set of clocks in the TimedAutomaton class, local_clocks, is scoped exclusively to its respective automaton. The variable g_v is the partial function that maps the global clock variables to their valuations. Figure 14.15 contains the ASML structures for a global system definition. The class Comp_System (Figure 14.15) contains the set of concurrently exe- cuting TimedAutomaton objects and a variable E. E represents the set of all 1. const global_clocks as Set of Clocks 2. var g_v as Map of Clocks to Integer = {clki − > 0 | clki in global_clocks} 4. class Comp_System 5. const TA_components as Set of TimedAutomaton 6. var E as Set of Events = {} FIGURE 14.15 Execution: ASML structures supporting concurrent composition of indepen- dent timed automata.
Semantics of Domain-Speciﬁc Modeling Languages 471 1. class Comp_System 2. InitializeCS_TA() 3. forall c in TA_components 4. require {t} intersect {tr.resets | tr in c.transitions} = {} 5. require c.local_clocks intersect global_clocks = {} 6. require c.local_clocks intersect {h.local_clocks | h in TA_components 7. where h c} = {} 8. c.InitializeTA() 10. UpdateEventsCS_TA() 11. let e = E union InputEvents(TA_components) 12. E := e 13. forall c in TA_components 14. c.UpdateEvents(e) 16. UpdateTimeGuardCS_TA() 17. forall c in my_sys.TA_components 18. c.UpdateTimeGuardTA() FIGURE 14.16 Execution: Initialization and update for noninteracting concurrent timed automata. active events in the composed system. This composition does not restrict or scope events that an automaton can see; therefore, events generated from one automaton will be visible for all other automata in the composed system as well. The InitializeCS_TA method invokes the InitializeTA method for each TimedAutomaton object in the composed system after it checks constraints that are placed on the clock variables (Figure 14.16). First, in the composed system, the clock variable t is the system clock and is not allowed to be reset. The next two constraints ensure that no clock is defined both globally and locally and that no clock is defined as local to multiple automata. The Upda- teEventsCS_TA method must correctly update the global set of active events for all TimedAutomaton objects in the system. Remember, all of the automata see the same set of active events (i.e., there is no scoping of local events ver- sus global events). Still, this could be extended to allow event scoping in the semantics of other variations of a composed system. The UpdateTime- GuardCS_TA method simply calls the UpdateTimeGuardTA method for each TimedAutomaton. The TimeProgressCS_TA and EvolveCS_TA methods (shown in Figure 14.17) are responsible for changing the state of the system for every execu- tion step. Along with calling the TimeProgressTA method for each automa- ton, TimeProgressCS_TA must increment all global clock valuations by the defined constant . This method is only called if all automata in the sys- tem have elected to take the time transition in this step. The EvolveCS_TA method takes as input each timed automaton in the system with its respec- tive highest priority currently enabled transition. ev and nev are initialized to
472 Model-Based Design for Embedded Systems 1. class Comp_System 2. TimeProgressCS_TA() 3. g_v := {clki -> g_v (clki) + epsilon | clki in global_clocks} 4. forall c in TA_components 5. c.TimeProgressTA() 7. EvolveCS_TA(cT as Set of (TimedAutomaton, Transition)) 8. let ev = {k | k in cT where k.Second time} 9. let nev = {l | l in cT where l.Second = time} 10. let gr = BigUnion({ h.Second.resets | h in ev}) 12. g_v := {clki -> 0 | clki in ( gr intersect global_clocks) } 13. union { clki -> g_v (clki) | clki in global_clocks 14. - ( gr intersect global_clocks)} 16. forall m in ev 17. m.First.EvolveTA(m.Second) 18. forall n in nev 19. n.FirstUpdateEvents({}) FIGURE 14.17 Execution: Progress for global time and individual automata. the automata that will take a non-time transition in this step and those that will not, respectively. The automata in nev indicate that their highest prior- ity transition is the time transition; however, all other automata (specified in ev) do not agree so the time transition will not be taken. If a transition is not taken by an automaton, the set of active output events for that automa- ton are cleared. Given the automata that will be taking a non-time transition, the method must also reset global clocks specified in the resets field of the enabled transitions. The EvolveTA method of each automaton will reset the local clocks. Accordingly, the EvolveTA method is called for each automaton in the set ev. The RunCS_TA method provides a single execution loop for the com- posed system (Figure 14.18). First, each automaton of the composed sys- tem must be initialized. Notice that the variable count restricts the number of execution steps of the loop and has no semantic meaning for the system. During each iteration of the execution loop, the active event set is updated (UpdateEventsCS_TA method) to include the events generated from the last set of transitions, initially held in E, joined to the events returned from the InputEvents method. Also, all time guards must be reevaluated given the resulting system state from the last execution step. Following these updates, the set of enabled transitions for all automata can be determined. First, the set of all enabled transitions for each automa- ton are stored in eT in the anonymous 2-tuple of type . Next, the set of enabled transitions for each automaton is reduced to a single transition that has the highest priority of all enabled transitions. This reduction is nondeterministic if multiple enabled transi- tions have the highest priority value. Time will progress only if all automata
Semantics of Domain-Speciﬁc Modeling Languages 473 1. class Comp_System 2. RunCS_TA() 3. Var_ count = 1 4. step my_sys.InitializeCS_TA() 5. step while count < 35 6. step 7. UpdateEventsCS_TA() 8. UpdateTimeGuardCS_TA() 9. step 10. let eT = {(ta, ta.EnabledTransitionsTA()) | ta in TA_components} 11. let eT2 = {(b.First, (any h | l in b.Second where 12. b.First PriorityTA(h) = (max b.First.PriorityTA(tp) 13. | tp in b.Second))) | b in eT} 14. if {b2.Second | b2 in eT2} = {time} then 15. TimeProgressCS_TA() 16. else 17. EvolveCS_TA(eT2) 18. step 19. E := BigUnion({ c.GetEvents()| c in TA_Components}) 20. count := count + 1 21. FIGURE 14.18 Execution: Global coordination code. indicate that the time transition should be taken; otherwise, eT2 is passed to EvolveCS_TA. Following either action (time progress or taking other transi- tions) all generated events from each automaton in the composed system are collected and stored in the variable field E. 14.4.2.5 TASU Modeling Language Within the MIC semantic anchoring framework, model transformations between metamodels of a given DSML and the TASU specifies the anchoring of the DSML to the TASU. In order to connect the ASML and the MIC tool suites, we must represent the TASU ADM as a MIC metamodel (expressed in MetaGME) and must implement a translator that translates MIC model instances into ADM model instances. Figure 14.19 shows the metamodel of the TASU specified in the MetaGME metamodeling language [22] of the MIC tool GME. The metamodel in Figure 14.19 captures the Abstract Data Model of the TASU. Note that the metamodel includes Constant and Variable objects for defining model-dependent data. The remaining piece of the TASU is a model translator that generates the ASML of data models from timed automata models created in the MIC tool suite. Since these time automata models are instances of the TASU Metamodel as well as the TASU ADM on the ASML side, the translator is a simple XML parser.
474 Model-Based Design for Embedded Systems Event System Clock 0..x 0..x 0..x Constant Transition x 0..x Type : field 0.. Value : field TimedAutomaton output : field resets : field x 0.. Variable trigger : field time_guard : field Priority : field x Type : field 0.. Value : field 0..x dst 0..xsrc 0..x Initial Location 0..x FIGURE 14.19 Metamodel for our timed automata abstract data model. 14.4.2.6 Semantic Anchoring Example: The Timing Deﬁnition Language The timing definition language (TDL) [16,36] provides a high-level pro- gramming abstraction that allows distributed real-time system designers to describe the temporal behavior of components apart from their functional code and deployment/configuration concerns. This timing model is based on logical execution time (LET) introduced by the Giotto modeling lan- guage [20]. TDL preserves many other artifacts of Giotto, but some syntactic and semantic differences remain. This case study will capture the timing behavior of a TDL application by anchoring a TDL modeling language to the TASU. For simplicity, in this example, all TDL communication artifacts will be excluded from the map- ping since they have no effect on the temporal behavior of a TDL application. In Giotto [20] a system is defined over a set of nonconcurrent modes, each of which contains periodically executing activities and a communica- tion topology description. The periodic activities, task invocations under LET semantics, actuator updates, and mode switches, all conditionally execute a finite number of times, their frequency, within the mode’s cyclic execution period. A task’s timed execution cycle is initiated by a release for scheduled execution and finished by a completion event at time after the release. Actua- tor updates and mode switches are considered synchronous activities; there- fore, they take zero logical time to execute. In TDL [16] the notion of a mode is preserved; however, the model is extended to include a module, a TDL component. A module encapsulates
Semantics of Domain-Speciﬁc Modeling Languages 475 what is characterized as a Giotto system, and a TDL system is defined as a set of modules and communication networks between them. Like Giotto, the modes within a single module do not execute concurrently; however, modules of a TDL system execute in parallel. 14.4.2.7 Anchoring the TDL Modeling Language to the TASU Figure 14.20 shows an abbreviated metamodel for the TDL modeling lan- guage. The full metamodel contains data handling mechanisms, such as ports and drivers; however, these omitted artifacts do not affect the tim- ing behavior of a TDL application. Notice that the ModeSwitch class inherits from the abstract class Periodics. The attribute frequency that ModeSwitch now contains will be ignored in the transformation since nonharmonic mode switches are not allowed in TDL unlike Giotto [20]. The TaskReference class is used to copy a previously defined Task into a new mode that may define a different frequency value for the TaskReferemce versus the original Task object’s frequency. The model transformation that provides the anchoring across the meta- models is specified in the UMT language of the MIC tool GReAT [26]. The transformation is given by a set of rules that define the mapping between the TDL metamodel and the TASU metamodel. The transformation takes a TDL System Module 0..x 0..x Mode ModePeriod: field StartMode: bool 0..x Periodics Frequency: field DriverFunction: field Task TaskReference ModeSwitch FIGURE 14.20 TDL MetaGME Metamodel (abbreviated).