A Language and Environment for Rigorous Modeling and Analysis of e-commerce Architectures

全文

(1)A Language and Environment for Rigorous Modeling and Analysis of e-commerce Architectures V. S. Alagar, V. Bhaskar, D. Muthiayen, O. Popistas, V. Srinivasan, Z. Xi. . Department of Computer Science Concordia University Montreal, Quebec H3G 1M8, Canada alagar,bhaskar,d muthi,popistas,sriniva,xi @cs.concordia.ca. Abstract The main issue in the development of agent-based architectures for e-commerce applications is to produce agents that collaborate with correct functional and temporal properties. They should be able to cope with large, complex, multi-lingual, and multi-platform systems. In order to achieve this potential, specific techniques for modeling, specification, analysis, and evolution of agent-based architectures must be provided. This paper advocates and presents one such approach.. 1 Introduction Internet offers a new way of marketing products and services that require distributed transactions to be carried out at prescribed times. Dependability and security are two major concerns for the developers and users of e-commerce systems. To deal with these concerns, it is crucial that e-commerce software be designed with a sound architecture. A good architecture simplifies the construction of large complex systems, and accomodates the design changes forced by a steady stream of new requirements. This paper describes a method, a language, a set of constructs, and tools that facilitate the design of architectures in e-commerce domain. More importantly, the presented approach enables rigorous validation and analysis of the design. Software architectures provide a high-level view of the system, enabling developers to abstract on the relevant issues and focus on the “big picture”. Most architectural descriptions for e-commerce applications are typically expressed only informally, in terms such as “client-server organization”, “layered systems”, “blackboard architecture” and in terms of box-and-line drawings showing the global organization of computational components and their interactions. More detailed descriptions of architectures are traditionally provided by Module Interconnection Languages (MILs) and Interface Definition Languages (IDLs). Informal descriptions are usually imprecise and incomplete. MIL and IDL descriptions focus on implementation relationships among parts of the system. Although such descriptions are essential, neither of them is suitable for analyzing the internal consistency, communication patterns, and the presence of the safety and security properties in an architecture. The distinction between abstract architectural descriptions and implementation-dependent descriptions, and the need to de-. scribe architectures at a level above their implementation details are clearly brought out in [4]. In this article we combine visual descriptions with rigorous notations. We use UML notational extensions as the visual architectural description language (VADL) to model ecommerce architectures. The developer uses only Rose [12] tools and a graphical user interface (GUI) [13] to model and analyze agent-based e-commerce applications. The graphical descriptions are mechanically translated into a formal architectural description language (FADL). The GUI provides the interface to compile the formal specification generated mechanically from UML diagrams, to validate, debug and reason about the architectural designs, and to verify safety and security properties. Basic Concepts Three distinct building blocks of a software architecture are components, connectors, and architectural configurations. For us, software components are agents, where an agent is an autonomous and encapsulated system that interacts with the environment. continuous basis. The following properties characterize agents: (1) an agent always reacts to a stimulus from its environment, which is a collection of agents; (2) an agent has sufficient computational power to process and respond to a stimulus so that the time elapsed between a stimulus and its response is acceptale to the relative dynamics of the environment; (3) an agent is encapsulated the internal state of an agent is not observable; and (4) an agent communicates with its environment through messages at its ports, where a port is an abstraction of an access point for a bidirectional communication between an agent and its environment. An agent type is a generic reactive agent (GRA). Instances of agents having different environmental interactions can be created from an agent type and used in different designs. A typical e-commerce application involves four agent types: client, merchant, transaction system, and payment gateway. The agents created from these agent types interact by exchanging events. The system of interacting agents is secure if every message is responded within the specified time bound. These properties should be verified at the architecture level, prior to implementation and deployment of the system on the internet..

