ࡱ> hjcdefgE@ 0bjbj )}/  HHH8$/41lA"T$ R] -/[1//E:aIaIaI/Z |(aI/aIaIiJv·, $Hq<j,0/@ri?Bi,if##2&HaI)*4###1QDDD;?I"QAn Abstract Communication Model Uwe Glsser, Yuri Gurevich and Margus Veanes May 2002 Technical Report MSR-TR-2002-55 Microsoft Research Microsoft Corporation One Microsoft Way Redmond, WA 98052 Abstract We present an abstract communication model. The model is quite general even though it was developed in the process of specifying a particular network architecture, namely the Universal Plug and Play (UPnP) architecture. The generality of the model has been confirmed by its reuse for different architectures. The model is based on distributed abstract state machines and implemented in the specification language AsmL. Keywords: Distributed Systems, Computer Networks, Communications Software, Requirements Specification, Systems Modeling, Rapid Prototyping Introduction The group on Foundations of Software Engineering at Microsoft Research  REF _Ref9559788 \r \h  [16] has developed a high-level executable specification language AsmL  REF _Ref9560551 \r \h  [2] based on the concept of abstract state machine or ASM  REF _Ref535815723 \r \h  [21]. AsmL is integrated with Microsoft s software development, documentation and runtime environments. AsmL supports specification and rapid prototyping of object oriented and component oriented software. It is a successful practical instrument for systems design (and reverse engineering). ASMs are able to simulate arbitrary algorithms in the step-for-step manner. There is a substantial experimental confirmation  REF _Ref8441174 \r \h  [1] REF _Ref9559788 \r \h  [16] as well as theoretical confirmation  REF _Ref5622720 \r \h  [6] REF _Ref535816125 \r \h  [22] of that ASM thesis. ASMs have been used to specify various architectures, protocols and numerous languages, in particular C  REF _Ref9563257 \r \h  [20], Java  REF _Ref526062066 \r \h  [30], SDL  REF _Ref535385772 \r \h  [15] and VHDL  REF _Ref526062086 \r \h  [8]. The International Telecommunication Union adopted a comprehensive ASM-based formal definition of SDL as an integral part of the current SDL standard  REF _Ref515900185 \r \h  [28]. AsmL specifications look like pseudo code over abstract data structures. As such, they are easy to read and understand by system engineers and program developers. Practical experiences with industrial applications helped to establish a pragmatic understanding of how to model complex system behavior with a degree of detail and precision as needed  REF _Ref526065198 \r \h  [7] REF _Ref8545287 \r \h  [8]. Some features of high-level rigorous specifications are well recognized in the academic community as advantageous. While informal documentation is often ambiguous, incomplete and even inconsistent, properly constructed formal specifications are consistent, avoid unintended ambiguity and are complete in the appropriate sense that allows for intended ambiguity (nondeterminism). Let us emphasize though that in practice formal specifications build on given informal descriptions. You fix loose ends, resolve unintended ambiguities and inconsistencies, separate concerns, etc. Gradually the given informal description gives rise to a mathematical model or to a hierarchy of such models. Some other features of high-level rigorous specifications are more controversial. We advocate AsmL specifications that are executable and written in the style of literate programming so that they are easy to comprehend; see examples at  REF _Ref9560551 \r \h  [2]. AsmL is used to explore and test the design, to validate the specification itself, and to test the conformance of the implementation to the specification. In particular, executable specifications are used for test-case generation  REF _Ref9852754 \r \h  [25] and runtime verification  REF _Ref9564451 \r \h  [3]. And there are features of high-level rigorous specifications, at least of ASM specifications, that have not been given sufficient attention. An ASM model is a closed world with well delineated interfaces to the outside world. The need to make that world closed provokes one to fill various gaps in a given informal spec. That is what happened when we worked on the Universal Plug and Play (UPnP) architecture  REF _Ref6385476 \r \h  [17]. While the informal documentation described UPnP devices and the UPnP protocol, it did not provide a conceptual model of the network. We had to construct such a model. It turned out to be general and was reused on several occasions. The communication model partitions the whole system into a collection of communicating subsystems. The particular subsystems change from one project to another but the communication structure is the same. In particular, the communication model was reused in our work on XLANG  REF _Ref9564844 \r \h  [36] where the documentation given to us was partially formal but did not address the communication model. In this paper, we present our communication model and illustrate it on the examples of UPnP and XLANG. As far as domain specific languages  REF _Ref525673966 \r \h  [14] are concerned, our work fits in well, the specific domain being Software Architecture Description. We try to make this paper self-contained. In Section  REF _Ref8547871 \r \h  2, we recall some basic definitions on abstract state machines (ASMs) and in particular distributed abstract state machines (DASMs). In Section  REF _Ref9853040 \r \h  3, we describe a portion of AsmL sufficient for our purposes in this paper. The abstract communication model is described in Section  REF _Ref9853287 \r \h  4. The abstract communication model is reused in both Section  REF _Ref8547211 \r \h  5, where we describe the UPnP model, and in Section  REF _Ref9853477 \r \h  6, where we describe the XLANG model. In Section  REF _Ref9611724 \r \h  7 we discuss the classification of AsmL as a software architecture description language.  Abstract State Machines Our method rests on the ASM theory. Here we give a quick description of ASMs sufficient for our purposes in this paper. The interested reader may want to consult  REF _Ref5622720 \r \h  [6] REF _Ref9825688 \r \h  [22] REF _Ref9759101 \r \h  [23]. Basic ASMs A basic ASM consists of a basic ASM program together with a collection of states (the legal states of the ASM) and subcollection of initial states. First we describe basic ASM states and then define basic ASM programs. Basic ASMs are sequential algorithms. Intuitively sequential algorithms are non-distributed algorithms with uniformly bounded parallelism. The latter means that the number of actions performed in parallel is bounded independently of the state or the input. The notion of sequential algorithms is formalized in  REF _Ref9759101 \r \h  [23] where it is proved that, for every sequential algorithm, there is a basic ASM that simulates the algorithm step for step. States The notion of ASM state is a variation of the notion of (first-order) structure in mathematical logic. A vocabulary is a collection of function symbols and relation symbols (or predicates); each symbol has a fixed arity (the number of arguments). Symbols split into dynamic and static. Every vocabulary contains (static) logic symbols true, false, undef, the equality symbol, and the standard propositional connectives. A state A of a given vocabulary is a nonempty set X (the base set of A), together with interpretations of the function symbols (the basic functions of A) and the predicates (the basic relations of A). A function (respectively relation) symbol of arity j is interpreted as a j-ary operation (respectively relation) over X. A nullary function symbol is interpreted as an element of X. The logic symbols are interpreted in the obvious way. The value undef is the default value for basic functions. Formally a basic function f is total but intuitively it is partial. The intended domain of f consists of all tuples a with f(a) `"undef. Every state includes an infinite "naked" set called the reserve. The role of reserve will become apparent later. The default value for relations is false. We think of a j-ary relation R as a set of j-tuples of elements. Remark. Traditionally, in logic, true and false do not belong to the base set, and so there is a principal difference between basic functions (taking values inside the structure) and basic relations (taking values outside). In our framework, basic relations are seen as special basic functions whose only possible values are true and false and whose default value is false rather than undef. This simple definition of state is very general. Any kind of static mathematical reality can be described as a first-order structure. Second-order and higher-order structures of logic are special first-order structures. Many-sorted first-order structures (with several base sets called sorts) are special one-sorted structures; the roles of sorts are played by designated unary relations which are called universes in the ASM literature. Notice that ASM universes may be dynamic. Example 1. The vocabulary consists of one static unary predicate Scandinavia and one dynamic binary predicate Flight. (In addition, it contains the logic symbols but it is customary to ignore the logic symbols, their interpretation and the reserve in the descriptions of states.) The base set of our state consists of three airports ARN, CPH and SEA. The unary relation Scandinavia contains ARN and CPH but not SEA. The relation Flight is this {(ARN,CPH),(CPH,ARN),(CPH,SEA),(SEA,CPH)} The intended meaning is that there are direct flights (of some fixed airline) from ARN to CPH, from CPH to ARN, etc., but there are no direct flights between ARN and SEA. Updates We view a state as a kind of memory. Dynamic functions are those that can change during computation. A location of a state A is a pair l = (f, (x1,, xj)) where f is a j-ary dynamic function (or relation) symbol in the vocabulary of A and (x1,, xj) is a j-tuple of elements of A. The element y = f(x1,,xj) is the content of that location. An update of state A is a pair (l, y'), where l is a location (f, (x1,, xj)) of A and y' is an element of A; of course y' is true or false if f is a predicate. To fire the update (l, y'), replace the old value y = f(x1,, xj) at location l with the new value y' so that f(x1,, xj) = y' in the new state. Intuitively, one may view dynamic functions as being represented by function tables that can be updated dynamically at run time. The effect of the update instruction above is illustrated in  REF _Ref9855617 \h Figure 1; the new content y' is replaced by the old content y of location l.  Figure  SEQ Figure \* ARABIC 1. Function update A set S = {(l1, y'1), ..., (ln, y'n)} of updates is consistent if the locations are distinct. In other words, S is inconsistent if there are i, j such that li = lj but y'i is distinct from y'j. To fire a consistent set of updates, fire all the updates at once; to fire an inconsistent update set, do nothing. Rules and Programs Expressions are defined inductively. If f is a j-ary function symbol and e1,..., ej are expressions then f(e1,..., ej) is an expression. (The base of induction is obtained when j = 0.) If f is a predicate then the expression is Boolean. An update rule R has the form f(e1,...,ej) := e0 where f is a j-ary dynamic function symbol and each ei is an expression. (If f is a predicate then e0 should be a Boolean expression.) To execute R, fire the update (l, a0) where l = (f, (a1,..., aj)) and each ai is the value of ei. A conditional rule R has the form: if e then R1 else R2 where e is a Boolean expression and R1, R2 are rules. To execute R, evaluate the guard e. If e is true, then execute R1; otherwise execute R2. A do-in-parallel rule R has the form do in-parallel R1 R2 where R1, R2 are rules. To execute R, execute rules R1, R2 simultaneously. An import rule R has the form import x R1(x) To execute R, fish out any element x of the reserve and execute the rule R1(x). A program (that is a basic ASM program) is just a rule. An ASM is given by a program, a collection of legal states and a subcollection of initial states. Note that the program described just one step of the ASM. It is supposed to be executed until if ever the state does not change. Example 1 (continuation). The following rule reflects that direct flights have been established between ARN and SEA. do in-parallel Flight(ARN,SEA) := true Flight(SEA,ARN) := true Parallel ASMs We generalize the definition of basic ASMs in a two directions. First, we enrich the notion of expression. {t(x) | x "s where (x)} is an expression (a comprehension expression) denoting the set of all values t(x) where x ranges over those elements of set s that satisfy (x). This presumes that s is a set expression and (x) is Boolean. We require that every state A is closed under tuples and (finite) sets: if a1,..., an are elements of A then the tuple (a1,..., an) and the set {a1,..., an} are elements of A. We require also that A contains the standard operations over tuples and sets, e.g. the set pairing operation {e1, e2}. Remark. We often require also that the states are closed under finite partial maps but the set background is sufficient for theoretical purposes  REF _Ref5622720 \r \h  [6]. Second, we enrich the notion of rules. A do-forall rule R has the form forall x "s R1(x) where R1(x) is a rule and x does not occur freely in the expression r. To execute R, execute all subrules R(x) with x in s at once. Parallel ASMs are parallel algorithms. The appropriate notion of parallel algorithms is formalized in  REF _Ref5622720 \r \h  [6] where it is proved that, for every parallel algorithm, there is a parallel ASM that simulates the given algorithm step for step. Nondeterministic ASMs Basic and parallel ASMs can be made nondeterministic by the use of external basic functions. For example, an ASM can employ a function Input operated by the user. It is convenient though to have explicit nondeterminism. To this end, we enrich parallel ASMs with choose rules. A choose rule R has the form choose x ( s R1(x) where R1(x) is a rule and x does not occur freely in the set expression s. To execute R, choose any element x of s and execute the subrule R1(x). Example 1 (continuation). Imagine that, for some reason, you want to remove all direct flights between SEA and one of the Scandinavian airports. The following rule accomplishes that. choose x ( {ARN,CPH} Flight(SEA, x) := false Flight(x, SEA) := false Distributed ASMs Until now, we dealt with one-agent ASMs. A distributed ASM (DASM) involves a collection of agents. Mathematical abstraction allows us to speak about global states of a DASM even though different agents may live on different computers. In a global state, the agents interact by reading from and writing into "shared" locations of the global state; potential read-write and write-write conflicts are resolved according to the definition of partially ordered runs below. Agents are represented in global states as well. They are elements of a dynamically universe Agent that may grow and shrink. With each agent we associate a program defining its behavior. A static universe Program abstractly represents the set of all agent programs collectively forming the distributed program of A. Agents may perform their computation steps concurrently. A single computation step of an individual agent is called a move of this agent. Formally, a run ( of a distributed ASM A is given by a triple (M, (, () satisfying the following four conditions: M is a partially ordered set of moves where each move has only finitely many predecessors. ( is a function on M associating agents with moves such that the moves of any single agent of A are linearly ordered. ( assigns a state of A to each initial segment Y of M, where ((Y) is the result of performing all moves in Y; ((Y) is an initial state if Y is empty. The coherence condition: If x is a maximal element in a finite initial segment X of M and Y = X {x} then ((x) is an agent in ((Y) and ((X) is obtained from ((Y) by firing ((x) at ((Y). Intuitively, a run can be seen as the common part of histories of the same computation recorded by various observers. See  REF _Ref9825688 \r \h  [22] for further details. Example 2. We illustrate the coherence condition in a simple situation. Suppose that we have only two propositional variables (dynamic nullary relation symbols) door and window. Intuitively door = true means that "the door is open" and window = true means that "the window is open". Imagine now two distinct agents: a door-manager (agent d) and a window-manager (agent w). The program of the door-manager is to open the door if the window is closed (move x). The program of the window-manager is to open the window if the door is closed (move y). Programd = if (window then door := true Programw = if (door then window := true Assume that initially (in state S0) both the door and the window are closed. Then there are only two possible runs, and in each run only one of the agents makes a move. Indeed, we cannot have x < y because w is disabled in the state S1 obtained from S0 by performing x. Similarly we cannot have y < x because d is disabled in the state S2 obtained from S0 by performing y. Finally, we cannot have a run where x and y are incomparable, that is neither x < y nor y < x. By the coherence condition, the final state S3 of such a run would be obtained from S1 by performing y which is impossible. (It would also be obtained from S2 by performing x which is equally impossible.) From Abstract State Machines to AsmL To actually program ASMs in industrial environment, we need an industrial-strength language. One such language has been (and is being) developed in Microsoft Research. It is called AsmL (ASM Language). Here we focus on those aspects of AsmL that are most important for the general understanding and that are actually used in this paper. The description given here is incomplete in many respects. For an in-depth introduction to AsmL, we recommend the reader to consult  REF _Ref9560551 \r \h  [2]. First we explain how the fundamental modeling concepts of ASMs are realized in AsmL. Then we introduce additional functionality into the modeling framework that enables us to faithfully simulate distributed ASM agents; such simulation is needed because the current version of AsmL lacks runtime support for true concurrency or simulation of true concurrency. Remark. There is a fair amount of freedom in AsmL regarding the representation of ASM functions and domains. The reader should keep in mind that the particular choice of representation is often a matter of taste, readability and a way to control how the model is executed, and does not affect the underlying ASM semantics. Types Some ASM universes give rise to types in AsmL. Other universes are represented as (finite) sets; some examples are found below. An AsmL model may first declare an abstract type C and later on concretize that type into a class, a structure, a finite enumeration, or a derived type. type C class C AsmL has an expressive type system that allows one to define new types using (finite) sets, (finite partial) maps, (finite) sequences, tuples, etc., combined in arbitrary ways. For example, if C and D are types then the type of all maps from C to sets of elements of D is this. Map of C to Set of D Finite sets, sequences, maps are ordinary elements. The common operations on sets, sequences, maps and other built-in data types are available as built-ins, for example the binary operation apply(f, a) applies a map f to an element a. The shorthand notation for map application is f(a). Derived Functions Derived functions play an important role in applications of ASMs. A derived function does not appear in the vocabulary; instead it is computed on the fly at a given state. In AsmL, derived functions are given by methods that return values. A derived function f from C0(C1( ... (Cn to D can be declared as a global method. f(x0 as C0, x1 as C1, ..., xn as Cn) as D The definition of (how to compute) f may be given together with the declaration or introduced later on in the code. Alternatively, if C0 is a class (or a structure) then f can be declared as a method of C0. Notice that n can be 0. class C0 f(x1 as C1,...,xn as Cn) as D A nullary derived function can be introduced as a global method that takes no arguments. For example z() as Integer return e where e is evaluated in a given state. Constants A nullary function that does not change during the evolution can be declared as a constant. z as Integer = 0 A unary static function from a class C to D can be declared as a constant field of C as in following example. class C id as String Variables There are two kinds of variables, global variables and local variable fields of classes. Semantically, fields of classes are unary functions. var b as Boolean class C var f as Integer Notice that f represents a unary dynamic function from C to integers. Dynamic functions of ASMs are represented by variables in AsmL. A dynamic function f from C1 ( ... ( Cn to D of any positive arity n can be represented as a variable map in AsmL. var f as Map of (C1, ..., Cn) to D With the map representation, a normal ASM update f(c) := b corresponds to a partial update of the map variable f. A set of consistent ASM updates to f corresponds to a set of consistent (non-conflicting) partial map updates that are combined into a single total update of f. We do not use partial updates on maps in this paper. The theory of partial updates is developed in  REF _Ref238236 \r \h  [23]. Classes and Dynamic Universes AsmL classes are special dynamic universes. Classes are initially empty. Let C and D be two dynamic universes such that C is a subset of D and let f be a dynamic function from C to integers. class D class C extends D var f as Integer The following AsmL statement adds a new reserve element c to C and D and initializes f(c) to the value 0. let c = new C(0) Classes are special dynamic universes in that one cannot programmatically remove an element from a class. In general, classes cannot be quantified over like sets (given by expressions) but it is possible to check whether a given element is of type C by using the is keyword. if x is C then ... In order to keep track of elements of a class C, one can introduce (essentially an auxiliary dynamic universe represented by) a variable of type set of C that is initially empty. var Cs as Set of C = {} Set-valued variables can be updated partially by inserting and removing individual set members. Several such pairwise non-conflicting partial updates (i.e. you don't both insert and remove the same element) are combined into a single total update at the end of the step. let c = new C(0) Cs(c) := true //insert c into Cs Sets (given by expressions) can be quantified over like in the following rule where all the invocations of R(x), one for every element x of the set s, happen simultaneously in one atomic step. forall x in s R(x) Simulation of Agents Ideally one would like to have a distributed runtime environment for running distributed ASMs. The current version of AsmL doesn't have yet runtime support for true concurrency or simulation of true concurrency. Therefore we have to build functionality for simulating concurrent agents into our model. This is how we do it. Agents are introduced through a class Agent. To keep track of the currently active agents, a variable Agents of type set of Agent is updated each time an agent is created or discarded. class Agent var Agents as Set of Agent = {} Each agent (more exactly, its state) evolves in sequential steps with each invocation of its Program. Each agent a has a mailbox of messages and a method InsertMessage that is used by other agents to send messages to a. type Message class Agent Program() var mailbox as Set of Message = {} InsertMessage(m as Message) mailbox(m) := true Several agents may simultaneously insert messages into the mailbox of a. This will not cause a conflict in updating the mailbox of a because these updates are partial. The method RunAgents gives the operational semantics of a single step of the top-level system, in the definition of which chooseSubset selects nondeterministically a subset of the active agents. Thus, at each global step of the system, some, none or all of the active agents in the system may perform a step. RunAgents() forall a in chooseSubset(Agents) Program(a) Abstract Communication Model It is not clear how to deal with the network in a sufficiently abstract and general way. This problem came up in a number of our projects, initially in the UPnP project. To solve this problem, we introduced a special category of agents which we call communicators. Each communicator represents a part of the communication network. Intuitively different communicators represent disjoint subnets, and typically this is indeed the case. But we don't impose this restriction. class COMMUNICATOR extends Agent The communicators transfer messages between applications running on hosts connected to the network. Thus, one can think of communicators as an abstract kind of "router" of messages. However, the term "router" used in this sense is much more general than the corresponding TCP/IP term. class APPLICATION extends Agent Our communication model is a distributed ASM. It was obtained by an abstraction of TCP/IP networks  REF _Ref9399949 \r \h  [13]. The multitude of communicators reflects the fact that a TCP/IP network consists of distinct interconnected physical networks. We abstract from routing details. The communicators transfer messages between applications.  REF _Ref9859595 \h Figure 2 is a sketch of an instance of the abstract communication model. We emphasize that, even though the model was obtained by abstraction from TCP/IP networks, it is independent from TCP/IP and is used to deal with very different networks.  The whole system, applications and communicators, operates in some external environment which may affect the system in various ways. For example, it may change the system configuration by creating and removing agents. It may also affect the communication load of the network which affects message delays. Those external environmental actions and events are unpredictable as far as the system is concerned. Communicators are nondeterministic in two ways. There is an internal nondeterminism that reflects abstraction of various details of routing. In addition, there is environment-induced nondeterminism that may cause e.g. that some messages are lost. For example, in the case of UPnP, one uses the TCP protocol, which is reliable, and the UDP protocol, which is not reliable. It is the responsibility of an application to tolerate the non-reliable behavior of the network. In the following subsections, we discuss the various aspects of the communicator's operation and then present the main program that integrates these aspects. Message Transformation Not all messages have a single recipient. Some messages are intended to be sent to many recipients. However, multicasting is just one example of a general class of message processing. Other transformations include incrementing a hop count for time-to-live calculations and encryption. The ResolveMessage method transforms a message (an inbound message of the communicator) into a set of messages (outbound messages of the communicator). For example, the transformation may involve adding or removing header information or converting a multicast message into separate unicast messages. The model places no restriction on the kind of transformation performed in this step. It is even possible that a transformation may discard a message completely, by returning an empty set. type MESSAGE class COMMUNICATOR ResolveMessage(m as MESSAGE) as Set of MESSAGE In the TCP/IP world, addressing mechanisms classify as unicasting, broadcasting or multicasting where multicasting can be viewed as the most general one  REF _Ref9399949 \r \h  [13]. In our model, a multicast can involve any set of applications that are reachable over the network; in principle every such set of applications may have an address. The receiver addresses of a multicast message can themselves be multicast addresses. An addressTable of a communicator is a (possibly dynamic) mapping whose domain consists of the addresses a of some multicast groups (that the communicator can deal with). If a is the address of a multicast group g then addressTable(a) is a set that consists of the addresses of some multicast subgroups of g which could be singleton groups. The union of all the subgroups is g itself. type ADDRESS class COMMUNICATOR var addressTable as Map of ADDRESS to Set of ADDRESS The address table is used in the process of resolving an inbound message into a set of transformed outbound messages. destination(m as MESSAGE) as ADDRESS class COMMUNICATOR Transform(m as MESSAGE, dest as ADDRESS) as MESSAGE ResolveMessage(m as MESSAGE) as Set of MESSAGE return {Transform(m,a) | a in addressTable(destination(m))} Message Routing Communicators determine the recipient of a message. Presumably, this is done by examining addressing information in the headers and reconciling that information with the communicator's knowledge of network topology. The Recipient method of a communicator identifies which agent would receive an outbound message if that message were to be forwarded by the communicator. The recipient may be an application running on a local host that is connected directly to the communicator or another communicator that will forward the message further. The message may also have no recipient in which case the return value of the method is undef; this possibility forces us to use the type Agent? which consists of agents and the undef value. class COMMUNICATOR Recipient(m as MESSAGE) as Agent? A generic way to encode global network topology, as far as this information is required in an abstract communication model (where the degree of detail and precision can be freely chosen depending on the given application context), is through a (possibly dynamic) mapping called routingTable. The routing table of a communicator maps addresses to neighboring agents (communicators or applications) as required for routing messages through a network. class COMMUNICATOR var routingTable as Map of ADDRESS to Agent The recipient of an outbound message is determined by looking up the destination address of the message in the routing table. If there is no entry in the routing table for a given address a then the value of routingTable(a) is undef. class COMMUNICATOR Recipient(m as MESSAGE) as Agent? return routingTable(destination(m)) Delivery Conditions In real-world distributed systems, there are complex conditions that govern when (or if) a message is forwarded by a communicator. These might include network latency, security parameters and resource limitations of the underlying physical network. Since we abstract here from lower-level network layers, the decision whether a message is ready to deliver in a given state of the network is expressed through an external predicate ReadyToDeliver. class COMMUNICATOR external ReadyToDeliver(m as MESSAGE) as Boolean Note that messages that are never ready to deliver are in effect "lost", even though they persist in the communicator's mailbox. (For example, for some UDP message m the condition ReadyToDeliver(m) might never hold.) Message Delivery We are now ready to present an algorithm for how communicators route messages to other agents. The control program of a communicator forwards messages found in its mailbox by inserting them into the mailboxes of the respective recipients of the message. The communicator program is highly nondeterministic. class COMMUNICATOR Program() = let availableMsgs = {m | m in me.mailbox where ReadyToDeliver(m)} let selectedMsgs = chooseSubset(availableMsgs) forall msg in selectedMsgs me.mailbox(msg) := false //delete the message let resolvedMsgs = ResolveMessage(msg) //resolve the message forall m in resolvedMsgs let a = Recipient(m) if a <> undef then // if recipient found InsertMessage(a,m) // forward the message else skip // else ignore message First, the communicator determines the subset of unprocessed messages that are ready to be delivered. Next, the communicator (nondeterministically) selects a subset of the available messages for processing in this step. Note that some, all or none of the available messages may be selected for processing. Next, the communicator transforms each selected message, as described above. This may result in the unfolding of a single message into many messages, each of which will be posted to a single recipient (for instance, in the case of multicasting). Note that a recipient may be another communicator. Finally, the communicator calculates the recipient of each resolved message and inserts the (transformed) message to the mailbox of the recipient. Universal Plug and Play The Universal Plug and Play Architecture (UPnP)  REF _Ref9860172 \r \h  [33] is an industrial standard for dynamic peer-to-peer networking defined by the UPnP Forum  REF _Ref9860197 \r \h  [34]. Here is how UPnP is described in  REF _Ref9860172 \r \h  [33]: Universal Plug and Play is a distributed, open networking architecture that leverages TCP/IP and the Web technologies to enable seamless proximity networking in addition to control and data transfer among networked devices in the home, office and public spaces. We have developed a high-level executable behavior model of the UPnP architecture  REF _Ref6385476 \r \h  \* MERGEFORMAT  [17] REF _Ref6383438 \r \h  \* MERGEFORMAT  [18] REF _Ref6382768 \r \h  \* MERGEFORMAT  [19] based on the informal requirements specification  REF _Ref9860172 \r \h  [33]. The construction of a DASM allows us to combine both synchronous (that is one-agent) execution models of individual devices and control points and asynchronous execution models of an ensemble of devices and control points within one uniform model of computation. Here we give an overview of our UPnP model focusing on some interoperability aspects (rather than on the internal behavior of UPnP components) related to the abstract communication model. The UPnP Protocol We briefly summarize here the basic characteristics of the UPnP protocol. Technically, it is a layered protocol built on top of TCP/IP by combining various standard protocols: DHCP, SSDP, SOAP, GENA, etc. It supports dynamic configuration of any number of devices offering various kinds of services requested by control points. To perform control tasks, a control point needs to know what devices are available (i.e. reachable over the network), what are the services advertised by devices, and when those advertisements expire. The services of a device interact with the external (physical) world through the actuators and sensors of the device. A sample UPnP device, a CD player, is shown in  REF _Ref9860694 \h Figure 3. In the full model  REF _Ref6385476 \r \h  \* MERGEFORMAT  [17], this device has two different services, called ChangeDisc, and PlayCD;  REF _Ref9860694 \h Figure 3 illustrates only the first one. The ChangeDisc service allows a control point to add or remove discs from the CD player, to choose a disc to be placed on the tray, and to toggle (open/close) the door. The figure illustrates the relevant state information associated with the service.  Protocol Phases The UPnP protocol defines 6 basic steps or phases. Initially, these steps are invoked one after the other in the order given below, but may arbitrarily overlap afterwards. (0) Addressing is needed for obtaining an IP address when a new device is added to a network. (1) Discovery informs control points about the availability of devices and their services. (2) Description allows control points to retrieve detailed information about a device and its capabilities. (3) Control provides mechanisms for control points to access and control devices through well-defined interfaces. (4) Eventing allows control points to receive information about changes in the state of a service at run time. (5) Presentation enables users to retrieve additional device vendor specific information. Restrictions Control points and devices interact through exchange of messages over a TCP/IP network where network characteristics, like bandwidth, dimension, and reliability, are left unspecified. In general, the following restrictions apply. Communication is considered to be neither predictable nor reliable, that is message transfer is subject to arbitrary and varying delays, and some messages may never arrive. Devices may appear and disappear at any time with or without prior notice. Consequently, there is no guarantee that a requested service is available in a given state or will become available in future. In particular, an available service may not remain available until a certain control task using this service has been completed. UPnP Abstract Machine The individual communication endpoints, or applications, in UPnP are devices and control points. class CONTROLPOINT extends APPLICATION class DEVICE extends APPLICATION In addition to communicators and applications, the full model  REF _Ref6385476 \r \h  [17] employs some additional agents that reflect the external world, e.g. DHCP server agents, but here we ignore them. With each agent type we associate one or more interfaces for interaction with other agents in our model or with the environment that is the external world. The environment affects the system behavior in various ways. For example, it changes the system configuration e.g. by creating and removing agents. It also affects the communication load of the network which affects message delays. Those external environmental actions and events are unpredictable. Our model is integrated with a graphical user interface (GUI) allowing for user-controlled interaction with the environment. The overall organization of the model is illustrated in  REF _Ref9675553 \h Figure 4.  SHAPE \* MERGEFORMAT  Figure  SEQ Figure \* ARABIC 4. Instance of UPnP Abstract Machine. Device model The purpose of the device model specification is to describe how a device behaves in a UPnP compliant way. In a given system state, a UPnP device may or may not be connected to a network. The network connectivity of a device is affected by actions and events in the external world and may therefore change in an unpredictable way. The device model specification is a parallel composition of a number of rules operating in parallel; different rules describe different protocol phases. external isConnected(d as DEVICE) as Boolean class DEVICE Program() if isConnected(me) then RunAddressing() RunDiscovery() RunDescription() RunControl() RunEventing() RunPresentation() Here we focus only on one of those phases, the control phase given by RunControl, that involves direct interaction with communicators. Every device offers a set of services. Each service of a device can be called by control points by means of messages. Each service call produces a response message sent back to the caller; the response message tells the caller whether the call succeded or not and may include a return value. The communication between the devices and the control points is enabled by communicators. Every device is associated with one communicator. A device sends messages by inserting them into the mailbox of that communicator. A device may receive messages from that communicator but also from other communicators. Who can deliver messages to whom depends on the actual address tables and routing tables used by communicators. type SERVICE class DEVICE services as Set of SERVICE var communicator as COMMUNICATOR Call(s as SERVICE, msg as MESSAGE) as MESSAGE The control phase of the protocol is executed only if the device has a valid address. Initially the address is undef but it is eventually updated by the addressing phase of the protocol. When active, the control phase handles service requests one at a time and runs the services. IsServiceRequest(m as MESSAGE, s as SERVICE) as Boolean class DEVICE RunServices() var address as ADDRESS? = undef RunControl() if address `" undef then RunServices() choose msg in mailbox, s in services where IsServiceRequest(msg,s) reply = Call(s,msg) mailbox(msg) := false InsertMessage(communicator, reply) After a service call to the device is taken care of, the service may continue to run. Whether only some or all of the services are allowed to run simultaneously depends on the definition of the RunServices method of the particular device. Modeling Automated Business Processes In this section we summarize a real-life application of distributed abstract state machines to model automated business processes  REF _Ref9564844 \r \h  [36]. The purpose of the summary is to illustrate the effective reuse of the abstract communication model. A business process is a protocol for commercial transactions that occur between two or more parties. Transactions are exchanges of goods, services or information. A typical example of a business process is the series of interactions required to settle a securities trade. Many business processes are designed to span organizational boundaries. For example, a process for corporate purchasing may include roles for a "buyer", a "seller" and a "shipping agent," where each of the parties is a separate enterprise. An automated business process is executed without manual steps. For example, banks in the United States use an automated clearinghouse to settle accounts for checks they honor on each other's behalf. A protocol for an automated business process specifies data formats for messages, some constraints on the behavior of the electronic communications network itself, and a description of the possible patterns of messages that constitute a transaction. XLANG XLANG is an XML based formal language that can be used to define the data and networking protocols of automated business processes  REF _Ref9565950 \r \h  [32]. XLANG builds on the existing standards for the Internet and World Wide Web. The building block standard that XLANG is most dependent on is WSDL, the Web Service Description Language  REF _Ref9690428 \r \h  [35]. XLANG has a two-fold relationship with WSDL. Syntactically, an XLANG service description is a WSDL service description with an extension that describes the behavior of the service as a part of a business process. Operationally, an XLANG service behavior may rely on simple WSDL services to provide basic functionality for the implementation of the business process. The goal of XLANG is to make it possible to formally specify business processes as stateful long-running interactions. As a rule, business processes involve more than one participant. The full description of a process, called a contract, must constraint not only the behavior of each participant, but also the way these behaviors match to comply with the overall process. XLANG Abstract Machine The definition of an abstract operational semantics for XLANG comes in the form of an abstract machine model in combination with an XLANG-to-AsmL compiler. The behavior is formalized by mapping a given XLANG contract to AsmL code effectively explaining this behavior in terms of machine runs. An XLANG contract contains two parts: a collection of individual so-called XLANG service behaviors (that is service behavior specifications), and a port map defining the interconnection topology of those services. Each of the service behaviors is compiled into a sequence of XLANG Abstract Machine (XAM) instructions. The port map determines the routing information that is used by the network abstract machine to interconnect the services. The approach taken here is similar to the concept of "phases of compilation" in compiler construction.  SHAPE \* MERGEFORMAT  Figure  SEQ Figure \* ARABIC 5. Generation of XAM instructions Note that our approach is abstract: the structure we describe does reflect a real-world implementation but omits implementation-specific detail. The full XLANG abstract machine is a DASM that has two main components, each of which is again a DASM: Service Abstract Machine: a service abstract machine is parameterized with a sequence of XAM instructions. Network Abstract Machine: here the port map of the contract determines the necessary interconnection topology of the services. In the remainder of this section, we first outline the overall structure of the service abstract machine. We omit the details regarding the behaviors of the individual XAM instructions. We then describe the interaction of the service abstract machine with the network abstract machine. Service Abstract Machine The Service Abstract Machine models an individual service. It consists of two different types of ASM agents: 1) a uniquely identified service manager that represents the behavior of the infrastructure on top of which the service runs; 2) some, possibly empty, collection of concurrently operating processes (or process agents) that represent the XLANG processes associated with that service. Each process represents either a service instance created directly by the manager or a sub-process spawned by a previously created process. During its lifetime, a service instance may spawn several sub-processes. The behavior of that agent group consisting of the service instance and all its descendants plays an important role. Each process belongs to some manager. There are four modes that indicate whether (a) a process has exited by having run all of the XAM instructions, (b) a process has been interrupted by an exception, (c) a process has been halted by external intervention, or (d) a process is currently executing instructions. type Service type Label type ServiceProgram class Manager extends Agent service as Service pgm as ServiceProgram enum ProcessMode exited raised halted running class Process extends Agent manager as Manager var pc as Label var mode as ProcessMode var subProcesses as Set of Process class ServiceInstance extends Process The program of a process is to execute the next XAM instruction in the running mode, and to do nothing (skip) in any other mode. Some instructions may be executed without incrementing the program counter; others cause the program counter to jump to a new position in the program. type Instruction Execute(intr as Instruction, p as Process) instr(pgm as ServiceProgram, lbl as Label) as Instruction class Process Program() if mode = running then let instr = instr(manager.pgm, pc) Execute(instr, me) else skip A manager has two independent jobs. One is to activate new service instances when activating messages are received. For example a buyer may send a purchase request to a seller that will trigger the creation of a new instance of the seller service to handle that request. The seller may of course receive several requests from different buyers and create several independent service instances to handle those requests. The other job is to handle message traffic class Manager Program() ActivateServiceInstance() HandleMessageTraffic() HandleMessageTraffic() ReceiveIncomingMessages() ForwardOutgoingMessages() Interaction with the Network Abstract Machine The Network Abstract Machine part of the XLANG model is a specialization of the abstract communication model with appropriate routing tables and address tables that enable communication between services whose ports are interconnected according to the port map of the contract. A service manager has a set of communication ports. Each port is associated with an inbox and outbox of message instances. The inbox of a port contains all the message instances that have been sent to that port and the outbox contains all the outbound message instances from that port. (The message instance terminology is due to WSDL.) type MessageInst class Port var inbox as Set of MessageInst var outbox as Set of MessageInst class Manager ports as Set of Port A message instance is transformed into some concrete network message format when it is transmitted over the net. The network message contains the original message instance and a destination port. class NetworkMessage port as PortName msg as MessageInst Each port is associated with a communicator and may be owned by a manager (the manager, if any, who has the port among its ports). No port can be owned by more than one manager. class Communicator class Port communicator as Communicator A manager uses the port map of the contract to create network messages from outbound message instances and forwards them to the communicators of the corresponding ports. class Manager portMap as Map of Port to Port class Manager ForwardOutgoingMessages() forall p in ports where p.outbox ne {} choose m in p.outbox p.outbox := p.outbox - {m} let msg = new NetworkMessage(portMap(p),m) InsertMessage(p.communicator,msg) When a network message has arrived, the original message instance is extracted from it and inserted into the inbox of the destination port. class Manager ReceiveIncomingMessages() if mailbox ne {} then choose m in mailbox mailbox := mailbox - {m} let p = m.port p.inbox := p.inbox union {m.msg}  REF _Ref9862006 \h Figure 6 shows an instance of the XLANG abstract machine.  SHAPE \* MERGEFORMAT  Figure  SEQ Figure \* ARABIC 6. Instance of XLANG Abstract Machine The XLANG model instance in  REF _Ref9862006 \h Figure 6 contains several service abstract machines (SAMs) and a network abstract machine (NAM). Each SAM contains a manager, some service instances and other processes. The NAM contains several communicators. The XLANG abstract machine has been implemented in AsmL  REF _Ref9564844 \r \h  [36]; a GUI is used to interact with the model and visualize the state during simulation runs. Related Work We start with domain-specific languages; the connection to AsmL will soon become apparent. General introductions to domain-specific languages are  !,-/<ANOPTXYǺ|reXNJ=h5h8aJmH sH h8haJmH sH h5h-aJmH sH h5h,:aJmH sH h8aJmH sH h aJmH sH h5h aJmH sH h5hmaJmH sH hntaJmH sH jh0JUaJmH sH h th FQaJmH sH h th]faJmH sH h th FQCJ aJ h th-CJ aJ h thCJ aJ h thu!CJ aJ  !OPYZl{|}~}   gd7gdpXgd]f $ & Fa$gd8 $@&a$gd8 V$@&a$gd8$a$gd8$a$gdnt$a$gdm@gd-...0- 0 M W { | }    [ \ ʼ{naTJh_H mH sH h5h7_H mH sH h5h FQaJmH sH h5hS-aJmH sH h5h_aJmH sH h5hpXaJmH sH h5haJmH sH h5h}aJmH sH h5hURaJmH sH h5h FQ5aJmH sH h7h7mH sH h!CmH sH h]fmH sH h}mH sH h7mH sH h5h FQmH sH \ ] t u    . 0 4 Ⱦ񴧝{gȾ{WJ=h7h7_H mH sH h76]_H mH sH h5h76]_H mH sH 'jyh-pBhpU_H mH sH h-pB_H mH sH jh-pBU_H mH sH h [_H mH sH h7_H mH sH h5h7_H mH sH h+_H mH sH h8_H mH sH h8_H mH sH 'jhShpU_H mH sH hS_H mH sH jhSU_H mH sH 4 6 < > @ r t v x "#,-_`wܺί܇zzzpffXpjh'@U_H mH sH h(I_H mH sH h'@_H mH sH h5hVH_H mH sH hVH_H mH sH h7_H mH sH hP _H mH sH h8_H mH sH h8_H mH sH 'jh+hpU_H mH sH jh+U_H mH sH h+_H mH sH h5h7_H mH sH h76]_H mH sH " %4'-F-N/d/033305689n;N= ?gdWgd(gdM1gd0gd0Lgd?gd;:gdm gd.gdm gd|gdQgdU*gdVHwx :<>@HJ  ݾݾtȒfRff'jh(IhpU_H mH sH jh(IU_H mH sH 'jah(Ih3=U_H mH sH h3=_H mH sH jh3=U_H mH sH h(I_H mH sH 'jh'@hpU_H mH sH h'@_H mH sH h8_H mH sH h8_H mH sH jh'@U_H mH sH 'joh'@hpU_H mH sH <@~@BDFNPR^`ȺȦҀlbҀN'jMh5h+U_H mH sH h+_H mH sH 'jh5h+U_H mH sH !jh5h+U_H mH sH h8_H mH sH h8_H mH sH 'jWhhpU_H mH sH jhU_H mH sH h_H mH sH h5h+_H mH sH h(I_H mH sH h'@_H mH sH h'@h'@_H mH sH :<>@FHLN2BJvxtvx̸̮̮̮̮̐̚ykyjhn.U_H mH sH hn._H mH sH h5hVH_H mH sH hVH_H mH sH 'jGh5h+U_H mH sH h+_H mH sH 'jh5h+U_H mH sH h5h+_H mH sH h8_H mH sH h8_H mH sH !jh5h+U_H mH sH ' ";E_oqvwݾݝuuuuhuh^hU*_H mH sH h5h 0_H mH sH h(_H mH sH h 0_H mH sH h(_H mH sH hVH_H mH sH h5h+_H mH sH 'jAhn.hpU_H mH sH hn._H mH sH h8_H mH sH h8_H mH sH jhn.U_H mH sH 'jhn.hpU_H mH sH "Cfwxy (HdȾҾuuukh3! _H mH sH h_H mH sH h69_H mH sH hM _H mH sH he@_H mH sH h3=_H mH sH h(_H mH sH h5h!_H mH sH h!_H mH sH h 0_H mH sH h5h 0_H mH sH h(_H mH sH hU*_H mH sH h5hU*_H mH sH &  &dfl$D Ⱦ砖uukukk]Sh3=_H mH sH jh3=U_H mH sH hgq_H mH sH hik_H mH sH hh?_H mH sH h5h 0_H mH sH h69_H mH sH hQ_H mH sH h 0_H mH sH h!_H mH sH h8_H mH sH h8_H mH sH 'jhM hpU_H mH sH hM _H mH sH jhM U_H mH sH   "LNP~$.LVX`& ݾ~Ȓqgg]g]gg]]]hgq_H mH sH h 0_H mH sH h5h 0_H mH sH 'jhM hpU_H mH sH jhM U_H mH sH hM _H mH sH hh?_H mH sH hik_H mH sH h!_H mH sH h8_H mH sH h8_H mH sH jh3=U_H mH sH 'j3h3=h5U_H mH sH "& ( ^ d!!!!!!!!!"" "Q"U"^"g""""""""""""""#######̭♏|t||jh}_H mH sH h}mH sH h5h@mH sH h@mH sH h@_H mH sH hO5_H mH sH h8_H mH sH h8_H mH sH 'j%h`hpU_H mH sH jh`U_H mH sH hmH sH h`_H mH sH hh?_H mH sH hQ_H mH sH )###$$0$2$4$6$>$@$N$p$$$$$$%L%f%%%%%%$&&&(&ʶԫʗyoaVJjh.UmH sH h.h.mH sH h5h*6]mH sH hQ_H mH sH h _H mH sH h._H mH sH h}_H mH sH hO!_H mH sH h8_H mH sH h8_H mH sH 'jh`hpU_H mH sH h`_H mH sH jh`U_H mH sH h|_H mH sH hO5_H mH sH h@_H mH sH (&Z&\&^&`&h&j&l&&&&&&2'4'''''''''(((&)()*),).)uɇmamOa#j h.h5UmH sH jh.UmH sH h.mH sH #j hphpUmH sH jhpUmH sH h*mH sH h5h\cmH sH h5h*mH sH h@mH sH hpmH sH h mH sH h8mH sH h8mH sH jh.UmH sH #j h.hpUmH sH h.mH sH .)0))8*:*h*j*l*n*p*r*t*v*~****++ +"+$+&+*+:+^+|++++++++++ ,,&,(,V,뚬tjhl|MUmH sH hl|MmH sH #jx h.h5UmH sH #j hphpUmH sH jhpUmH sH hU:rmH sH h8mH sH h8mH sH #j h.h5UmH sH h.mH sH hpmH sH jh.UmH sH (V,X,Z,\,^,`,,,----D-F-n-v--2.j.z..............ȶ}rmia]Ramj hhUh;:jh;:Uh8 h8jj h{Uh{jh{Uh.h V h)@h-h-h5h2_H mH sH h5h.i_H mH sH h_H mH sH h%mH sH hl|MmH sH h8mH sH h8mH sH jhl|MUmH sH #j hl|MhUmH sH  .// /8/://F/H/L/N/X/b/h/r/|////0 0F000d11111122 2 2B2223333~3333333ɳɯŎ|hv}h-6]hCh0 h0Lh0L hm hm j h?Ujh?Uh?hA)h;:h;:6]hm h0Lh;: h)@h-h- h8j\ hhUh.jh.Ujh;:Uh80344!4$4-45464:4D4E4R4S4d4~4444444444444444444444555.5/525758595<5C5D5O5b5c5e5i5m5r5u5v5w5־ȴȪȘ h&6]h!6h&h-6]h&h'h-6]hv}h-6]hF{hF{6]h-hM1hM16]hM1 hM16] h@Rh@R h@R6]hDh-6] h)@h-9w55555555555555555555556666#6,6-6A6B6C6G6Q6i6o6p6666666666:7;7<7?7{7}777777778ʶʲʶʥʶh!6h=W]h=Wh=W56\]h!6h=Wh=W6]h!h=W6]h=Wh@Rh@R6]hM1hDh-6] h@R6]h@Rh&h- h)@h-;88 8888888:9D9F9d9f99999999: :::;::::::;*;.;3;8;T;Y;f;k;l;m;n;k<<<= ="=$=N=U=༮ҪhijhM15h'?h`lh`l6]h`lh=~h-h(h!6h=Wh@R6]h@Rh!6h@R5hM1hM16]hM1h!h=W6]h=Wh=Wh=W6]"h!6h=WOJPJQJ]^Jo(3U=W=Y=w=~=========> >5>E>u>v>>>>? ? ??????@@S@U@]@i@j@t@u@y@z@{@|@}@~@@뾺xhHh-6] hH]hHh-]h4h-6]hHh-6h1th-6]h(h~ h)@h-h-hM1 hijhM1hHhM16CJaJh=~hM16CJ]aJhM1CJaJh=~hM1CJaJhij hc5- ?6???DACCCEEF#F6FGCGYGGH1HH $^a$gd-`gdgd`gd-gd-gd`gd-$a$gd-gdl^gd\3Dgd0LgdM1@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@AAAAAAAAA A!A"A#A*Aɿɻɯɻɻ~лhjh-6H*]hHh-6]hjh-6]h~h~6]h\3Dh(h~hHh-6h-h~h-6] h)@h- hHh-h4h-6H*] h-6] hH]hHh-]hHh-H*]1*A1A2A4A9AGAWAXAbAcAdAeAfAgAhAjAkArAsAwAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAѻٴªѴŸh(hjh-6]hHh-6H*]hHh-H*] hH6] hHh- h-6]hHhH]hHh-]h4h-6]hHh-6 h)@h-h-h(h-6]9AAAABB BBBBBBB B#B$B%B&B'B(B4B5B;BIBJBKBTBUBVBWBXB[B\B]B^B_B`BbBcBdBuBwBvo h4h-h4hH6H*]hHhHH*]hHhH6]h4h-6H*] h-6] hH]hHh-H*]hHh-6]hHh-]h4h-6]hjh-6] h)@h-h- hH6]hHhH]h4hH6])wBBBBBC"C5C6CJCKCLCSCTCUCfCgChCuCCCCCCC۵˨ːېrdYO>!jh5h-UaJmH sH hah-6]hl^6aJmH sH hl^hl^]aJmH sH hnIh-6aJmH sH h5h-6]aJmH sH h-]aJmH sH h8aJmHnHsH uh^fh8aJmH sH *jNh~h5U]aJmH sH jh~U]aJmH sH h~]aJmH sH hl^]aJmH sH h5h-]aJmH sH CCCCCCCCCCCCCCCCCCCCCCCCCѳ~vohaoYOEY@O h]hh-H*]hh-6]hh-] hh h:h- hh-hh-6 h)@h-hl^h~h-mH sH h~h-CJ\aJmH sH h~h-CJaJmH sH h~h~CJaJmH sH h8CJaJmHnHsH u%jh^fh-CJUaJmH sH h^fh-CJaJmH sH h5h-aJmH sH CCCCCCCCCCCCCCCCCCDD DDDD>D?DCDOD]D^D_D`DaDlDmDnDrDsDxDyDzD{DDDDDDDE EEEŷųšššӊųņhh0L h>]hYWh-6H*] h6]hYWh-6]hh-6h-hl]h-6]hl^ h)@h- hh-hh-6H*]hh-6] h]hh-H*]hh-]3E#E@EAEGEHEaEbEcEhEiEjEkElEEEEEEEEEEEEEEEEEEFFFFFFFFF#F$Fʾ䯨ʟ򐉅{{mh:h-6]mH sH hC~th-6]h- h)@h- hhh:h]h:]mH sH  h:hh:h6H*]mH sH h:h:]mH sH h:h]mH sH h:hH*]mH sH h:h6]mH sH hhh6])$F%F&F'F,F-F.F0F3F4F6FM@MfMhMMMMMMMMMMM NN%N)N*N+N0N1N2N3NDNպհ՟՟՟}ujh1h-6H*]h1h-]h1h-H*]h1h-6]h:hHh 6]h- h1]h1h1]hqh16]h h 6] h)@h-h1h 6]h hqhBJ6]h1hBJ]h1hBJ6]hBJ h h )DNENJNVNWNXN]N^N_N`NaNbNeNoNpNqNvNwNxNyN{N~NNNNNNNNNNNNNNNNNNNOOOOv̀vh1h?FTH*]h1h?FT6]h1h?FT]h(hHh 6]h~h?FTh)h/h h;h; h;6]h1h16H*] h1]h1h1]h1h1H*]h1h16]h1h-hHh-6]+OOOO OOOOOOOOOPPP P PPP^PbP~PPPPPPPPPPPPPPPPẞ|rh`rhrh-]hrhrH*]hrh-6] hr6]hrOJPJQJ^Jo(hqhr6]hrhrh-5h/h-6]hqh-6] h)@h-hh8 h8jh-Ujh-Uh-h.hrh 5h h) h1h?FT%PPPPPPPPPPQQTQVQ\QpQrQQQQQQQQQQQRRRRRRRRRRSSTJTbTT콵윱yukuhh6]h hm h.h8 h8jh.Ujh.Uh. h.6]h.h/6]hrhrh/6h/h/h-6] hr]hrhr]hrhrH*]hrhr6]h- hrh-hrh-]*TT UUU(U)U*U8U>U?U@UAUBUCUDUJUKULUMUNUOUPUVUWUXUYUZU[U\UjUkUUUUUUUUUUUUUʼʲxnxh8h6]hh6] h k]h kh k]h kh k6] h kh/h kh/]h kh kH*]h kh/6] h6] jh kh kh kh/5hh/6]hh/6]h/hhhh6]+TU8UPUUVVVXZ[a[[m\(]8^?aia`gdcgdV]Vgd & F9V]Vgdh & F9gdhgd-gdhgdkcgds[ $^a$gdWgd~gd $^a$gd kgd/gdUUUUUUUUUUUUUUUVVVVVVVVVVVVVVVVVVVVVVVVVVø||n|n|n|nhIh~6CJ]aJhIhWCJaJ jhIhWCJaJhIh~6CJaJhIh~5CJaJhIh~CJaJhIh?FTCJaJhW hc5hWh;5hRngh kh k]h kh kH*]h kh k6]h khh(VVVVV#W%W4W5W;Wmnmompmqmrmtm}mmvnwnnnnnnn޺޺޺޺ʣh5hDH*mH sH h~5 h~5hDh~5hD6h5hD5h5hD6mH sH hDmH sH h5hDmH sH  hO_hD h5hDhO_hD5gd46gdk gd3gdk NgdO_gdDSrUrXr[r]rfrqrrrsrtr~rrrrrrrrrrsss s s s ssssssss1s2sXssseh5hk 6H*mH sH  jh5hk mH sH h3H*mH sH h5hk H*mH sH h5hk 6mH sH h5hk mH sH h3h3]mH sH h3mH sH hmH sH hfAhfA6mH sH h^hfA6mH sH hfAmH sH h^mH sH h.Bhk 5 h.Bhk $Xs_sasdsgsisnspsssts|s}sssssssssssssstt3t?tNtOttttttttuuvvꚩyph8mH sH #jh5hk UmH sH jh5hk UmH sH  h.Bhk h46mH sH h.Bhk 6h5hk 56mH sH h5hk 6mH sH hmH sH h5hk H* h5hk h5hk 5h5hk mH sH h5h3mH sH )v v vv&v(v:vlv|v~vvvvvvw^w`wrwtwwwwwwwwwwxxxx xxKxLxPxQxVxWxhxixjxkx}xxxxxxxxxNy޺ޤޔh>mH sH hi;mH sH h5hk 5 hQ(2hk h5hk hQ(2hk 5h5hk 6mH sH h7RmH sH h0qmH sH h5hk mH sH jh5hk UmH sH h8mH sH 7Nyyyyyyyyyyyyyyyyzzzz0z1z3zEzMzgzjznzpzuzwzzzzzz{j{v{{{{{{{{ɽɽɑɂɽɽzszszs hBhk hBhk 5hUHmH sH  h5hk h5hk 5hi;mH sH hUbmH sH h0qmH sH hUbhUb]mH sH h5hk 6mH sH h5hk mH sH hqh^hq5h^hq6mH sH hQ(2hq6mH sH hqmH sH -{{{{{{||!|-|0|1|2|3|4|5|L|N|Y|Z|[|\|b|c|q|||||||||||||||}},}<}b}d}p}Ľ颚Ꮗ|t|t|t|t|hhG_mH sH h5hk mH sH h7RmH sH  h5hqhh5hq5 hNhi;hNh5hUH6h5hN6 hNhN h5hN h5hqh5hq6 h5hmhqhUHhm hBhk hBhk B*ph-{{||||}~~~ 7߀!DSpJkgd|5!gd=gdgdT(gdhG_gdk Ngd5gdUHNgdO_p}r}}}}}~~ ~"~#~[~a~c~j~k~v~~~~~~~~~~~~~~~478?@KLMT[_güüüü⬤␂vvh5hk 6mH sH hT(hT(6]mH sH hT(mH sH hUhU6mH sH hUmH sH hAmH sH h@mH sH  h5hk h5hk 5hUhU6hUhk 6 hUhk h5hk mH sH h5hhG_mH sH hhG_mH sH *ghlu2678JX}~ǀɀYeṱyoyh7U0JOmH sH h7Uhk 6hUmH sH hh6]mH sH hmH sH hA h5hA hUhk hUhk 5h5hk mH sH hT(hT(6mH sH hT]mH sH hUhT(6hT(]mH sH hT(hT(]mH sH hT(6mH sH +eɁ!#),.DHORS\ikpjwHIJO]dk~t~jfjh|5!hgh|5!5\h\#h\#6]h\# hcVh|5!hcVh|5!5h5h|5!aJmH sH hmh|5!6]aJmH sH h|5!aJmH sH hxh=h>3 hk hk hAh7Uhk 5 h7Uhk h5hk hy0mH sH hmH sH h5hk mH sH (k !"/FdO\ogd>Jgdi7gdhgd O,gds$a$gd|gd|gd_NgdO_gd\#JLNPXZ^Z\ ǹ||rrrhZhjh=\UaJmH sH h=\aJmH sH h|aJmH sH hdTaJmH sH h8aJmH sH h8aJmH sH 'jhQAxhUaJmH sH hQAxaJmH sH jhQAxUaJmH sH h5h|aJmH sH h|5!aJmH sH h?aJmH sH h}aJmH sH h9 aJmH sH h|5! '()*8KUbchjv !"ùåïÛybPCh|h|aJmH sH #h5h|5OJQJaJmH sH ,jh5h|UaJmHnHsH tH ujhkUmHnHuhdTaJmH sH h9 aJmH sH h_aJmH sH h}aJmH sH h|aJmH sH hQAxaJmH sH h5h|aJmH sH h8mHnHuh8jh=\UaJmH sH 'jr h=\h?JUaJmH sH "ʼnډ5KQTcqŋƋʋҋ ./0Jvw/7EFcdhovǿǿh^hi76 h16h^ hi7h1 hi7hi7h=Whi7h1h-hshdThZ<hxhZ<mH sH hdTmH sH h?mH sH h\#mH sH h] aJmH sH h5h\#aJmH sH h\#aJmH sH 2vR\`'3NOST[\aoyؐĽĶuh5h$,6]aJmH sH h5h>J6]aJmH sH h5h>JaJmH sH h$,aJmH sH h *aJmH sH  hFh t hFh1 hFh^hFh^5 hFhEhFhE\hFhE5\h thx8h^h|vhi7(%9:;RS (,0Dd֒*,V´ ցtjtjttjc\c\Uc\ hFhr hFh|v hFh.&h.&aJmH sH h5h.&aJmH sH hzyaJmH sH h8aJmH sH h8aJmH sH 'j hh>JUaJmH sH jh>JUaJmH sH h>JaJmH sH haJmH sH h5h>JaJmH sH h5h>J6]aJmH sH h5h$,aJmH sH $(;C_ijknsՔ֔ܔ34xy߽쭟xpi hqvh>Jhqvh>J5 hqvhqv hqv5hVNhWIaJmH sH hZ*h>J6aJmH sH hFh>J]aJmH sH hVNh>J6]aJmH sH h}aJmH sH h~h>J6]aJmH sH hZ*h>J6h5h>JaJmH sH h>JaJmH sH h|vaJmH sH &ڕPu0@.R&T>Qupgdi7NgdH[Ngdygd_gd}gd O,gd<>NgdFNgdO_ǕȕʕϕѕٕڕەP^`jluzіӖݖߖ/08?@MƿhPw"h;lhi7 hFhWI hFh/hFh 75 hFh 7hFh *5 hFh *hFh,1v5 hFh,1vh,1vhZWhqvh}mH sH  h,1vhqvhqvh>J5 hqvh>J hqvhWIhqvhWI52Mڗ&(13?fpȘ !(6\!-<?FHKQRiƚ9<FPWXghpļ h t6hyh th} h5hyh_hi7 hi75hyh}]h}h}6]h#Q h#Q 6hKK h Ch Ch Ch C6h Ch#Q hPw"h} hi7hi7:ptvΛЛߛ(+9;@BKMSTUfpxyќ$01237<=>C_akmŽ󧟛}v}v} hRh_hRh_5 h6chI= h6ch&+h&+h&+6h&+hhi)hZWhi] hyh_ h_hh_h5hyh_aJmH sH h5h_aJmH sH h taJmH sH h_aJmH sH hyhyhy6.mstuy2<Ylq7MUV_`nopuvݟ +68Eûַ֦֭ބބhwhfbhfb5 hfbhyD hfbhi7hfbhi75 hfbhfbh0h/6PJh2uhfbhfb6hfbh9hyD hi7hi7h/h;lhi7 hH[h_hRh_5h_hT[ hRh_4֡=pqҢ5Sۣ-7ʪIgdtgdtgdtgdgd O,gdi7NgdO_EFZ[jxyz{|Ԡ(R[acġԡա֡ۡܡ $)ADTUpqu{»٬ heKnh~ heKnhuhu heKnh1 heKnhi7heKnhi75 hi7h~hVlh~h1 hi7hi7h[Thi7hfbhwhfbPJh0hfb6PJ hfbPJ h9PJ:ŢѢҢآۢ!$&'4=@S[]bchimtģϣӣڣhurB*phhVlheKnhi7B*phhxhzqheKnheKn5heKn heKnh~heKnhi75 h[h~heKnh[B*phhVlB*phheKnh~B*phh[h~heKnh~5hi7 heKnhi74,-Diui٦7;RS_ghnah8_H aJmH sH +jd!hnh?JU_H aJmH sH hn_H aJmH sH jhnU_H aJmH sH "h5ht6]_H aJmH sH h5ht_H aJmH sH h5htmH sH h?Jh*+.hh6OheKnhi7B*phhVlB*phhVlhi7heKnhi75" DFtvxzʪ˪سؐɇ|oeoR$jh5htU]aJmH sH htaJmH sH h5htaJmH sH ht]aJmH sH h5htCJ+jV"hnh?JU_H aJmH sH h8_H aJmH sH +j!hnh?JU_H aJmH sH h5ht_H aJmH sH hn_H aJmH sH jhnU_H aJmH sH h8_H aJmH sH 45E <>^`bjn¬ʬ̬.0Ȼȟ~siUsiKhpaJmH sH 'j#h5htUaJmH sH h8aJmH sH h8aJmH sH 'jH#h5htUaJmH sH h5htaJmH sH !jh5htUaJmH sH h8]aJmH sH h8]aJmH sH $jh5htU]aJmH sH *j"h5htU]aJmH sH h5ht]aJmH sH 02`bdfnptޭ LMYȾ񱥖uiu]]]SIShaJmH sH htaJmH sH ht_H aJmH sH h_H aJmH sH h8ht_H aJmH sH "h5ht6]_H aJmH sH h5ht_H aJmH sH hp_H aJmH sH h5htaJmH sH h8aJmH sH h8aJmH sH 'j:$hph?JUaJmH sH hpaJmH sH jhpUaJmH sH NPZhu{|}گ>?]Ȱְذ,M2btv~崤崖~th5aJmH sH htaJmH sH h5ht]aJmH sH h5ht6aJmH sH h5ht6]aJmH sH h5htaJmH sH h}_H aJmH sH h_H aJmH sH ht_H aJmH sH h5ht_H aJmH sH hp__H aJmH sH (ʪ~ٰ246FR_=SۻtgdB & Fgd3gdRLgdRL$gdTNgdO_gdtgd"gdtgdtgdp_̲βв(*JLNVXγڳ 񹨹wwnd^Nddj%h5h?JUaJ h50JTjh5UaJh|ht0JTh5ht6h8aJmH sH h8aJmH sH 'j,%h5htUaJmH sH !jh5htUaJmH sH h5htaJmH sH h8mHnHuh8'j$h5h?JUaJmH sH h5aJmH sH jh5UaJmH sH 5:DE]3456T]"m Syz˽颕˅˅˅˅˅˅{q{q{h3aJmH sH hHPYaJmH sH h5ht6]aJmH sH h5h%aJmH sH 4jh5h5OJQJUaJmHnHsH tH ujh%UmHnHuh5htaJmH sH h|ht0JTh5ht6htaJmH sH  h ~@ht h5aJ&ǻλϻڻۻ<^dhƽ¾º¾°јфyoѰbbh5htaJmH sH h8aJmH sH h8aJmH sH 'j&hQWhtUaJmH sH jhtUaJmH sH hG^aJmH sH hHPYaJmH sH hHPYht hcVhthcVht5htaJmH sH hHPY]aJmH sH hHPY6aJmH sH hFrht6aJmH sH $ npsȾݾ:PVYhvۿCNRSghipqrstu¸ ¸k&jhZ}UaJmHnHsH tH ujhZ}UaJmH sH hZ}aJmH sH h8mHnHuh8'j&h ;hUaJmH sH h ;aJmH sH jh ;UaJmH sH hG^aJmH sH h5htaJmH sH htaJmH sH hFrht]aJmH sH $"&P145BOTyܿhzh 1PJhzh 15PJ hBPJ h?PJ h[$PJ h 1PJ h PJ h\JPJh,MhRLhth8[h ;h8mHnHujhTUhTjhZ}UaJmH sH !j'hZ}hZ}UaJmH sH 1-CXoZ 6Y)DNgdudNgdOgdHgdBNgdz$&(,-%0345B\ſŭ{wswowh#h|Lhh>hLSMhKhWAh,M hEPJh>h>6PJ]hBhB6PJ] h>PJ hBPJ hS PJ h~bPJ h PJ h 1h 1hzh 15\h_SQh 1PJh 1 h_SQh 1 hzh 1hzh 15*(,8=HXYZ~ "()35@CDTopu| #$&+-68ž h3cXh^i h3cXhS, h3cXh,Mh3cXh,M5 h3cXh>h3cXh>5 hKhKhHhUhqh3cXh&Uhf!oh^ih th|LhhB>8;<IKXY[`bdnrt~2BR]bkzẔ̵̵̌~~~hudhS,5 hudhS,h|h}hS,hS,6hS,h\xhohwhBh,Mh3cXho5h3cXh5 h3cXh h3cXho h3cXh> h3cXhP(h3cXhP(5 h3cXh^i h3cXh&Uh3cXh&U50)-/27BDP\fj&*ZdhŽ۶ꞚꚏhEh|LhKhBB*phhth,M hluhluhudh,MOJQJ^J hCh,MhudhS,5 hudhS, hudh#hudho5 hudhoh&Uhlu hudh,Mhudh,M5 hudhlu4D*hm17O&"?gd7U$gd_>Vgd_ & F<gd_gd+ZNgdzgdo.gdk@ggdo.gdj8gdo.gdNgdud3=Buvw pɹɂznbhk@gho.6mH sH h5ho.6mH sH h}mH sH he"mH sH h8mH sH h8mH sH #j'hj8hAUmH sH jhj8UmH sH hj8mH sH hImH sH h5ho.mH sH  hRLh8[h|L h|6hluhlu6hb1hluh|hEh$67cl7<@LMT "d.z|~ ()ѳŪ햎|nhzho.6]mH sH #j(hhUmH sH hmH sH jhUmH sH h8mH sH h8mH sH #j(hzhAUmH sH jhzUmH sH hzmH sH ho.mH sH h5ho.6mH sH h5ho.mH sH hk@gmH sH ))*3;<BL{xy%&@JKYck*+,/01=t~Ը԰ԤԤԤzn԰hcho.]mH sH h_ho.]mH sH h_]mH sH h_h_]mH sH h_6mH sH h5ho.6mH sH h_mH sH h+ZNho.]mH sH h+ZNmH sH ho.mH sH h5ho.mH sH hB hz6]mH sH hzmH sH hzhzmH sH + !"#:;<=>FG]^_`b",39=uy{Ӿӫ}uumm_hdho.6]mH sH ho.mH sH hBndmH sH h5ho.6]mH sH h7UmH sH  hO7h_>Vh8mHnHujh_>VUh_>Vj )h5ho.UmH sH (jh5ho.UmHnHsH tH ujh5ho.UmH sH h5h7UmH sH h5ho.mH sH h_mH sH  {e0:CLVrNgdO_gdgd:&5gdo.gdo. & F&gdo.gdBndgd_*10;EUѾѰѨѨќ~~rfѨќh5ho.5mH sH h5ho.]mH sH h:&56mH sH h:&5h:&5]mH sH h}6mH sH h5ho.6mH sH h}mH sH h5ho.6]mH sH hCq ho.mH sH ho.mH sH h5ho.mH sH h/ho.mH sH hdho.6]mH sH ho.6]mH sH 'p #V[dk|~46FH\^qrsu} hAh h5ho.h5ho.5h5ho.B*mH phsH h5ho.mH sH hmH sH N'R 8Qo!2=gd(gdo.gdo.gd0fgdNgdO_Bis!$).4 !%27?BIKPRadlnsulq[`nsChdmH sH h}mH sH ho.mH sH hA h5ho.h5ho.5h5h0fmH sH h5ho.6mH sH h5ho.mH sH h0fmH sH C=_l[nzCQr8c4Nogddgdo.NgdO_CH[]bdjlrw 8^`cd )+/3:@CEwz·𫣑#j)hrvIh?JUmH sH hrvImH sH jhrvIUmH sH h5ho.mH sH hmH sH hd hTrhdhTrho.5 hTrho.hTrhTrhTr5 h5ho.h5ho.58o fg*ILb & FgdgdAgdpfgdtgdo gd+Jx]^`gdgd;ngdgd&gd@$gd@gd@NgdO_'(>?@ACefgûzzzsog[gI[#j*hx>Mh?JUmH sH jhx>MUmH sH hx>MmH sH ho. hvh@jh@Uh@j*h@h@UmH sH "jh@UmHnHsH tH uh@mH sH jh@UmH sH h&mH sH h@56mH sH h5ho.56mH sH h5ho.mH sH jhrvIUmH sH h8mHnHuh8&':;EI^_ ԮܒtrUh5hEmH sH humH sH h5hmH sH h&h@mH sH h8mH sH h8mH sH #j+hh&UmH sH jh&UmH sH hx>MmH sH h&mH sH h5h&mH sH jhx>MUmH sH h8mHnHuh8, given in  REF _Ref525673966 \r \h  [14] REF _Ref9862233 \r \h  [27]. The annotated bibliography  REF _Ref525673966 \r \h  [14] categorizes the domains of various domain-specific languages into five different groups. The group on software engineering is further subdivided into several subgroups including one for software architectures. The main focus of a software architecture description language (ADL) is to specify system's conceptual architecture rather than its actual implementation. Recent surveys of ADLs are given in  REF _Ref525985481 \r \h  [11] and  REF _Ref9862309 \r \h  [30]. This is a quote from  REF _Ref9862309 \r \h  [30] regarding the prevailing argument for using ADLs: They are necessary to bridge the gap between informal, "boxes and lines" diagrams and programming languages which are deemed too low-level for application design activities. According to  REF _Ref525981826 \r \h  [29], an ADL must provide means for explicit specification of the following building blocks of an architectural description: components, connectors, and configurations. Let's see what these building blocks are in AsmL. Components are agents or groups of agents together with a collection of interfaces defining the interaction points of the component with the environment. The interfaces may be declared as native COM  REF _Ref515906955 \r \h  [10] interfaces, automation interfaces or abstract model interfaces, depending on their usage. For example, in the UPnP model, devices are components that interact with communicators via abstract model interfaces and with the GUI via automation interfaces. Connectors are special components that enable the interaction of other components. Their behavior is clearly separated from the core behavior of the model. For example, in the UPnP model the communicators are the connectors; indeed they do not reflect any UPnP specific behavior. Configurations describe the topology of the system. In AsmL, configurations are normally described explicitly in the state. For example, the address table and the routing table in the abstract communication model encode configurations. However AsmL does not have an explicit configuration sublanguage considered necessary in  REF _Ref9862309 \r \h  [30]. The main strength of AsmL is the unified semantic model based on ASMs. This is in contrast to many existing ADLs which lack formal semantics completely, or use different formal semantic models for components and connectors  REF _Ref9862309 \r \h  [30]. A rigorous semantics is often a prerequisite for many tool generators  REF _Ref9862423 \r \h  [28]. AsmL specifications can be used for automatic test case generation  REF _Ref9852754 \r \h  [25], conformance checking  REF _Ref9071428 \r \h  [4] REF _Ref9071433 \r \h  [5], and to provide behavioral interfaces for components  REF _Ref9564451 \r \h  [3]. Methodological guidelines and epistemological reasons how and why the ASM paradigm offers a mathematically well founded approach to high-level systems design and analysis of complex system behavior, also in relation to other formal methods, are discussed in  REF _Ref526065198 \r \h  [7] REF _Ref8545287 \r \h  [8]. References Abstract State Machines (ASMs), the academic Web site, http://www.eecs.umich.edu/gasm. AsmL, the ASM Language, the website, htt:p//research.microsoft.com/fse/asml M. Barnett and W. Schulte. The ABCs of Specification: AsmL, Behavior, and Components, Informatica, 25(4), 2001. M. Barnett, C. Campbell, W. Schulte, and M. Veanes. Specification, simulation and testing of COM components using Abstract State Machines. In Formal Methods and Tools for Computer Science, Eurocast 2001, pp. 266-270. IUCTC Universidad de Las Palmas de Gran Canaria, February 2001. M. Barnett, L. Nachmanson, and W. Schulte. Conformance checking of components against their non-deterministic specifications. Technical Report MSR-TR-2001-56, Microsoft Research, June 2001. A. Blass and Y. Gurevich. Abstract State Machines Capture Parallel Algorithms. Microsoft Research, Technical Report, MSR-TR-2001-117. To appear in ACM Transactions on Computational Logic, 2002. E. Brger. High Level System Design and Analysis using Abstract State Machines. In D. Hutter, W. Stephan, P. Traverso, M. Ullman, eds., Current Trends in Applied Formal Methods (FM-Trends 98). Springer LNCS 1641, pp. 1-43, 1999. E. Brger. The Origins and the Development of the ASM Method for High Level System Design and Analysis. Journal of Universal Computer Science, 2 (8): 2-74, Springer Pub. Co., 2002. E. Brger, U. Glsser and W. Mller. Formal Definition of an Abstract VHDL'93 Simulator by EA-Machines. In C. Delgado Kloos and Peter T. Breuer, editors, Formal Semantics for VHDL, Kluwer Academic Publishers, 1995, 107-139. D. Box, Essential COM, Addison-Wesley, Reading, MA, 1998. P. Clements, A Survey of Architecture Description Languages. In Proc. Eighth Intl. Workshop in Software Specification and Design, Paderborn, Germany, March 1996. E. Christensen et al. Web Service Description Language (WSDL). W3C Note, March 15, 2001, URL: www.w3.org/TR/wsdl. D. E. Comer. Internetworking with TCP/IP, Principles, Protocols, and Architectures. Prentice Hall, 2000. A. van Deursen, P. Klint, and J. Visser. Domain-Specific Languages: An Annotated Bibliography. ACM SIGPLAN Notices, 35(6):97-105, June 2000. R. Eschbach, U. Glsser, R. Gotzhein, M. von Lwis and A. Prinz. Formal Definition of SDL-2000 Compiling and Running SDL Specifications as ASM Models. Journal of Universal Computer Science, 11 (7): 1025-1050, Springer Pub. Co., 2001. Foundations of Software Engineering Group at Microsoft, the website, http://research.microsoft.com/fse. U. Glsser, Y.Gurevich and M. Veanes, Universal Plug and Play Machine Models, Foundations of Software Engineering, Microsoft Research, Redmond, Technical Report, MSR-TR-2001-59, June 15, 2001. U. Glsser, Y. Gurevich and M. Veanes. High-level Executable Specification of the Universal Plug and Play Architecture.. In Proc. of 35th Hawaii International Conference on System Sciences (HICSS-35), Software Technology Track, Hawaii, Jan. 2002. U. Glsser and M. Veanes. Universal Plug and Play Machine Models: Modeling with Distributed Abstract State Machines. To appear in Proc. of IFIP World Computer Congress, Stream 7 on Distributed and Parallel Embedded Systems (DIPES02), Montreal, Aug. 2002. Y. Gurevich and J. Huggins. The Semantics of the C Programming Language. Springer Lecture Notes in Computer Science 702, 1993, pages 274-308. Y. Gurevich and J. Huggins: The Railroad Crossing Problem: An Experiment with Instantaneous Actions and Immediate Reactions. Springer Lecture Notes in Computer Science 1092, 1996, pages 266-290. Y. Gurevich. Evolving Algebras 1993: Lipari Guide. In E. Brger, editor, Specification and Validation Methods, Oxford University Press, 1995, pages 9-36, Y. Gurevich. Sequential Abstract State Machines Capture Sequential Algorithms, ACM Transactions on Computational Logic, vol. 1, no. 1, July 2000, pages 77-111. Y. Gurevich and N. Tillmann. Partial Updates: Exploration. Journal of Universal Computer Science, 11 (7): 917-951, Springer Pub. Co, 2001. W. Grieskamp, Y. Gurevich, W. Schulte and M. Veanes. Generating Finite State Machines from Abstract State Machines, Microsoft Research, Redmond, Technical Report, MSR-TR-2001-97, Updated May 2002, to appear in Proceedings of the ACM SIGSOFT 2002 International Symposium on Software Testing and Analysis, ISSTA 02. HJLNVXZ  F\r{۬ttht``h;nmH sH h;nhE]mH sH h5hE6mH sH #j,h5hUmH sH #j,h-0sh?JUmH sH h-0smH sH jh-0sUmH sH h8mH sH h8mH sH #j+h5hUmH sH jh5hzUmH sH h5hzmH sH h5hEmH sH %89  FHJLTV*滯ïïwo`Uh5h+mH sH jh5h+UmH sH h+mH sH h5hECJ#j-h-0sh?JUmH sH h5hEmH sH #j-h-0sh?JUmH sH jh-0sUmH sH h-0smH sH h8mH sH h8mH sH #j -h5hUmH sH jh5hzUmH sH h5hzmH sH $4^rHISWs*+  nprx %4)7źźźźz͗#j.h5hUmH sH h5hgmH sH jh5hgUmH sH ho mH sH h5hE6mH sH h5hEmH sH h+mH sH h8mH sH h8mH sH jh5h+UmH sH #jx.h5h+UmH sH 07?\8ͯ펃q#j/hvyAh?JUmH sH h5hgmH sH hpfmH sH hEmH sH h8mH sH h8mH sH #jr/hvyAh?JUmH sH jhvyAUmH sH hvyAmH sH htmH sH hsmH sH hg1mH sH h5hEmH sH hl"mH sH %Z\^ :<>@FHŽὫŘwЉeЉŽ#j1h5h0UmH sH #jV1h5h0UmH sH jh5h7UmH sH h5h7mH sH hpfmH sH #j0hvyAh?JUmH sH hvyAmH sH h5hEmH sH h8mH sH h8mH sH jhvyAUmH sH #jd0hvyAh?JUmH sH "149<  :<>@FHLbźВtlZttMh5hCaJmH sH #j>3hhpfUmH sH hpfmH sH jhpfUmH sH #j2h5hUmH sH jh5hmJUmH sH h5hmJmH sH h5hE6]mH sH h5hEmH sH h5h7mH sH h8mH sH h8mH sH jhvyAUmH sH #jH2hvyAh?JUmH sH b >XZh*5]$jɺٺq`O h _hCJPJaJmH sH  h5hCJPJaJmH sH hh$kCJaJmHsHh5h$k6CJaJmH sH h5h$kCJaJmH sH h-pBh [CJaJmH sH h-pBCJaJmH sH h5h [CJaJmH sH h5h$kCJ]aJmH sH hW4CJaJmH sH h [CJaJmH sH h5hCCJaJmH sH bD]wW3o$ & F 77L^7`La$gdo$ & F 77L^7`La$gdUYV$ & F 77L^7`La$gd$k$ & F 77L^7`La$gd-pB$ & F 77L^7`La$gdW4$ & F 77L^7`La$gd [ jrbrRC7ChhCJaJmH sH h5hCJaJmH sH h5hCJ]aJmH sH h5hdCJ]aJmH sH h5h[tCJ]aJmH sH h5hCJ]aJmH sH h5hCJaJmH sH h _hCJaJmH sH h _h6CJaJmH sH  h _hCJPJaJmH sH h _hCJPJaJh _hdGCJaJh _hdGCJPJaJh _CJPJaJ(*OQRTUXYZ\vw*W_l23ŵqbRCh5h7BCJaJmH sH h5h(~nCJ]aJmH sH h5h(~nCJaJmH sH "h5hg6CJ]aJmH sH h5hgCJ]aJmH sH "h5hI6CJ]aJmH sH h5hICJ]aJmH sH h@3hICJ]aJmH sH h5hCJ]aJmH sH h5h6CJaJmH sH h5hCJaJmH sH hoCJaJmH sH  7m4Y[]_`񰠐~o`P`D`D`4hhANCJ]aJmH sH hJCJaJmH sH h5hAN6CJaJmH sH h5hANCJaJmH sH hhANCJaJmHsH"h5h7&6CJ]aJmH sH h5h7&CJ]aJmH sH h@3h7&CJ]aJmHsHh5h7BCJ]aJmH sH "h5hP06CJ]aJmH sH h5hP0CJ]aJmH sH h5h7BCJaJmH sH h5hP0CJaJmH sH 7oo$ & F 7W^7`Wa$gd49$ & F 7W^7`Wa$gdJ$ & F 7W^7`Wa$gd'@$ & F 77L^7`La$gdW4$ & F 77L^7`La$gdJ$ & F 77L^7`La$gdUYV 79;n4P 267ɺyiy]WQWQWKW] h49PJ hJPJ h'@PJh'@CJaJmH sH h5h6ba6CJaJmH sH h5h6baCJaJmH sH "h5hF)6CJH*aJmH sH h5hF)6CJaJmH sH h5hF)CJ]aJmH sH h5hF)CJaJmH sH h5hCJ]aJmH sH hhCJaJmH sH hW4CJaJmH sH hCJaJmH sH 7Cg $%&34QnoĴߥӇĴ{l{\O\hJCJ]aJmH sH h5h}CJ]aJmH sH huhuCJaJmH sH huCJaJmH sH h5hdCJaJmH sH h5h49CJaJmH sH h49h49CJaJmH sH h5hC6CJaJmH sH h5hCCJaJmH sH h'@CJaJmH sH h49CJaJmH sH  h49PJh5h=1ICJaJmH sH 4v(p))*+ ,w,,(--.....&`#$gd8A$a$$ & F 7W^7`Wa$gd'@$ & F 7W^7`Wa$gdJ$ & F 7W^7`Wa$gduovw(u(v((d)n)o)p)οwhWEW4 h'@0JL6CJ]aJmH sH #h5h!0JL6CJaJmH sH  h5h!0JLCJaJmH sH h5h!CJaJmH sH h5hCCJaJmH sH Uh5h~6CJaJmH sH h5h~CJaJmH sH h'@CJaJmH sH hJCJaJmH sH h5h}CJaJmH sH h5h}6CJaJmH sH h5h}CJ]aJmH sH "h5h}6CJ]aJmH sH D. Hamlet and J. Maybee. The Engineering of Software: Technical Foundations for the Individual. Addison Wesley, 2001. J. Heering. Application software, domain-specific languages, and language design assistants, in: Proceedings SSGRR 2000 International Conference on Advances in Infrastructure for Electronic Business, Science, and Education on the Internet, May 2000. J. Heering and P. Klint, Semantics of programming languages: A tool-oriented approach, ACM SIGPLAN Notices, 35(3):39-48, March 2000. ITU-T Recommendation Z.100: Languages for Telecommunications Applications - Specification and Description Language (SDL), Annex F: SDL Formal Semantics Definition, International Telecommunication Union, Geneva, 2000. N. Medvidovic and R.N. Taylor, A Classification and Comparison Framework for Software Architecture Description Languages, IEEE Transactions on Software Engineering, 26(1):70-93, January 2000. R. Strk, J. Schmid and E. Brger. Java and the Java Virtual Machine: Definition, Verification, Validation. Springer, 2001. S. Thatte. XLANG: Web Services for Business Process Design. URL: www.gotdotnet.com/team/xml_wsspecs/xlang-c UPnP Device Architecture V1.0. Microsoft Universal Plug and Play Summit, Seattle 2000, Microsoft Corporation, Jan. 2000. Official Web site of the UPnP Forum. URL: www.upnp.org. E. Christensen et al. Web Service Description Language (WSDL). W3C Note, March 15, 2001, URL: www.w3.org/TR/wsdl XLANG Abstract Machine, Foundations Of Software Engineering, Microsoft Research, Internal Report, 2002.  This author is currently at Heinz Nixdorf Institute, Paderborn, Germany. The work on which this paper is based was done mainly when he visited Microsoft. PAGE  PAGE 10 -  PAGE 2 - C GUI (VB) C C C Network P P SI Manager GUI (VB) P SAM P P SI Manager P SI Code generation Parsing Instruction sequences of XLANG Abstract Machine Service behavior WSDL Port map Abstract syntax tree of service behaviors XML text of XLANG contract Control Points Network D Devices CP CP D C C C C SAM Figure  SEQ Figure \* ARABIC 2. Communicators. Figure  SEQ Figure \* ARABIC 3. ChangeDisc service of a CD player. p))))))))****H+q++++ , ,F,G,񰡒sdUF7h5h. )CJaJmH sH h5h~2CJaJmH sH h5hICJaJmH sH h@3hICJaJmH sH h5h-z6CJaJmH sH h5h-zCJaJmH sH h5h5h8hM>CJh5jh50JUh5h FQ<mH sH h5h0gCJaJmH sH h5h0gmH sH h _h0gmH sH h5h. )mH sH h _h. )CJaJmH sH h5hF)CJaJmH sH h'@CJaJmH sH "h5hb6CJ]aJmH sH h5hbCJaJmH sH h@3h'@CJaJmHsHh _h#CJaJmHsHh@3h. )CJaJmHsH .K.M.{...........................................ſſſŰſϓ|s|h@6mH sH h@*h@6mH sH h "h@mH sH h@mH sH hVYwmHnHujh@3Uh@3h50JmHnHuh5 h50Jjh50JUhVYw hh5 h8CJh8h5CJh8CJmH sH h8hM>CJmH sH -......................$a$gd@gd@  h]hgd@3h]h&`#$&`#$h]h................///////////// /!/"/$/%/&/.///0/2/3/4/6/7/8/H/I/Q/V/////////////////鸭鸭鸭鸭鸢hxNh5mH sH hW?dh5mH sH h5mH sH h_<h56mH sH hZ}h56h@*h@6mH sH h@6mH sH h5h "h@mH sH h@mH sH ?.........//////////!/"/%/&///0/3/4/$a$gd:0gd@ $a$gd@4/7/8/H/I/Q/R/S/T/U/V/////////////00 $a$gd:0 $a$gdo.gdo.gdo.gd@///00 0 0 0 0000000000 0"0#0%0&0(0)0+0,0-0102090:0P0Q0R0S0c0d0e0l0m000000000׽Ʊh5h FQ<mH sH h FQjh%Uh%hkmHnHuh8mHnHujhkUhkh@*h@6mH sH  h:0h5h5hZ}h56 h5600 0 0 0 0000000 0!0#0$0&0'0)0*0,0-01020d0e0gdk $a$gd@ $a$gdT $a$gd:0e000000A$a$gd%50&P P:p@3. A!. "#p$%`!QLa,ܿKGo 8{.Vx] xW۞g33g"+X(VKARZBkت%j'$J"JJѯVW >Dy߉Zw'g{y6N&OJ$1S T HR$QIJH/$IjJX%%TZ**U *BݍH;Hfּ$#ܮ W*)m%KB @IQ IxWOr!y9{lȳTzR?[[H5O6J|zr_J~@>q+ [o*,=1MwY %vMjz5tf)E1%SsC{TiΟ6?(i}}񭥕U>efk>"=b sۧ;#*âtIJ7En|HT&ivz t:uv.-\O|>6_gDx%}:}EMKi|<0V/Fb:ceD̡k|^&RG'gg'G6x}#Fdf =۠o;x; c!x ŽͰ'vm}ػvz,<>;<;[G-Ӗ`ѫ|uxev+}*Oz2OD?\"h]1Fd[LT:2OHW`D:h|؉؃5W#]JFZ[oz=/z߃ c+l-<Laz6Zհw%^NM)9i$`a$1&M=|+HTXe^(&FSaq/(›U"b!Eȧ| . /AO:Cog RN=Ŏ. ]|]R5 w@v}(rCSbO> '( dd7dʷ=3&UX V[ߓd/&l2/^Al7R9g8e;9ayߠw^U\^!S!ioEQwޠD `E5*i8{RX`QZa=iҲȗGyEWFGQ5j;e{'HZM @C<o5aG (zUaoy]Ih<{Lz0 |x;3Y!x4ϥU^'K $^ _/=#~;-ݠ!dHc^ nZa^GkeP^!hWCYVѪxZQk=jmx<^!] OBBQkixqv~( GD}cw?Kn# |k<=w xD1 ]a{cawn$}'(Iœy/c~b~3x/xC~x8j=j2ʳQOyڐZc^Fk«jy=%ouF;`GNh5QOqx ?8#7OD^#o8x&PA9>r8I⾓+$iUێmy M A@@!c!SPvK>|GwB}gFA艁荆&~A$$D氢%$uT[ng!!C ($ǂq.#/;@OkU6WfA꟯jyUkr[-ck*A^6C*+e;,aRSJ ; CDÎ)=wQsH;ޑfnި[**D~gxqϓq^&d*IU<:dSGj9&VILJjϑǵ8NGⴾdև#BO^0RUMI>gX}/% d& ䷠<~?~G3 FqDcy|~vdÞ-+5i$ ?V Ԩ#↎O}XAB!}|sz%/I f {s/LbW;;2ߜ]LwNG ]қ-#2il YƓul$fC7l aqD㱤2K>i| C!>5>j ). !2RU]CnE Q~?i?~W_9<ʣx4/,7EH5sX lF/Jbv|σiv=î]Ĵ`q"%Vssh5tc)(5l6gq%VJx?95,I1w=9=Caޜޫue(F*(; Y`܃L0Vk1B+Wk@([ۑͱޱ^l>}9L}-nCށPz8JcWxQkt}=g #F уzfL0N*n8˦CYwVz %Soduǔ0^IrJ QZ.J)-E1(H!ߠ,R(0*)M0%xLeUF e7:+H ? v~*@гRw)/ _+gx-T\{O`hؕ>ioӕFe^cq8Z"!aDĎ69*Žh~d/VWcm(IX#w*5,nԡYtр~m4'V4LjcpZ&p"\KnOі&s(C}zZtь]_Z Ð,wxa/ClAF0{(bQuDs$ڡ.m"tW+ 9h!-|y,3th;<Q^.`|,-sLsӷ=ص5 6mo\4;7[S w=~:B ~nPou4(D}w 9f~04<+')gDulޖ __{57xoyZ=+z'Nx=idOX9\=pOmHG:Hl=8YQɞRtϣF1Ht2^0V{zoy56 ݌F>A83 9ss~3y|w ]aعc[0'j ho|#Gn=;G;jbnnn^v|(\!R܅@SL Un 0r?I&z"V#+9C$B(:S2:er.4p!Mˤq45ndj,!ed$1\C џ|%EYsPab'IWBډ%XC,i)Eh(C4v[ɫ`BT~Iԗ'"T( 7{OHċ^$edXHdI&fKΈXNn776BRGJߒA ?!QBV ^[y{]o'b5x!ZrT#?wɏb#9%6/W)9+BB|jg5-&MH{] 쯗B@})sUF FW Y/?W{:qzf-65r+U Y*.Ő^Ur1Y`3^@ ۽Bqd.:+. lssWԛmgTWݫ<.n+!/[S.B.)w {=pZ[vL0Wb 7 x,6۠cvGFHgs;ﵲ $gRb6Eq[­f 7 'k>>N|G[&zm8=Np~.˙hR9,XvmA+T8@)A-/ߗfm ڗoMس^=+?Z),\l&ny<}yXWtdoy* >ev]F[mvnܾw?sw3ܻlq5?5;J65*8eo'l6nMں`z6G8&no>nv[FYclvH#,y6qGwYܕ_} g:ڻ? Q'&T~.wʹfX{ln.Z漲 5q}'oi8eo_~;&noNu=Q6(Gplt '6q7w?l!-ܓ6qco=GFoo$bp~ ̡o Tϒgj~:6qsŝbn; [g_9&Wq M{n{&y:bRn.p?n5g;D`&oTgF?ۑx_S}o6[pOYj pTqoX6qJ\pK n1E,r6q܇,܊6q܇-*6q _ZG]ŚϿ\cq~dž5ǖsk>O vƗa7n= \OvpÁpye7H ü8}bsrl>6͖m69 ijg;ϝǭ`6܊pg¿o o.t.to7տg3XAt6NЇ4?{Wva=wbJNaEwUfD$Yy.b! V"}(v]-G|*0_+tрxDOU^C Dag=ևޏ= =[Az[cy;=x3i_ҌgI`t)}36J79t5l`59۝A(Eγuv}F"oye on7jōFmqQ[ܨ-n7jōFmqQ[ܨ-n7jōFmqQ[ܨ-n7jōFmqQ[ܨ-n7jjFmq"ܨ-n7jōFmqQ[ܨ-n7j-FmqQ[ܨ-n7jōFmqQ[ܨ-n7jōFmqQ[ܨ-n7jōFmqQ[ܨ-n7jōFmqQ[ܨ-n7jōFmqQ[ܨ-n7jōFmqߓy9 82ndESoξ?PwQ)&2*?U˭[ )-`!Zip`(8K x-9(xw|UEo һ:PzINE0%D:JyP:TQCGC`Ky?N盳e=;s$N}> '/ : VN ={6Ǥ>V3~|{(FJpWIZB=huԍ(E]#UTzSjznwDPکFF5>SѴTMEj2ViI<`K9uU[Io^6R':CԏD]W>p-9\=UZP \CMj)ڶ/u~rucF}9.Pu'@X:Z WeC*V*%*dW%7Ւ@PSBͥz46҂J[j'̤ޒo.r!w)BrOIƑd^RPW{Hk&җ@n)ùDs#d&ג\Cr|̯R~UVpUYV+uyYց l*+V~N\IvrEA︼rr2rK\R.s &-p?##I%Y%L)TRKYyBGkeTKu pPCǻ nsm:8cr]+Gk>rJfGn,繉 ry[^nw&flᶲ˿-^'dY+ B+L(d, A(;R RcޒW6wŕ q޴}~,x_ 7W>UXaT'%lykvRKh3>Ŵ?!-4P ϦhI}3/G=x:uiԁЛoR9nVeUn$~-$=+ll䴗%*kRސP~ uuib/IKt礫^"1gcJz/]!vtJ;_:Y;MIڎv4C/l?9z^ԉv<5m԰=%FHuujTe^^oJeT #lM)o_/K"m%)hä-'ORx<6D>#Yl>S^dsS6-d3'Mϧis6%߲8Я9I9>_8?O)(|o_BY`2 hIз3=m(5:e7I#JoH =צ$Z \j\<6-uhKsl=e ۀ޳hmBSm3-imKmGgQAcm47 }h}w;aiGQCl4u-;ۉD-m a'S3NƠ!:x^AEPNRYPdQ;Ρ@;nyt̥Sf}2hI Zl"3c&,37hOq4L5`C=)f M1`M83ƚ4 f(EADQgӟژuӇ^TD˦U6)tR4m(iI4#iB4&4$!xtM78pF7)inA6LE uW#iu)Bz$5c)\OWDz^O򠤎Bz*QV=s(OV@?@R!G o}wO{_ |? 軅c$I}~*nR{^g%2ʯ8*moaܢ87 p\#GC#{ٽ:CQduVS4t9F QpCwFjjjg4e-X֣4nl(e7zُhM+J z_ Pڥ ?v8tGQ;Xԍ]/4 v > ~qd߃gcD9?zUĆ+v]PhP::կWWJJuᯍ|m\}`/؃fs-6ovq8eESP.P\DLQ\@<8fQ dY gƞ&4{=>[Q 5@MPKHۦ2σP(w]SA޶A{H ̨Keۀ֠h~ Z`{"1`2JJR D PƮQv8$'}d50o冼&nJVO;/> G"yqoڼyUuJ**+ 9RO2^OŸS0o&8ܡt>K:Eohv9--4iOS&NCh&~ !FjFpF; Ƈ*EgK!:N@E)+Rз7wtQ3(U'uS]:m]b UJxJȖD؉ 09'{/<{?=ݽURf#.|&@Do +  !6|'Z+>;~X]^XGlWWW Myu ޶+jƒxPƒ<P`;I|9qU 㸂 i\vv|w:6:~{y 5@bӡg*|-UT~rtJi׏k㟟{=~DgO)(W/b\Iry]KRr!ו9~sjSs])hqvݙsΫ.@.ǀ\Bg$.ra=zpA o@&ێ񻸤e!~IW1Op=}9h ڀwq]_H}wy!:XFj%dmdN&surYSRV` [~902;\Zn>6o2I EҚl䐬&2iGBL^)J|R@5B&43YƷ7OJgFzXgHL 6x%*7y23x ,/i7y0W8\6g9ajf/2;wzgV⸒l. jq;Y\NPål4#̕l?~ʶ3Wmql1?grE[ۗ%m?kKB| ;9=?ElR8=goQ.{toS.dQR{A ntl+f#ř tάSf 3)֬f%6`-h[>4|N4z&h>QcclG͠j|UT6T4_R9ʛTbf'mm&z BwrtSoz ]A'n:A}룴WtR-?ׇi;Z<0L@H~} OS'}KB_.5\W )N:+WyAvbCbR/x''!O)NlqIP')ʼnz17}/ k#Ye=>| ?^ȷ\if|Tp;.λXߍ1hCpT_.=LTNtD@s5h ]>WTLOYȭ8LZG矑=|r|yꋋ?waSofᯬXA䌮IE\V=jRuP+g rI lC`[I9 pI;qJUJ9q *MwMBku( juF.\N/VUr1ZwBhыK<>yXsrFo .OF9='snO'%=,R JᠤK!$s A9ĕP:r+\BPql)P湔[!;ǀkk\y{]bQuSwE9֕SB~%XW. jĢoĢ>maC<01^n !;˃ʻ_lRFo.*zRhݮy,UwRC}+=|wY5̦QZZh|_9+[l4o@:>Dϙ{xg?fwCmã?mas?r˷e=&{\×S_˳\3Yg=,P0ޗ_+K?$| ,8m\ 5 αv}g㥒*:wܩ///-'Ic(:sWC.;ž''(keFum]:tRȱ<^}`_NXxb[%kUGUCҸڃkPUwޡS,=9u1d%s -^/OSSe"2xL^&/De"2xL^/{=}_/{/{=rx}=b{rx^/{=rxK^/C!rx9^ǗC ="yDyK  _Ref9559788yDyK  _Ref9560551}DyK _Ref535815723yDyK  _Ref8441174yDyK  _Ref9559788yDyK  _Ref5622720}DyK _Ref535816125yDyK  _Ref9563257}DyK _Ref526062066}DyK _Ref535385772}DyK _Ref526062086}DyK _Ref515900185}DyK _Ref526065198yDyK  _Ref8545287yDyK  _Ref9560551yDyK  _Ref9852754yDyK  _Ref9564451yDyK  _Ref6385476yDyK  _Ref9564844}DyK _Ref525673966yDyK  _Ref8547871yDyK  _Ref9853040yDyK  _Ref9853287yDyK  _Ref8547211yDyK  _Ref9853477yDyK  _Ref9611724yDyK  _Ref5622720yDyK  _Ref9825688yDyK  _Ref9759101yDyK  _Ref9759101yDyK  _Ref9855617Dd & LMD  # A#" `2?x44y-MW `!x44y-MW6! ; Y;p+ xڽ s=NĮ*VrmJ E:XBy!c]]]:~(tE0 ^ / ѱ8YCYCNC1:Fu; z Y/N/n/+t{ p>:: s~p#a:hc ^! >{}$b-{9jSp2:k"kimsrQN$3HwYWYWNWneNm[63;Sn66܊1FFsFsܚ$܏UxOVsVsWf`:r6M63{t'a^xMVé輦W 1g+e+9+<$d9u~asll;g;=NB|[fj^uttV_VS{Qu; ulM3+ sP^W9qp7 a]]]:~"48#~A%z]<Ǽ8'c554slTpz'ҹB׽B:: s~p#a$\ Wqq\^!yqpO]uutvѹ(Iɘ;eS9SSuuǼ8'ޤ32IeXGe+8++tu<7ΪdU*uu; /c ]666w5+1/ au:/; Dp/(Jy,yqpO>{}$b-{9+1/ &&&ܦ:'$\A:t+1/ YWYWNWneNm[63;Sn] y̋{Bll4g4wέNX'l5g5wΓP +p jҝ7;K[g{<=!FVéᾮF* ptаx<+z]<{FrOw{}$n\:h+1s9k&ki=MyqNBO\Q.S}q^yNnnn:=ҝbSЙ{0puƥ; 3555:>m),ƃx""":; !>^^^=o9[/[Y}KgCr8rCgdy^C,p:Qn':Btuuwyn^hZ%tBւӂ{Nt'/bFpFpG fc(t[֛ӛ{Nt'a *1Usc*ݹ6*11DDD$NrVNg6^r,#ΖʖrrY$l|}|ssuyqYݭ)JfT2'4),,:vyJd9N[SZRRtqʸe:]u+y^>'ឭ6Iq Fppuyq_֟ӟ{΀t'ac jN5Z^!=!llg.N*W񚬆SíyM׽B{BxJJJc:; ;9AAAtి_mVϜw˼e!_4o\Ҽ;Ծ̅g]ҟؐ4[Zʯ;?uz?[?w|>oqKތ>/.g6'ZԻ|uQ?=]Te&מ }=5d&eF2ۢZ. j^?C~扵zi[8ҿ]t˰7恃nL߿ϜwYk<Ԯ/ yDyK  _Ref5622720yDyK  _Ref5622720yDyK  _Ref9825688yDyK  _Ref9560551wDyK  _Ref238236yDyK  _Ref9399949yDyK  _Ref9859595yDyK  _Ref9399949yDyK  _Ref9860172yDyK  _Ref9860197yDyK  _Ref9860172yDyK  _Ref6385476yDyK  _Ref6383438yDyK  _Ref6382768yDyK  _Ref9860172yDyK  _Ref9860694yDyK  _Ref6385476yDyK  _Ref9860694yDyK  _Ref6385476yDyK  _Ref9675553Dd D  3 @@"?yDyK  _Ref9564844yDyK  _Ref9565950yDyK  _Ref9690428Dd D  3 @@"?yDyK  _Ref9862006DdD  3 @@"?yDyK  _Ref9862006yDyK  _Ref9564844}DyK _Ref525673966yDyK  _Ref9862233}DyK _Ref525673966}DyK _Ref525985481yDyK  _Ref9862309yDyK  _Ref9862309}DyK _Ref525981826}DyK _Ref515906955yDyK  _Ref9862309yDyK  _Ref9862309yDyK  _Ref9862423yDyK  _Ref9852754yDyK  _Ref9071428yDyK  _Ref9071433yDyK  _Ref9564451}DyK _Ref526065198yDyK  _Ref8545287YF@F bNormal $xa$CJ_HmH sH tHf@f Heading 1'$ & FQ<@&^`Q5KH \^JaJ f@f 9,A Heading 2'$ & FB<@&^B`5\]^JaJR@R X{ Heading 3$ & F<@&5\^JaJL@L Heading 4$@&5>*hmH sH tHu@ Heading 5S$ & F$d%d&d'd@&NOPQ>*hmH sH tHuR@R Heading 6$ & F@&>*hmH sH tHu@@@ Heading 7 & F<@&D@D Heading 8 & F<@&6L @L Heading 9 & F<@& CJOJQJDA@D Default Paragraph FontViV  Table Normal :V 44 la (k(No List >>  Footnote TextCJaJ@&@@ Footnote ReferenceH*4 @4 Footer  !.)@!. Page Number4@24 Header  !@YB@  Document Map-D OJQJB"@B Caption$`a$ 56CJ6U@a6 Hyperlink >*B*phdC@rd Body Text Indent%$h7$8$H$^h`a$aJFV@F FollowedHyperlink >*B* phTR@T Body Text Indent 2h^h`,X@, Emphasis6\B@\ Body Text<$d%d&d'dhmH sH tHu:O: Domain6:mH sH tHu4O4 Macro:mH sH tHu:O: Function6mH sH tHu6P@6 Body Text 2CJ0O0 ASMKeyword58O8 SDLKeyword 5OJQJjO"j RuleAndDefStart1"$ 3Nj @@@@@@@@^a$4O!24 RuleAndDef#TOBT BulletList $ & FCJOJQJmH sH u2OQ2 DomainName6:4Oa4 FunctionName6>0@r> 2V List Bullet ' & F)CJH1@H List Number( & F 9DG$H$PJ @O@ Note) & F CJPJ dOd Note numbered'* & F `^`CJPJ HOH Done+ & F 4CJPJ <O< Figure,$ & F@&a$CJ@O@ AbstractSyntaxName66O6 InvisibleNote<8O8 Aufzhlung / & FHS@H Body Text Indent 3 0h^h,O, ASM_Name6BOB AfterRuleAndDef2CJ`O` AppendixTitle 13$$$ & F@& 5:CJ$XOX AppendixTitle 24$ & F,<@&5CJ TOT AppendixTitle 35$ & F<@&CJ^Ob^ Standard-noblock6$ & F e^e`a$CJ.Oq. MacroName:6O6 ASM-Keyword5CJTOT address9$`a$CJOJ QJ mH sH uPOP email:$`a$CJOJ QJ mH sH u~O~ FunctionStart9;$$ 0Pp ]^CJmHnHu:O: Paragraph<5CJ\O\ HCode Char Char=$CJOJQJ^J_HaJmH sH tH <O< | codeintextCJOJ QJ ^JFg@F HTML TypewriterCJOJQJaJNQ@N Body Text 3@$a$5CJ\mH sH uROqR LiteraturAx^`CJmHsHu0O!0 ModuleName:H2H  Balloon TextCCJOJQJ^JaJPBP SprechblasentextDCJOJQJ^JaJ:OR: Function ParaE6TORaTFunctionStart Char_HmHnHsH tHuPOrP .BN QuotationG$Tx`Ta$6CJmH sH bOb ="XCode Char Char Char$CJOJQJ^J_HaJmH sH tH fOf SFB blockquoteI$x\$^a$6CJOJQJaJmH sH tH jT@j E Block TextJ]^`6CJ]_H aJmH sH tH VOV  NumberListK$x`a$CJaJmH sH tH 0a@0 ! HTML Cite6]*W@* gStrong5\vOvRO_AsmL0N$dd*$-DM \$a$m$#CJOJ QJ aJmHnHsH tH u4O4 2VCodeChar CJOJ QJ NON  Itemized List P & F+aJmH sH tH <O< T AsmL Literal CJOJ QJ RO!RNO_ AsmL Char'CJOJ QJ _HaJmHnHsH tH uO12 r1Style Heading 3 + Before: 0 cm First line: 0 cm S & FCJLOAL |Style codeintext + 12 ptaJFOQF dG headlines15CJOJQJ\aJo(:L@b: 8Date V$a$ mH sH tH DOrD ?CodeW OJQJ^J_HaJmH sH tH VOV zx(Heading 3 Char"5CJ\^J_HaJmH sH tH,#'+/9CGLPTXbfj{"2<?HLPSVY\_dohgfeca`_^pwtsvxyz{|}*#'+/9CGLPTXbfj{"2<?HLPSVY\_d   !"#$%&'()*F !}X +=.FJU0pf !n#+%V%&&d')))%+8+%,C,V,?-c-y- .2.Q...."/A0011R1~113A444#5*6@6T7q7788"939;<?==>>a?@4B^BB*EOEEGHIIKKK5LJLiM{MNNOOO\PtPPPQQQQQQ/R@RHR[RRVSySU.UUUVVVVWWoXXYYYZZZZ[\\\]]]] ^(^?^^`)`L`[`x`Rbsbccff f#f$f%f&f'f(f)f*fgi7jNjlkWmdmwmmppp6qqqqrLrrruswuuuowwwxxxx yzz{{{2}E}S}}}}}.~q~~~~7D{<Yiu`vג% (4Pf{љ}"/<Y|Ş =Li}ԟ:)OXX"R@Ӯ:$B[rhuƵ޵ 1FXrշKYe¸˸ָܺ.LzAPg+@Sh-9X1[" .EnMf#.AZtT0 @000 00^@0^  0@0@0@0@0@0@0@0@0({00T/:0T{00T/:0T+z00d80d{00T/:0T+z00d80d+z00d80d+z00d80d+z00d80d+z00d80d+z00d80d+z00d80d+z00d80d+z00d80d+z00d80d+z00d80d+z00d80d+z00 d80d+z00!d80d@0(@0(@08+z00%d80d{00'T/:0T+z00'd80d+z00(d80d+z00)d80d+z00*d80d+z00+d80d+z00,d80d+z00-d80d+z000d80d+z001d80d+z002d80d+z004d80d+z005d80d+z003d80d+z007d80d+z00:d80d+z00d80d{00>T/:0T{00?T/:0T{00@T/:0T{00AT/:0T{00BT/:0T{00CT/:0T{00ET/:0T{00FT/:0T{00GT/:0T+z00;d80d{00IT/:0T{00JT/:0T{00LT/:0T{00MT/:0T{00OT/:0T{00RT/:0T{00ST/:0T;00TT/:0T@08@08@ 08@ 08@ 08@ 08@08@0?@=0?@=0? @ 0;00aT/:0T{00 D/:0D@0D@0DA 0DD@0H@N0H@N0H@0H@N0H@0HA 0DD@0sL@N0sL@0sL@N0sL@N0sL@0sLA 0DD+z00Kd80d+z00Ld80d@0O@N0O@0O@N0O@N0OA 0??@0K@N0K@N0K@N0K@0K@0K@N0K@0KA 0??@0O@N0O@N0O@N0O@0O@N0O@0O@N0O@0O@N0O@0O@N0O@N0O@0O@N0O;00t/:0tA 0??@0U@0U@N0U@N0U@0U@N0U@N0U@N0U@N0U@N0U@N0U@0U@0U@N0U@N0U@N0UA 0ZZ@0j@N0j@0q@0q{00D/:0D@0q@0q@0q@0q@0q@0q@0q@0q@0q@0q@0j@0q@0q*B 0qq@0v@0v@N0v{00D/:0D@N0v@0v@N0v@N0v@0v@0v@N0v@N0v@N0v@N0v@N0v*B 0qq@0@0@N0@N0@0@N0@0@0@N0@N0@0*B 0qq@0@N0@N0@0*B 0qq@0@N0@N0@N0@N0@N0@N0@N0@N0@N0@N0@N0@N0@N0@N0@0 @ 0@0Z@I0Z@0ZA 0ZZ@0#`@0#`@0#`*B 0#`#`@0d*B 0#`#`@0gA 0ZZ@0j@N0j@N0j@0j+z00d80d*B 0PoPo+z00d80d+z00d80d+z00d80d+z00d80d+z00d80d{00D/:0D+z00d80d@N0u@N0u@N0u@N0u@N0u@N0u@N0u@N0u{00D/:0D+z00d80d{00D/:0D+z00d80d@0u+z00d80d{00D/:0D{00D/:0D@N0u{00D/:0D{00D/:0D{00D/:0D+z00d80d@N0u@N0u{00D/:0D@N0u@N0u@N0u@0j{00D/:0D{00D/:0D @ 0@0@0@0A 0@0@0A 0@0}@0}@4 0}@4 0}@0}@0}@0}@0}@& 0}@& 0}@0}*B 0}}@06@06@N06@N06@N06@N06@N06@N06@N06@N06@N06@N06@N06@N06@N06@N06@N06@N06@N06@06@N06@N06@N06@N06@N06@N06@N06@N06@N06@N06@06@N06@N06@N06@N06@N06@N06@N06*B 0}}@0@0@N0@N0@N0@N0@N0@N0@0@N0@N0@N0@0@N0@N0@N0@0@N0@N0@N0@N0@N0@N0@N0@N0@0@N0@N0@N0@N0@N0@N0@N0@0 @ 0@0´@J0´@0´@0´@0´@0´@0´@0´ @0@ 0(@ 0(p@ 0(p@ 0(p@ 0(p@ 0(p@ 0(p@ 0(p@ 0(p@ 0 (p@ 0 (p@ 0 (p@ 0 (p@ 0 (p@ 0(p@ 0(p@ 0(p0R !OPYZl{|}~}X +=.FJU0pf !n#+%V%&&d')))%+8+%,C,V,?-c-y- .2.Q...."/A0B0011R1~113A444#5*6@6T7q7788"939;<?==>>a?@4B^BB*EOEEGHIIKKK5LJLiM{MNNOOO\PtPPPQQQQQQ/R@RHR[RRVSySU.UUUVVVVWWoXXYYYZZZZ[\\\]]]] ^(^?^^`)`L`[`x`Rbsbccff f#f$f%f&f'f(f)f*fgi7jNjlkWmdmwmmppp6qqqqrLrrruswuuuowwwxxxx yzz{{{2}E}S}}}}}.~q~~~~7Dxyz{<WYiu`vג% (4Pf{љ}"/<Y|Ş =Li}ԟ:)OXX"R@AӮ:$B[rhuƵ޵ 1FXrշKYe¸˸ָܺ.LzAPg+@Sh-9X1?[" .En%&Mf#.AZtT0 41lfm %&)*-.>?GHIJKL|}  "#'(Z[@0 0p00p0pV0p000lp0l0l0l0l0lp0l0l0l0p0p0p 0p000p0000 0p0. 0..p0J0J( 0JJp0p0p0p000p0p0p0p0p( 0JJp0&p0&0&p0&0&p( 0JJp0%+p0%+p0%+p0%+p0%+p0%+p0%+p0%+p0%+p0%+0%+0%+p0%+p0%+(0%+p0%+p0%+p 0..p01p0101p01p0101010101 0..p0*6p0*6p0*6p0*6p0*6p0*6p 0..0"9p0"9p0"9p9 0"989 0"9p9 0"9p9 0"9p0"90"9p0"9p0"90"9p 00*E0*Ep0*Ep 0*E*Ep0IpN0IpN0I0IN0Ip0I 0*E*Ep0iMN0iMH0iMN0iMpN0iM0iMN0iMp0iM 0*E*Ep0PN0Pp0PN0PpN0P 0*E*E0QpN0QpN0QN0Q0Q0QpN0Qp0Q 0*E*Ep0UN0UpN0UN0U0UN0U0UN0U0UN0U0UN0UpN0U0UN0UpN0U 0*E*E0Zp0ZN0ZpN0Z0ZN0ZN0ZN0ZN0ZN0ZN0Z0Z0ZXN0ZpN0ZN0Z 00[`pN0[`p0[`N0[`p0[`0[`p0[`0[`p0[`p0[`p0[`p0[`p0[`p0[`0[`p0[`p0[`0[` 0[`[`p07j07jN07jhN07jN07j07jN07jpN07jN07j07jN07jN07jN07jN07jN07j 0[`[`0rp0rpN0rpN0r0rN0rpN0r0rN0rpN0rN0r 0[`[`0xN0xpN0x0x 0[`[`p0{pN0{pN0{N0{N0{N0{N0{N0{N0{N0{N0{N0{N0{N0{N0{0{0{p0{p0{p 0p0{I0{p0{ 0{{p00p00p( 0p0Yp( 0p0up 0{{p0`pN0`pN0`0`0`p0`0`p0`0`p(0`p0pN0pN0N0N0N0N0N0N0N0N000N0pN0N0N0N00N0N0N0N0N0N0N0N0N0N0N0N0N00 0p0)0)p0)p 0))p00p 0))00p< 0p< 0p0p0p00p0p0p& 0& 0p0p( 0p0Bp0BpN0BpN0BN0BN0BN0BN0BN0BN0BN0BN0BN0BN0BN0BN0BN0BN0BN0B0BN0BpN0BN0BN0BN0BN0BN0BN0BN0BN0B0BN0BpN0BN0BN0BN0BN0BN0B( 00L0LpN0LpN0LN0LN0LN0LN0L0LN0LpN0LN0L0LN0LpN0LN0L0LN0LpN0LN0LN0LN0LN0LN0LN0LN0L0LN0LpN0LN0LN0LN0LN0LN0L0L0L0Lp0L0Lp0L 00J0p000p000p0p 0#p 0#p 0#p 0# 0# 0#p 0#p 0#p 0#p 0 #p 0 #p 0 #p 0 #p 0 #p 0# 0#p 0#p 0# 0# 0# 0# 0#p 0#p 0#p 0#p 0#p 0#p 0# 0#p 0#p 0#p 0#p 0 # 0!#p 0"#p 0##pA0p@0p0a@0@0@0@0@0@0@0@0@0@0@00xa 000000000000000000000000000000000000000000000000000000000000000000000000000000000000000:0Wa !OPYZ{|}~}X +=.FJU0pf !n#+%V%&&d')))%+8+%,C,V,?-c-y- .2.Q...."/A0B0011R1~113A444#5*6@6T7q7788"939;<?==>>a?@4B^BB*EOEEGHIIKKK5LJLiM{MNNOOO\PtPPPQQQQQQ/R@RHR[RRVSySU.UUUVVVVWWoXXYYYZZZZ[\\\]]]] ^(^?^^`)`L`[`x`Rbsbccff f#f$f%f&f'f(f)f*fgi7jNjlkWmdmwmmppp6qqqqrLrrruswuuuowwwxxxx yzz{{{2}E}S}}}}}.~q~~~~7Dxyz{<WYiu`vג% (4Pf{љ}"/<Y|Ş =Li}ԟ:)OXX"R@AӮ:$B[rhuƵ޵ 1FXrշKYe¸˸ָܺ.LzAPg+@Sh-9X1?[" .En%&Mf#.AZtT0 41lfm&*-.>?GL|}'@0000@0D@50@0@0@0@0@0@0@0@0@00 000  00=0=0=0=0=0=0=  00I 0II0b0b* 0bb0000000000* 0bb0&0&0&0&0&* 0bb0<+0<+0<+0<+0<+0<+0<+0<+0<+0<+0<+0<+0<+0<+0<+0<+0<+ 0II010101010101010101 0II0?60?60?60?60?60?6 0II0790790799 0799 0799 0799 079079079079079079  00>E0>E0>E 0>E>E0JN0JN0J0JN0J0J 0>E>E0|MN0|M0|MN0|MN0|M0|MN0|M0|M 0>E>E0PN0P0PN0PN0P 0>E>E0QN0QN0QN0Q0Q0QN0Q0Q 0>E>E0"UN0"UN0"UN0"U0"UN0"U0"UN0"U0"UN0"U0"UN0"UN0"U0"UN0"UN0"U 0>E>E0Z0ZN0ZN0Z0ZN0ZN0ZN0ZN0ZN0ZN0Z0Z0ZN0ZN0ZN0Z  00m`N0m`0m`N0m`0m`0m`0m`0m`0m`0m`0m`0m`0m`0m`0m`0m`0m`0m` 0m`m`0Hj0HjN0HjN0HjN0Hj0HjN0HjN0HjN0Hj0HjN0HjN0HjN0HjN0HjN0Hj 0m`m`0r0rN0rN0r0rN0rN0r0rN0rN0rN0r 0m`m`0 yN0 yN0 y0 y 0m`m`0{N0{N0{N0{N0{N0{N0{N0{N0{N0{N0{N0{N0{N0{N0{0{0{0{0{  00I00 00000* 00a* 00} 00hN0hN0h0h0h0h0h0h0h*0h0N0N0N0N0N0N0N0N0N0N000N0N0N0N0N00N0N0N0N0N0N0N0N0N0N0N0N0N00  0000000 0000"0" 00000< 0< 0000000& 0& 00* 00F0FN0FN0FN0FN0FN0FN0FN0FN0FN0FN0FN0FN0FN0FN0FN0FN0FN0F0FN0FN0FN0FN0FN0FN0FN0FN0FN0FN0F0FN0FN0FN0FN0FN0FN0FN0F* 00P0PN0PN0PN0PN0PN0PN0P0PN0PN0PN0P0PN0PN0PN0P0PN0PN0PN0PN0PN0PN0PN0PN0PN0P0PN0PN0PN0PN0PN0PN0PN0P0P0P0P0P0P0P  00J0000000 0 0 0 0 0 0 0 0 0 0 0  0  0  0  0  0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0  0! 0" 0#0Vg0z00 0az00l@0:00lxh@0:00lh@0:00lh@0:00l i@0:0 0lLk:0 0lTm@0:00lm@0::00lj@0::00l k@0:00ln@0:00l4o@0:00l@0 c:00l,@R> c @0>0 ...1\ 4 w & #(&.)V,.3w58U=@*AAwBCCE$FFxG0HHJzLDNOPTUVXZ[]_Na|bXc4dknoGqSrXsvNy{p}ge"vMpmE08)C7bj7op)G, ../0{~      ?HTiaq{kʪD=ob..4/0e00| !"0}\u{06 9RWXsy9?Fagr*EK r7:25i &'@FfU)k)t))))484=4555???$G=GBGTU Ud.d4de'e0eBn[nanÂ܂<U["()RXYԅڅkȊΊ.7c|uҖԖѡĦ}nBXad}#)D]cE^d+1Jchi  _ _ _  ')1!!!k  O2$QLa,ܿKG7F2$D%2_2$ip`bc2$$,|9\"53o  4     A5% 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E|| "0e@     @ABC DEEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN E5%  N E5%  N F   5%    !"?N@ABC DEFFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `ab@82Vp.(    %(/ 3  s"*?`  c $X99? %(/ZB  S D#m#Z s t'?'  s t'?'`"  C (s t'?' (z"  c $"`""$# z"  c $"`+!C# z"  c $"`"_%&& z"  c $"` #!_% z"  c $"`f%'!&" z"  c $"`+_%& N  3 W##$_%N  3 I!_%"%N  3 " $N B 3 $ &N  3 $!f%C#Z  s ^&   s ^&`"  C   s ^&  z"  c $ "`##%&  z"  c $ "`d #G3$  z"  c $ "`#@o$  z"  c $"` OS" z"  c $"`Oo$% N  3 G##N B 3 o$%N  3 !#N  3 @#O#%`"  C (9 w. z"  c $"`,u. z"  c $"`++, z"  c $"`+,- N  3 ++Q-f B s *ZGJHIJU3$+f  s *ZG"HbI"&$K-Tb  C GHm(Hb  # +s Hb  # Os `"  C : z"  c $"`>*,   NG7HdI7?"0@NNN?NL+>, B 6?"0@NNN?NuK-+Q-  HG{/H0SI{/?"0@NNN?NL+,$  $%(6 \3  s"*?` ] c $X99? $%(6DT" ^ # ^d %u'*D T" _ # _.X#60D T" ` # `'&)D T" a # a')D ZB b S Ds.)/)DT" c # c3X#5D ZB d S Dm.)/)DT2 e # e^*.D T2 f # f^603D h g 3 g"`J+:f-D h h 3 h"`0"3D D  '& n#  s"*?t m s *X99?"` '&)" s  f s Ԕ,k8c? "6@`NNN?NwB#)  " p  fp Ԕ,k8c? "6@`NNN?N z) B r <D?"0@NNN?N)" t  ft Ԕ,k8c?"6@`NNN?NK ) B u <D?"0@NNN?N\~)" v  f!v Ԕ,k8c?"6@`NNN?N ) !" w  fw Ԕ,k8c? "6@`NNN?N"!D%) " x  f"x Ԕ,k8c?"6@`NNN?N") "" y  f#y Ԕ,k8c?"6@`NNN?ND 5!|) #" z  f$z Ԕ,k8c?"6@`NNN?Nj"#) $" {  f%{ Ԕ,k8c?"6@`NNN?N"w#) %" |  f&| Ԕ,k8c?"6@`NNN?N#5$) &" }  f'} Ԕ,k8c?"6@`NNN?NP$%) ' B TZG?;HWI?;?"0@NNN?N$) B TZGHI?"0@NNN?Nje#)  <?"0@NNN?N+#e#) B <?"0@NNN?N#$)  <?"0@NNN?Nw+#A$)"  NZHI6?"0@NNN?NbR#)  NGfHBIf?"0@NNN?N5|!A$)b  s *? "0@NNN?Nj'b  s *? "0@NNN?N_`'b  6G0H? "0@NNN?Na!'" o  f o Ԕ,k8c? "6@`NNN?NU)  < 3 # A=< j # A8b  C )"` )\  3 *"` *B S  ?o-v}/xz1z{3{}5{|7t|;|yWXYZ[\]^_`abcde f!fW8j t380t8(4j4n=t \t tT _Ref8549970 _Ref513720338 _Hlt513720352 _Hlt9853522 _Ref8547871 _Ref9070395 _Ref9855617 _Ref9853040 _Ref9853287 _Ref520622409 _Toc527515133 _Ref520803553 _Toc527515134 _Ref520803555 _Toc527515135 _Toc527515136 _Ref8547716 _Ref8926860 _Ref8547211 _Ref512138262 _Ref9675553 _Ref9853477 _Ref8721799 _Ref9862006 _Ref9611724 _Ref8441174 _Ref526061256 _Ref9560551 _Ref9564451 _Ref526066737 _Ref9071428 _Ref526066744 _Ref9071433 _Ref534780974 _Ref5622720 _Ref526065198 _Ref526062086 _Ref8545287 _Ref515906955 _Ref525985481 _Ref521123461 _Ref6385536 _Ref9399949 _Ref525673966 _Ref535385772 _Ref9559788 _Ref6385476 _Ref6383438 _Ref6382768 _Ref534185810 _Ref9563257 _Ref509221367 _Ref535815723 _Ref9825688 _Ref535816125 _Ref9759101 _Ref238236 _Ref9071361 _Ref9852754 _Ref535808524 _Ref525982392 _Ref9862233 _Ref526024298 _Ref9862423 _Ref515900185 _Ref525981826 _Ref9862309 _Ref526062066 _Ref521123421 _Ref8693253 _Ref9565950 _Hlt513366458 _Hlt8723880 _Ref7317334 _Ref9860172 _Ref8093336 _Ref9860197 _Ref8693138 _Ref9690428 _Ref8722162 _Ref9564844 _Hlt513720164 _Ref9859595 _Ref9860694..)*E[`7j7jlklkxx{{{{:).@AYZT0 !klef<Xlm([@@  !"#%$&'()*+,-./0213456789:;<=>?@ABCDGHE@F@IJKLMNOPQ@RS)\9\9NEw`?j?jrryy{tՖNN@@YY1sS/ 3!0kee<<YllI|: }Y }Z }DZ }V}d}<$}dȫ}a}T}}V}}}}} }L}}$«}d«}} }$!}k"} l#}Ll$}l%}l&}TN'}N(}N)}O*}TO+}J,},K-}lK.}K/}F0}$G1}dG2}G3}G4},C5}lC6}C7}C8},D9}?:}?;}@<}D@=}@>},<?}l<@}<A}<B}\8C}8..7#$/E/E8E..722;i{{yy99 DDg//:      !"#$%&(')*+,-./01235468796<<#$7E=E=E 6<<:@@l""|?? KKu8AA   !"#$%&(')*+,-./0123546879 B+*urn:schemas-microsoft-com:office:smarttagscountry-region96*urn:schemas-microsoft-com:office:smarttagsState=2*urn:schemas-microsoft-com:office:smarttags PlaceType=3*urn:schemas-microsoft-com:office:smarttags PlaceName87*urn:schemas-microsoft-com:office:smarttagsCity8*urn:schemas-microsoft-com:office:smarttagsdate98*urn:schemas-microsoft-com:office:smarttagsplace;:*urn:schemas-microsoft-com:office:smarttagsaddress:9*urn:schemas-microsoft-com:office:smarttagsStreet>5*urn:schemas-microsoft-com:office:smarttags PostalCode 1520013DayMonthYear:98765832888328+8+8+832832887687+8868683287878878787+832%,\|}79=>@9z{}~:@Fhilmqr*LNRSa r ;=?@H68=>@iGJOPTf !&&&&''?'A'''D(F(|(~(U)r)s)u)w)z) * ***********i+l+++++L,N,e,h,,,--(-*-;-=-114>4A4G44455555555 88????@@4B'A'''@(C())))* *++C,E,V,[,--c-e-y-~-2.4.Q.V...B0[000111122333@44444J5)6q7w77785888 ====>>?@@@VBXByBBFDGHHcMeMtPyPSSTUWWT]Y]^^c7deremdnoo8pEpIuNuxx{{r||݅<Y%ɓ=֖ז^_'ΜҜO"ǦRS fpn&,HcxLEe"eiZ 4%'ov=lC(/IJKY[b|}~33333333333333333333333333333333333333333333333333333333333333333333333333338M E-\);g*.FHU1&&))))%+8+113?4J5)6*6@6"939?@@FDGIIiM{MPPQQTU.UZZP`x`c6deqe7jNjpprrx y{{|2}?{]^܅<XYiu`v%ȓ=ז)O"Ʀ!B[Ѹ+U1_n&,HbxLDefg"#.Zg't j14Vl C $&(*,.=?F}  !#&(/IY[b|~ Dana Kaiser Dana Kaiser Dana Kaiser Dana Kaiser Dana Kaiser Dana Kaiser Uwe Glsser margus veanes Yuri Gurevichjennir;|c}ώ~D$."\!xFD,[t'h2 Y<4#S aG Kj345`9 j}tS 8(8N 5lRs `M)jⲽx8{!6mH%x>'xB&1j}(d(p+Z̿n,~J<&C- N@.sr/BM)-31Ɗ&\6o6A'[8ln%9&wv ;U> (1~JDJU,,sEh(E ae?E $zI2!xO=/QԐR^7@R$")"`Tܒ*:V}MUwnZ$S[D>h]rEހ,bPb&o"HMj\J+lr~lq~M/,t9_ue Dvj}:3w}?x, px%  ^`.^`.88^8`.^`. ^`OJQJo( ^`OJQJo( 88^8`OJQJo( ^`OJQJo(hh^h`.^`6OJPJQJ^Jo(l^`OJQJ^Jo(hHopp^p`OJQJo(hH@ @ ^@ `OJQJo(hH^`OJQJ^Jo(hHo^`OJQJo(hH^`OJQJo(hH^`OJQJ^Jo(hHoPP^P`OJQJo(hHhhh^h`OJQJo(hHoh88^8`OJQJ^Jo(hHoh^`OJQJo(hHh  ^ `OJQJo(hHh  ^ `OJQJ^Jo(hHohxx^x`OJQJo(hHhHH^H`OJQJo(hHh^`OJQJ^Jo(hHoh^`OJQJo(hH P ^`P Appendix : @@^@`.08^`0..``^``... ^` .... ^` ..... ^` ...... `^``....... 00^0`........h ^`o(hH[]h ^`hH.h pLp^p`LhH.h @ @ ^@ `hH.h ^`hH.h L^`LhH.h ^`hH.h ^`hH.h PLP^P`LhH.h ^`o(hH[] ^`hH. pLp^p`LhH. @ @ ^@ `hH. ^`hH. L^`LhH. ^`hH. ^`hH. PLP^P`LhH.hh^h`. ^`hH. pLp^p`LhH. @ @ ^@ `hH. ^`hH. L^`LhH. ^`hH. ^`hH. PLP^P`LhH.h hh^h`OJQJo(h 88^8`OJQJo(oh ^`OJQJo(h   ^ `OJQJo(h   ^ `OJQJo(oh xx^x`OJQJo(h HH^H`OJQJo(h ^`OJQJo(oh ^`OJQJo(hhh^h`OJQJo(hHh88^8`OJQJ^Jo(hHoh^`OJQJo(hHh  ^ `OJQJo(hHh  ^ `OJQJ^Jo(hHohxx^x`OJQJo(hHhHH^H`OJQJo(hHh^`OJQJ^Jo(hHoh^`OJQJo(hH^`o(() ee^e`hH. 5L5^5`LhH.   ^ `hH.   ^ `hH. L^`LhH. uu^u`hH. EE^E`hH. L^`LhH.h ^`o(hH[] ^`hH. pLp^p`LhH. @ @ ^@ `hH. ^`hH. L^`LhH. ^`hH. ^`hH. PLP^P`LhH. hh^h`OJQJo( W^`WOJQJo(lpp^p`OJQJo(hH^`OJQJ^Jo(hHopp^p`OJQJo(hH@ @ ^@ `OJQJo(hH^`OJQJ^Jo(hHo^`OJQJo(hH^`OJQJo(hH^`OJQJ^Jo(hHoPP^P`OJQJo(hHh88^8`OJQJo(hHh^`OJQJ^Jo(hHoh  ^ `OJQJo(hHh  ^ `OJQJo(hHhxx^x`OJQJ^Jo(hHohHH^H`OJQJo(hHh^`OJQJo(hHh^`OJQJ^Jo(hHoh^`OJQJo(hH hh^h`OJQJo(hhh^h`OJQJo(hHh88^8`OJQJ^Jo(hHoh^`OJQJo(hHh  ^ `OJQJo(hHh  ^ `OJQJ^Jo(hHohxx^x`OJQJo(hHhHH^H`OJQJo(hHh^`OJQJ^Jo(hHoh^`OJQJo(hHh ^`o(hH[]h ^`hH.h L^`LhH.h pp^p`hH.h @ @ ^@ `hH.h L^`LhH.h ^`hH.h ^`hH.h L^`LhH.h ^`OJQJo(h ^`OJQJo(oh pp^p`OJQJo(h @ @ ^@ `OJQJo(h ^`OJQJo(oh ^`OJQJo(h ^`OJQJo(h ^`OJQJo(oh PP^P`OJQJo(h ^`hH.h ^`hH.h pLp^p`LhH.h @ @ ^@ `hH.h ^`hH.h L^`LhH.h ^`hH.h ^`hH.h PLP^P`LhH. hh^h`OJQJo( ^`OJQJo(o pp^p`OJQJo( @ @ ^@ `OJQJo( ^`OJQJo(o ^`OJQJo( ^`OJQJo( ^`OJQJo(o PP^P`OJQJo(h ^`OJQJo(h ^`OJQJo(oh pp^p`OJQJo(h @ @ ^@ `OJQJo(h ^`OJQJo(oh ^`OJQJo(h ^`OJQJo(h ^`OJQJo(oh PP^P`OJQJo( hh^h`OJQJo( hh^h`OJQJo(hhh^h`OJQJo(hHh88^8`OJQJ^Jo(hHoh^`OJQJo(hHh  ^ `OJQJo(hHh  ^ `OJQJ^Jo(hHohxx^x`OJQJo(hHhHH^H`OJQJo(hHh^`OJQJ^Jo(hHoh^`OJQJo(hHhh^h`. ^`hH. pLp^p`LhH. @ @ ^@ `hH. ^`hH. L^`LhH. ^`hH. ^`hH. PLP^P`LhH.SVS^S`Vo(.P8^`P56 Figure : @@^@`.0^`0..``^``... ^` .... ^` ..... ^` ...... `^``....... 00^0`........h^`OJQJo(hHh^`OJQJ^Jo(hHohpp^p`OJQJo(hHh@ @ ^@ `OJQJo(hHh^`OJQJ^Jo(hHoh^`OJQJo(hHh^`OJQJo(hHh^`OJQJ^Jo(hHohPP^P`OJQJo(hHhhh^h`OJQJo(hHoh88^8`OJQJ^Jo(hHoh^`OJQJo(hHh  ^ `OJQJo(hHh  ^ `OJQJ^Jo(hHohxx^x`OJQJo(hHhHH^H`OJQJo(hHh^`OJQJ^Jo(hHoh^`OJQJo(hH^`OJPJQJ^Jo(s^`OJQJ^Jo(hHopp^p`OJQJo(hH@ @ ^@ `OJQJo(hH^`OJQJ^Jo(hHo^`OJQJo(hH^`OJQJo(hH^`OJQJ^Jo(hHoPP^P`OJQJo(hHhh^h`6.^`5o(.0^`05o(..0^`05o(... 88^8`5o( .... 88^8`5o( ..... `^``5o( ...... `^``5o(....... ^`5o(........h ^`hH.h ^`hH.h pLp^p`LhH.h @ @ ^@ `hH.h ^`hH.h L^`LhH.h ^`hH.h ^`hH.h PLP^P`LhH.h ^`OJQJo(h ^`OJQJo(oh pp^p`OJQJo(h @ @ ^@ `OJQJo(h ^`OJQJo(oh ^`OJQJo(h ^`OJQJo(h ^`OJQJo(oh PP^P`OJQJo(8^`56NOTE  h^h`o( NOTE  h ^`hH.h ^`hH.h pLp^p`LhH.h @ @ ^@ `hH.h ^`hH.h L^`LhH.h ^`hH.h ^`hH.h PLP^P`LhH.h^`OJQJo(hHh ^`hH.h pLp^p`LhH.h @ @ ^@ `hH.h ^`hH.h L^`LhH.h ^`hH.h ^`hH.h PLP^P`LhH.h^`.h ^`hH.h L^`LhH.h r r ^r `hH.h BB^B`hH.h L^`LhH.h ^`hH.h ^`hH.h L^`LhH.h^`.^`o(.hpLp^p`L.h@ @ ^@ `.h^`.hL^`L.h^`.h^`.hPLP^P`L.hhh^h`OJQJo(hHh88^8`OJQJ^Jo(hHoh^`OJQJo(hHh  ^ `OJQJo(hHh  ^ `OJQJ^Jo(hHohxx^x`OJQJo(hHhHH^H`OJQJo(hHh^`OJQJ^Jo(hHoh^`OJQJo(hHh ^`56CJo([]h ^`OJQJo(hpLp^p`L.h@ @ ^@ `.h^`.hL^`L.h^`.h^`.hPLP^P`L.P^`P56OJQJo( h^`OJQJo(hHh^`OJQJ^Jo(hHohpp^p`OJQJo(hHh@ @ ^@ `OJQJo(hHh^`OJQJ^Jo(hHoh^`OJQJo(hHh^`OJQJo(hHh^`OJQJ^Jo(hHohPP^P`OJQJo(hH hh^h`OJQJo(h ^`o(hH[]h ^`hH.h pLp^p`LhH.h @ @ ^@ `hH.h ^`hH.h L^`LhH.h ^`hH.h ^`hH.h PLP^P`LhH.^`OJPJQJ^J) ^`hH. pLp^p`LhH. @ @ ^@ `hH. ^`hH. L^`LhH. ^`hH. ^`hH. PLP^P`LhH.h ^`o(hH[]h ^`hH.h pLp^p`LhH.h @ @ ^@ `hH.h ^`hH.h L^`LhH.h ^`hH.h ^`hH.h PLP^P`LhH. hh^h`OJQJo(h ^`OJQJo(h ^`OJQJo(oh pp^p`OJQJo(h @ @ ^@ `OJQJo(h ^`OJQJo(oh ^`OJQJo(h ^`OJQJo(h ^`OJQJo(oh PP^P`OJQJo(P^`P@@^@`.0^`0..``^``... ^` .... ^` ..... ^` ...... `^``....... 00^0`........<px:3w{!A'[8UwnZ(}?xG &\6U>6mH%HMj^7@R"`T1~JD~llsr/S[M)4#SEs 0ln%90p+0n,Dv!xO`9 x$zI<&C-bp b(8 ;h]_u~j}(l,b}|/QxB&,ttS :V)-3N@. Ye?EsEPRbS8FT)#0VXb>>nR                                Z        _                         _                                           װ:                         ~&                 (8         *|       #G        xv~                 _        \`        _         @ @ @@DS-t)Jo|m\/ 4GJo|y\XJo|Jo|-tKdd Jt N9=VAW[s[cej!K#s(eQ8S "q*2ERLYH[ D(0?&K MV\`(&*2:FYOi]O_yx  4'*Zqewh;5DF`abqvv} -*yDWceq{!"8EHUp 3! 6 K M S 2S c l o  ' 8 "g m r ] 8  6 D #Q c =d In y z , 2 ?C C 5o     *" 7 k "Q+/5>E$K RVeXg`&(():HIb1nn{uk =WcZjjknq %,u4V[%&9-6NOZ[ypqs'j't'|'((2&(D6(:C(P(T(D_(e(zx(*~(). ) )2)L<)F)o[)i)* ****U**Y*Z*^+&+*+,+j2+"Y+[+[+u,S,",$,%,,M, O,7R,vz,},,0-5F-O-TW-Xm-..*+.?.?..D.2f.n.t.v.//3Q34}4&4y:4]K4W4[4m4x4&555!5:&5O5t5~5~56!6$646:6Y6Ou6 |6 7F77#7?7O7s76~7888J88"8778J>8B8(M8h8o8t8x8}9 9!94969 Q9:Q9n^9ac9,:I:WT:]v:i; ;P;y; ;*;1;>#>I$>*>->m/>M>Q>g>u> ??m?*?nF?]?h?@:@@ @S<@M@e@v@ ~@ A9,A6ALARMAPAWA-`AfAvyA{A~AzB7Bg*B.BSFBkB-pB{BC C CC!C>C8ICOC}~CCD\3D6Dh8Dt;DWSD|SDUD~uDEEg E1 EEEE)Ei.EyEF8FF F}KFRFGG!G,G/WG1WG^G H HHHHUH H$Hs+H4HIHVH'rH}HI=1IWIZIeIrvIJJ>J?JEJLJk`J`wJKKK(KNK^KPbK L0Lk>L)HLNLVL3[L;[L|LMk5MMLSM,aM-xMl|M NNN1N(?NAN.BN+ZNZN/gNrNtNwNxOOO&O7OfPOgXO\O+P<P"6PlLPZ\PgPzP-QG3Q7Q FQ_SQZQ~Q R R7R;RVSRURI S=0S6S&7SNS/bSfSmS{S9}S TTT",T?-T>TAT?FTVTdTgT nTArTjUUU7U7UnUvU=~U VV$V2V4Vg8V_>V@BVVJVKVLVQVRVXVUYVcVQWcW=W>WDWeUW@WWZWhWX"X_(X,X0X6XCXFX[IX)`X3cX YY'Y)Y -YHPYYYlYpYZB]Z-jZzrZ@zZe{Z [X([W+[8[#D[=M[p[Ap[P|[B\\5\#\(\=\\U\cr\|]z#]&]n)]8Y]h]K ^ ^v^?^3.^@^G^^^l^n^z^z^ _vC_;D_cscCcw3cDcEc,Rcd d6dz8d;dW?d`dUedBndudee+-e2e?eDeae fff)fYLf]f^fefjifqfgg0g3g7g?gk@g/GgMgRngh,hOhxZhM|hi iiL'i.i@iEiFiFMi^icijgimi}i2jijjj"Wj lj kMkfk$k8kFk\kekpukHk<l.l/l9l;l)=lGlVl`l*vlm67m%oOoYonoppp!pU2p;pCpNpRpWpzgpqhq!q(8qKqnXqgqlqbrrir r5rU:r^?rFrTrurovrvr~r9!sq)s-0sesgswstR tntGtLt^tbbtztulu^u2u2uCuEuFuNOu)dulunuuuzuv!v,1vSvHjvkvkv|v+w-w.CwDwVYwdbw+gwiwVxxt2x7xQAxOxXx\xcxTdx5mxoxyyyy7$yYydy~yzb$z-z5z![zgzQnz{{?{F{| |8*|O@|q| w|{|}l0}XO}Z}2e}~~'~@~3%~-~;~M~[N~2R~\~Ce~}l~]w~JPr[j" /g1BJT[^z_wA!$/6,mo@37jim{+[$'K7KoSY@mDS){,25Qbi&M@KBXP]#fqU q#8>?@UWP s-0{9 q /./3EF_b_jlzyA|Ro@&) 0J L%pu~! K  ,.R/2j8=bvmyN!F4IPpe!u*ww.E_RT rN.3<>GkNOw]_m ) <<<f&ouxd1 &AGRVoZ^`y04=ttL>?xN\z *qPtkr!0p_0fx +8rimivx>}$0&A)'@|JjUaeCs'W4;:L?=@FPMboqbf<6OOqYiZ]A5Ok{ *,ERVf.y-*vFHsQWc"K?X^3z\!(05i7e9NBCCRHP.Qv T%}%45C^w@"\EQW t~ e{Sdl] &"g=FTOO~)Pi\]^w}}:U2>BLbR;GHij|T7h8EGVS^ra cl?37(I=TqPttV%%11:OpXoD,.y0]27HO&UV]'i0XX^^czeu x: "#6Bq :fip' tyk&F0>w/B,CLQQWko,uJ&.:Zp\z*{ 1IN*j_z~ 7I9NCNZ\lq22r?M_p/{: 9KZehq2P7@UdY -$7Dzp-JVNn -9 ;a@CLE"O Sgwy6" p/#0_?}p*'rFWo6syK"!&O[Tibkmq#:pAmDLh."&$-37j:D@Re5$X?gG I,WEqfrsxx~B~%.\g ( 2bm}JOJrv*/0YT[4qwwI$6:t]_}bjm I b"9Gab6c^mwG~!hDJmJN\Emswy51'TV[$d6zu8:^MzPMUC]^(kmFp})2DdGO V{lZ"\&/X?BTLSATUpS0B9AxW_noms|*sC"Sik-$(ABipRtve|H %=K]~oppr Q ~(8K>[{7|g)/ 1MiYWni')05Nv| VC$$T1:XBsI0P [nQxL{}}}#Cl^/9zEtu *.|07FWOcY[cw*4-3@BFQPt/ 4j=>?l).C3`asyXz'+/8;_<K]PStjoIto.W2C8%?EUVkcE'1=KU6[ ctsv0zY + AZ at||%%[)#5a5JOnB7DkMJ`ajh{ ;;%o/2:Zamt} %m<~ $ (@cpp1-"_O___emyQCSTehi"`0>RT_m ?Ughkr{~@%.\J QuhU \#$D'.L~RTU __14:MErQxy Q#&dXg| , R)d;|E.bJeye6ilmnx=~2u!R?IGtx0HI JxMpf i/kzyY+qA0and.'33PI_^fkio @*?Gkp;F@?Pp X$*/27PY[lsy~7[]- #-1>Geiy|<e"k)1?KfQWchk$r-u+7ORaw~(M+!.K.6N W\c}[b(/7:3?+DxJT[Lhzq%, D;'>jmWrs~65fNfOhhoD66 /!COQjUChwt !I./|CCZb|yR188gqc&,Z@AEdG[zw -?!S[ZE0@d(vv   12949596?@FGUVde\n\o݂݃######[[~~~P@P P@PPPPP0@PPP PD@P$P&P(P*P,P.P`@P2Ph@P8Pt@PLP@PPPRP@P^P@PfP@PvP@PP@PP(@PPT@PP\@PPh@PP|@PP@PP@PP@PPP@PPP@PP@PPPP@PP@PP@UnknownG: Times New Roman5Symbol3& : ArialIArial Unicode MS;" Helvetica?5 z Courier NewG  MS Mincho-3 fg5& z!TahomaK@Palatino LinotypeA6 KaiTi_GB2312-SimSun[SO3Times71 CourierE5  Lucida Console7&  Verdana;Wingdings"1hte&6eefz<" w" w!. p4d 3qH(?S-_SDL Formal Semantics: Compiling and Running SDL Specifications on Abstract State Machine Models Uwe GlaesserjennirFZZZZ ecs-01-30###NTuDasm/KsEȉDMPIRECENT @ @ OL0OOWODOLBO@ @pLI,O;                           ! " # $ % & ' ( ) * + , - . / 0 1 2 3 4 5 6 7 8 9 : Oh+'0,8DT dp    `SDL Formal Semantics: Compiling and Running SDL Specifications on Abstract State Machine ModelsDL  Uwe Glaessermanwe we Normalejennire378Microsoft Word 10.0@hh@ @8@" ՜.+,D՜.+,P hp  0 Microsoftgw `SDL Formal Semantics: Compiling and Running SDL Specifications on Abstract State Machine Models TitlepH$D\d_AdHocReviewCycleID_EmailSubject _AuthorEmail_AuthorEmailDisplayName_PreviousAdHocReviewCycleID_ReviewingToolsShownOnce+#A new tech reportwngurevich@microsoft.comeYuri GurevichsoQuri  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>@ABCDEFGHIJKLMNOPQRSTUVWXZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRTUVWXYZ\]^_`abiRoot Entry F$kData ?31TableYaWordDocument)}SummaryInformation(SDocumentSummaryInformation8[CompObjj  FMicrosoft Word Document MSWordDocWord.Document.89q