(2) 2 A Theory of Agents An agent has a well-defined structure, interface, and behavior. Agents have no knowledge of other agents in their environment. Ports provide the only interface for an agent to communicate with its environment. An agent receives or delivers its messages at the ports attached to it. That is, agents do not communicate directly with other agents. Every message that occurs at a port is communicated along the connector that links that port to a compatible port, which is attached to another agent. It is the desiner’s responsibility to ensure that the configuration of agents are sound and complete.. Stimulus pid. Attributes Att. Func χ Φat. Port Condition ψport. Figure 1 shows the template (type) of a generic reactive agent (GRA). The filled arrows in the figure indicate flow of events. An input event is the result of an incoming interaction defined by the external stimulus, the current state of the agent, and the port constrained by the port-condition. Every event occurrence causes a state transition and may also involve a computation. A computation updates the agent’s state and attributes, shown by the arrow labeled with ‘Att.Func.’ The dotted arrow connecting the block of computation to that of time-constrained reaction signifies the enabling of a reaction due to a computation. Based on the clock, an outstanding reaction is fired by the agent, thereby generating either an internal event or an external event. All generated output events will result as a response at the port specified by the portcondition. A state update may also result in the disabling of an outstanding reaction.. Internal. Input. Output. Ε int. Events. Time-Constrained Reactions Υ. Ε in. Events. Events. Ε out. Disable. From Global clock. pid. Outgoing Interaction. Response. Figure 1: Anatomy of a Generic Reactive Agent The Formal Language (FADL) A formal definition of the different components of a reactive agent as described in Section 2 is given below. A full description of the grammar, the language semantics, and its expressive power in specifying real-ttime reactive systems have been discussed in [1, 2]. A reactive agent is an 8-tuple ( , , , , , , , ) such that:

(3). is a finite set of port-types with a finite set of ports associated with each port-type.

(4). is a finite set of events and includes the silent-event tick.

(5)

(6). is a finite set of typed attributes. The attributes can be of one of the following two types: i) an abstract data type ; ii) a port reference type.

(7). is a finite set of LSL traits introducing the abstract data types used in .

(8). is a function-vector where,. The significant features of the abstraction are the following: (1) A GRA can be specified individually. (2) The GRA specification is not biased towards any language or implementation. (3) Timing constraints are encapsulated, thereby precluding an input event from being a time constrained event. That is, an agent has no control over the times of occurrences of input events since they are under the control of the environment. (4) An agent has complete choice over selecting the port (and hence the external agent) to communicate. 3 The Language We use UML as the VADL for describing an architecture with reactive agents. The grammar for the FADL is based on a formal description of GRAs and subsystems.. States Θ. Transition Λ. Enable. An agent type is parameterized with port types and specifies the time-dependent functionalities of agents of the type. A port type defines the set of events that can be received at a port of that type. An agent may have several ports of a particular type. Port reference identifiers and abstract data types are the only data members for an agent. The behavior of an agent is captured by a hierarchical state machine with logical assertions on the transitions and time constraints. By preserving the interface (for external communication) and behavior (for internal consistency) of an agent, the agent becomes reusable in a black-box fashion in different designs.. Incoming Interaction. is a finite set of states. , is the initial state.. – "!$# associates with each state a set of states, possibly empty, called substates. A state is called atomic, if % &('*) ..

(9). +,!.- associates with each state a set – of attributes, possibly empty, called the active attribute set.. is a finite set of transition specifications including / /1032$0 . A transition specification 4 65 7 8 , is 2 EPGJIQSRTA a three-tuple : 9;:% <= .>@?BADCDFEHGJILK=BALENM 'HO where: /1032$0.

(10) – < = > U are the source and destination states of the transition; – event CVW labels the transition; EPGJILK= is an assertion on the attributes in and a reserved variable pid, which signifies the identifier of the port at which an interaction associated with the transition can occur. 2. – E M is the enabling condition and E GJILX is the 2 postcondition of the transition. E M is an assertion on the attributes in specifying the condition under which the transition is enabled. E GJIQ is an assertion on the attributes in , primed attributes in YBZ > and the variable pid and it implicitly specifies the data computation associated with the transition.

(11). is a finite set of time-constraints. A timing constraint 0 / 0 0 [ 0 \ is a tuple LC > J] ^=_1` where, / 0ba / is a transition specification. – ' 0h2 0 – C > c% ILdegf is the constrained event.. – ] ^==_1` defines the minimum and maximum response times. 0i. – is the set of states wherein the timing 0 constraint [ will be ignored. Figure 2 shows the template for agent specification in FADL. A subsystem architecture specification (SAS) is defined by composing reactive agents or by composing smaller subsystems. Figure 3 shows the template for a subsystem architecture specification: the include section lists subsystem architectures to be used in constructing the one under specification; the instantiate section lists agents with their attributes initialized and port-types instantiated with their cardinalities; the configure section specifies the connectors between agents. GenericAgent 9UjHkmlnCTRo] p1qrst5csXuepvC^ZwxJs` Events: States: Attributes: Traits: Attribute-Function: Transition-Specifications: Time-Constraints: end. Subsystem 9UjHkmlnCTR Include: Instantiate: Configure: end Figure 3: Template for System Architecture Specification.. assumed that the readers are familiar with UML and Rational Rose. Each subsection describes a component of the formal model introduced earlier. Generic Reactive Agent - A generic reactive agent is the basic abstract unit of a e-commerce system. UML provides an extension mechanism using stereotypes. We introduce generic reactive agents in Rose as classes with stereotype :=:FyTz|{|?=? . The class icon has three compartments in Rose: the name compartment, the attribute compartment and the operations compartment. The name compartment is mandatory, but the other two are optional. Relationship between a GRA and its Port Types - Following the same extension mechanism with stereotypes as for GRA, we introduce port types in Rose as classes with stereotype :L:%}TqrsX~up1C?L? . The name of the port type class must start with the symbol “@”. It has only one attribute, named events, of type Set, which is considered to be constant. The initial value of this attribute denotes the list of input (?) and output (!) events that can occur at a port of this type. We represent the relationship between a GRA and its port types as a binary association between the GRA symbol and the port type symbol in a class diagram (Figure 4). The association name is optional. The association end corresponding to the GRA must have the composition aggregation indicator, meaning that the GRA is a composite of port types. <<GRA>> GenericAgentName <<PortType>> attribute1 : PortTypeName1 <<DataType>> attribute2 : Set[int,IntSet]. <<PortType>> PortTypeAgentName2 events : Set = {Event3 , Event4!}. <<PortType>> PortTypeAgentName1 events : Set ={Event1!, Event2?}. Figure 4: UML Class Diagram with one GRA and its two port types. Figure 2: Template for Generic Agent Specification.. UML Notation (VADL) In this section we describe briefly how to model generic reactive agents and subsystem architectures in Rational Rose. A detailed discussion with examples appears in [11, 2]. It is. Events and States - All the events that may occur for a generic reactive agent (input, output and internal) and its states are modeled in Rose using the statechart diagram belonging to the GRA. In Rose, the triggering event is defined as the event that triggers a state transition. Graphically, the event name is represented as the label on the correspond-.

(12) ing state transition. Input and ouput events are also listed in the attribute section of the corresponding port type classes as described above. Only one start state can exist in each statechart diagram. When applying nested state, one start state should be defined in each context. A state may be nested to any depth level. We may define complex states for a GRA using Rose’s nested states concept. Typed Attributes - All typed attributes of a generic reactive agent are represented in Rose as attributes of the GRA. For generic reactive agents, attributes can be of two types:port types and data types. Port type attributes are represented in Rose as attributes with the :=:F}TqrsX~up1C?=? stereotype. The type expression must be the name of a port type class already defined in an aggregate association to the GRA. Data types such as set, queue, and relation are specified as Larch Shared Language traits [6]. Data type attributes are represented in Rose as attributes with the :=:Fkmskm~up1C?=? stereotype. Transition Specifications and Time Constraints - Transition specifications in the generic model have the following components: initial and final state, triggering event, portcondition, enabling-condition and post-condition. These components are modeled in Rose using the guard and action features of the statechart diagram. The guard condition of a transition has the form: port-condition && enabling-condition && timeconstaint condition. The action of a transition has the following format: Post-condition && Time-constraint-initialization. Event1[ port-condition && enabling-condition && time-constraint-condition ] / post-condition && TCvar1=0 state1. state2. Event2[ port-condition && time-condition && TCvar1<2 ] / post-condition. state3 entry: TCvar1=-1. Figure 5: Constrained Events in Statechart Diagram A time constraint in the generic agent model has the following components: constraining event, constrained event, lower and upper bounds and a set of disabling states. Time constraints will be introduced in Rose in the statechart diagram, as follows. For each time constraint, a reserved variable of type interger will be defined. This variable should be named TCVarN, where N is a numeral (for example TCvar1, TCvar2, etc.). This variable has to be initialized to 0 on the transition of the constraining event, as the second Action. On the transition corresponding to the constrained. event, the guard condition has to include the time-constraint condition, as a third predicate. Figure 5 shows part of a statechart diagram illustrating the transition specifications and time constraints. System Architecture Specifications - In Rose, we model a subsystem as a collarboration diagram. This collaboration diagram contains generic reactive agents instantiated with ports and port links for communication (Figure 6). The purpose of this collaboration diagram is to statically specify the architecture composed from agents, ports and port links. Therefore no messages should be shown on the links. port1 : PortType AgentName1. port3 : PortType AgentName3. obj1 : Generic AgentName. obj2 : Generic AgentName2. Figure 6: A Collaboration Diagram of an Architecture with two GRAs A reactive agent is defined in Rose as an instance of a generic reactive agent. A port is defined in Rose as an object of the class named with the port type name. We define a reserved variable pid as the identifier of the port at which an interaction associated with a transition can occur. This reserved variable can be used in the logical assertions in the portconditoins, enabling-conditions and post-conditions. An agent may have several ports of each port type defined for the class. This relationship is shown as a link between the agent and the port instances in the collaboration diagram of the subsystem. A link between two port objects belonging to two reactive agents defines a port link between the two objects. 4 The Environment This section describes the environment which supports the modeling, analysis, evolution, and implementation of ecommerce architectures based on reactive agents. The environment includes support tools for UML modeling and translation to the formal specification, an interpreter for syntactic and semantic checking, a validation assistant, a verification assistant, a browser, and a graphical user interface. Visual architectural models are created in Rational Rose [12]. The environment provides a link to Rational Rose, allowing the visual composition of reactive agents and subsystems in terms of UML classes, statecharts and collaboration diagrams. It also includes a translator [11] for generating formal specifications from the graphical descriptions. The browser [9] provides a navigational link to a library of components including data models, generic reactive agents,.

(13) and subsystem configuration specifications. These components, stored in a repository, are checked for syntactic correctness and internal consistency by the interpreter. Hence, they may be reused or adapted for use in different architectures. The interpreter [14, 13] performs lexical and semantic analysis on formal descriptions of agents and subsystems that are generated from the visual models. An internal representation of the architecture specification is used to instantiate reactive agents and perform validation and verification. The graphical user interface (GUI) [13] provides a comprehensive interfacing facility to the different tools in the environment. The interpreter, simulator, and verification assistants can be invoked through GUI. The simulator [8] is the central piece of the validation assistant and it simulates computational steps of agents in the architecture based on the operational semantics of reactive agents. The simulation process is useful for validating agent performance, system properties, functional requirements and timing constraints, debugging system designs, incremental development of systems, and for providing a level of assurance that security and safety properties are not violated. During the simultation process, the clock can be frozen before handling the next event from the event-list. The state of the system at this point and the histories accumulated during the simulation of computational steps up to this point can be inspected, and analyzed to determine the causes of the current system status. The verification assistant [10] generates a set of axioms from the abstract syntax tree description of the modeled architecture created by the interpreter. The goal is to use them in formally verifying security and safety properties in the system. For some applications, this set of axioms may have to be supplemented with additional axioms. 5. Developing an e-Commerce Application - An Example We consider a generic e-commerce system consisting of five components, Client, Internet, Merchant, Bank, and Data WareHouse. Many specific applications can be conceived based on the high-level architecture shown in Figure 7. We assume the following pattern of event-driven transactions in this model:. form. Once the client is satisfied with the order form, the client provides the credit card information and requests for the invoice. The internet in turn requests the merchant to give the invoice. The merchant gives the client information to the bank in order to check the validity of the client information. The data warehouse is the repository of data from which the merchant, bank and client retrieve information in a secure manner. That is, at any instant the data revealed by the warehouse is completely dependent on the port at which a message is received. Since messages determine the port-types and these are determined at the architectural level, from the formal specifications we can verify the security of message communication and hence ensure the privacy of transactions. Moreover, at the expense of increased message traffic we reduce the amount of data transfer between the agents. A complete architectural design with Rose models and formal specifications are given in [3]. In this section we present only partial views and specifications of the architecture. Client. Bank. DataWareHouse. Merchant. Internet. Figure 7: Generic e-commerce Architecture <<GRC>> Client. <<GRC>> FinanceNetwork. (from Client). (from FinancialNetwork). <<PortType>> @D3. <<PortType>> @D1 <<PortType>> @I. (from FinancialNetwork). (from Client). <<PortType>> @R. (from Client). <<PortType>> @N. (from FinancialNetwork). (from DataWareHouse). <<PortType>> @C. <<PortType>> @L. <<PortType>> @F. (from DataWareHouse). (from Merchant). (from Internet). The client provides the address for the webpage to the internet, which in turn contacts the respective merchant, receives a confirmation from the merchant and gives the message that the webpage is available for the client to view. The merchant informs the data warehouse to make available the catalogue to the client. The client can then select items and the required quantity from the webpage. After the selection of items, when the client is ready to make the purchase the client can request for the order form through the internet. The internet in turn requests the merchant for the order. <<GRC>> Internet (from Internet). <<GRC>> DataWareHouse. <<PortType>> @E. (from DataWareHouse). (from DataWareHouse). <<PortType>> @D2 (from Merchant). <<GRC>> Merchant (from Merchant). <<PortType>> @M. <<PortType>> @T. (from Internet). (from Merchant). Figure 8: Main Class Diagram Visual Models - VADL Descriptions From the architecture shown in Figure 7 we determine the port types for each agent. From the description of the model we extract the messages for communication, and partition the messages according to the port-types. For instance, the.

(14) bank requires two port typess: one for communication with the merchant agent and the other for communication with the data warehouse. In our model the financial network consists of a gateway which regulates a secure communication between the bank and merchant and between the bank and data warehouse. The event names and the port types associated with them are shown in Table 1. Following the method outlined in Section 3.2, we construct the UML class diagrams for the agents. The main class diagram for the full architecture is shown in Figure 8. The class diagram for the bank shown in Figure 9 describes the events that can occur at its port types, and the abstract data type Queue included in it. The queue data structure is necessary to enqueue the merchant requests received at the bank and service them on a first-in-first-out basis. <<PortType>> @R events : set = {Check_Info?, Confirmation!, Rejected!}. <<GRC>> FinanceNetwork <<DataType>> merq : Queue[@R,MQueue]. <<PortType>> @D3 events : set = {Check!, Valid?, NotValid? }. Figure 9: Class diagram for Bank The dynamic behavior of the bank agent is captured in the statechart diagram shown in Figure 10. The agent is in idle state when there is no request to process. In the state contacting the agent has received a request to process a transaction. In the sate waiting, a request is being processed. In the state validating, the transaction has a valid credit card number. In the state invalid, the transaction has an invalid card number. In every state except idle, the agent enqueues requests received. In the state waiting, the request at the front of the queue is deleted. The events Confirmation and rejected are time constrained events in the sense that within the time interval [3, 10] from the instant the event Check occurred, either the transaction must be confirmed or rejected. Figure 11 shows the architecture of an e-commerce subsystem with six clients, one internet, two merchants, two data warehouses, and three banks. The agents are linked through connectors at their respective compatible ports for communication. For instance, the port @ 1 of client is linked to the port @ of the internet 1 . That link is not shared by any other agent. Consequently, the architecture specification ensures secure communication. Formal Specifications - FADL Descriptions The Rose-GRA translator [11] translates the visual models. Port @R - Merchant Agent Events Check Info? (idle contacting) Check Info? (invalid form invalid form ) Check Info? waiting waiting Check Info? (validating validating) Check Info? (contacting contacting) Confirmation! (validating idle) Confirmation! (validating contacting) Rejected! (invalid form idle) Rejected! (invalid form contacting) Port @D3 - DataWareHouse Events Check! (contacting waiting) Valid? (waiting validating NotValid? (waiting invalid form). Meaning to validate card same as above same as above same as above same as above confirm card same as above reject card same as above. Meaning request to validate receive confirmation receive rejection. Table 1: Financial Network Events.

(15) Check_Info / merq’ = insert(pid,merq). @L1 : @L. idle entry: TCvar1 = -1 entry: TCvar2 = -1 entry: TCvar3 = -1 entry: TCvar4 = -1. Rejected[ isEmpty(merq) && true && TCvar2 <= 10 & TCvar2 >= 3 ]. @L3 : @L. invalid_form. Check_Info / merq’ = insert(pid, merq) Check_Info / merq’ = insert(pid,merq). Confirmation[ is Empty(merq) && true && TCvar1 <= 10 & TCvar1 >= 3 ]. contacting entry: TCvar1 = -1 entry: TCvar2 = -1 entry: TCvar3 = -1 entry: TCvar4 = -1. Confirmation[ !(isEmpty(merq)) && true && TCvar3 <= 10 & TCvar3 >= 3 ]. validating. @D12 : @D1. @D11 : @D1. Rejected[ !(isEmpty(merq)) && true && TCvar4 <= 10 & TCvar4 >= 3 ]. @L5 : @L. @L2 : @L. @D13 : @D1. @D14 : @D1. @L6 : @L. @L4 : @L. @D15 : @D1. @D16 : @D1. C1 : Client. C2 : Client. C3 : Client. @I1 : @I. @I2 : @I. @I3 : @I. @C1 : @C. @C2 : @C. @C3 : @C. I1 : Internet. NotValid. Check[ len(merq) > 0 && true && true ] / merq’ = tail(merq) && TCvar1 = 0 & TCvar2 = 0 & TCvar3 = 0 & TCvar4 = 0. @M1 : @M. @M2 : @M. @T1 : @T. @T2 : @T. M2 : Merchant. M1 : Merchant @D21 : @D2. @D22 : @D2. @E1 : @E. @E2 : @E. D1 : Data WareHouse. D2 : Data WareHouse. Check_Info / merq’ = insert(pid,merq). waiting Valid. Check_Info / merq’ = insert(pid,merq). Figure 10: State Chart diagram for the Bank. @N1 : @N. @N2 : @N. @N3 : @N. @D34 : @D3. @D31 : @D3. @D32 : @D3. F1 : Finance Network. into formal specifications in the syntax described in Section 2. The architecture of the translator is designed in such a way as to emphasize the information flow between the corresponding visual and formal components. The user invokes the translator from the Rose Graphical User Interface, which is linked to the GUI in the environment. The interpreter in the environment can be invoked from the GUI to type check the formal specifications. The architectural design is both incremental and iterative. If errors are found in a specification, Rose tool can be reentered to modify visual models, translate and the interpret them. GUI privides the necessary facilities for such design evolution. Figure 12 shows the formal specification generated by the translator for the e-commerce subsystem shown in Figure 11. The subsystem specification can be type checked and analyzed for semantic consistency. GUI provides facilities to invoke the simulator and view the simulated scenarios of the interpreted e-commerce system. Simulator results give insight into the temporal and functional behavior of the modeled system. 6 Conclusion Architecture-based software development offers great potentials for software reuse and software evolution. This paper has adapted a technique developed in [2] for real-time reactive systems to the context of e-commerce applications. Since agents in an e-commerce application are reactive and time-dependent the adaption looks appropriate. By improving the UML model and integrating it with formal notation, we have provided a two-tiered development technique that combines the advantages of visual modeling and. @R1 : @R. @F1 : @F. @D35 : @D3. @R3 : @R. @F5 : @F. @N5 : @N. @N6 : @N. @D33 : @D3. @D36 : @D3. F3 : Finance Network. F2 : Finance Network. @R2 : @R. @F3 : @F. @N4 : @N. @R4 : @R. @F2 : @F. @R5 : @R. @F4 : @F. @R6 : @R. @F6 : @F. Figure 11: Subsystem Architecture formal modeling. Application specialists use the widely accepted industrial standard Rose tool to create UML models. The Rose-GRA translator [11] translates them into formal specifications, that are rigorously analyzed by the tools in our environment. Thus, the architecture-based approach discussed in this paper has the great potetial for improving the quality of the resulting software through early analysis, validation, and verification. Agent specifications can be refined through the addition of states and events, strengthening of timing constraints, and adding new port types. Ensuring specific properties at the architecture level is of little value unless they are also ensured in the resulting implementation. We are currently working on these issues. In addition, we are working on code generation and test-case generation methods from the architectural specifications. REFERENCES [1] R. Achuthan. A Formal Model for Object-Oriented Development of Real-Time Reactive Systems. Ph.D. thesis, Concordia University, Montreal, Canada, October 1995. [2] V.S. Alagar and D. Muthiayen, A Formal Approach to UML Modeling of Complex Real-Time Reactive Systems, Submitted for publication, September 2000..

(16) [3] V.S. Alagar, V. Bhaskar and Z. Xi, Visual Modeling of eCommerce Architectures, Technical Report, Department of Computer Science, Concordia University, Montreal, Canada, August 1999. [4] R. Allen and D. Garlan, A Formal Basis for Architectural Connection, ACM Transactions on Software Engineering and Methodology, July 1997. [5] V. S. Alagar, D. Muthiayen, and R. Achuthan. Animating Real-Time Reactive Systems. In Proceedings of Second IEEE International Conference on Engineering of Complex Computer Systems, ICECCS’96, Montreal, Canada, October 1996. [6] J.V. Guttag and J.J. Horning. Larch: Languages and Tools for Formal Specifications. Springer-Verlag, 1993. [7] G. Haidar, Reasoning System for TROMLAB Environment, M.S. Thesis,(to be submitted in September 1999), Department of Computer Science, Concordia University. [8] D. Muthiayen. Animation and Formal Verification of RealTime Reactive Systems in an Object-Oriented Environment. Master’s thesis, Concordia University, Montreal, Canada, October 1996. [9] R. Nagarajan, VISTA: A Visual Interface for Software Reuse in TROMLAB Environment, 1999. M.S. Thesis, Department of Computer Science, Concordia University [10] F. Pompeo, A Verification Assistant for TROMLAB Environment, M.S. Thesis, (to be submitted in September), Department of Computer Science, Concordia University. [11] O. Popistas, Rose-GRC translator: Mapping UML visual models onto formal specifications, M.S. Thesis, Department of Computer Science, Concordia University, 1999. [12] Rational Software Corporation, UML Notation Guide, Version 1.1, September 1997. [13] V. VangalurSrinivasan An Integrated Visual Interface for the Evolutionary Development of Reactive Systems in TROMLAB Environment, M.S. Thesis (to be submitted in September 1999), Department of Computer Science, Concordia University. [14] H. Tao. Static Analyzer: A Design Tool for TROM. Master’s thesis, Concordia University, Montreal, Canada, August 1996.. SCS ECommerce Includes: Instantiate: F1::FinanceNetwork[@R:2, @D3:2]; F2::FinanceNetwork[@R:2, @D3:2]; F3::FinanceNetwork[@R:2, @D3:2]; D1::DataWareHouse[@E:1, @N:3, @L:3]; D2::DataWareHouse[@E:1, @N:3, @L:3]; M1::Merchant[@T:1, @F:3, @D2:1]; M2::Merchant[@T:1, @F:3, @D2:1]; I1::Internet[@C:3, @M:2]; C1::Client[@I:1, @D1:2]; C2::Client[@I:1, @D1:2]; C3::Client[@I:1, @D1:2]; Configure: F1.@D31:@D3 D1.@N1:@N; F2.@D32:@D3 D1.@N2:@N; F3.@D33:@D3 D1.@N3:@N; D2.@N4:@N F1.@D34:@D3; D2.@N5:@N F2.@D35:@D3; D2.@N6:@N F3.@D36:@D3; D1.@E1:@E M1.@D21:@D2; D2.@E2:@E M2.@D22:@D2; M1.@T1:@T I1.@M1:@M; M2.@T2:@T I1.@M2:@M; I1.@C1:@C C1.@I1:@I; I1.@C2:@C C2.@I2:@I; I1.@C3:@C C3.@I3:@I; C2.@D13:@D1 D1.@L3:@L; C3.@D15:@D1 D1.@L5:@L; D1.@L1:@L C1.@D11:@D1; D2.@L2:@L C1.@D12:@D1; D2.@L4:@L C2.@D14:@D1; D2.@L6:@L C3.@D16:@D1; M1.@F1:@F F1.@R1:@R; M2.@F2:@F F1.@R2:@R; M1.@F3:@F F2.@R3:@R; M2.@F4:@F F2.@R4:@R; M1.@F5:@F F3.@R5:@R; M2.@F6:@F F3.@R6:@R; end. Figure 12: Formal specification of Subsystem Architecture.

(17)