Home

1 Modelling the CoCoME with the JAVA/A Component Model*

1. Figure 4 Static structure of the component TradingSystem a relay port of type CDA Bank to delegate incoming and outgoing communications be tween a bank and internal components respectively The port multiplicity with a lower bound of 1 of indicates that for a proper instantiation of TradingSystem it is strictly required to provide appropriate bank connections to the system Beyond the component TradingSystem allows for several further system config urations For example the system might be used with store components which are independent of any enterprise On this account the TradingSystem contains a set of stores simpleStores each of them connected to its own instance of a data base simpleStoresDB Since the port feature pe I PD is required only for stores belonging to an enterprise the port must not be connected in this case Enterprise An enterprise is modelled by the composite component Enterprise in Fig 5 It consists of a number of stores of a component Reporting which provides means to create several reports from the enterprise manager s point of view of a compo nent Data as an intermediate layer between Reporting and the concrete DataBase which is also instantiated as part of an Enterprise and shared between Data and the stores and finally of a component ProductDispatcher to coordinate the product exchange among the stores of the enterprise In order to provide connections for the bank ports b of the contained store
2. oo AccountSale entry saleHistory add new SaleTO co products cok i co payMode Cash icdg saleSuccess PaymentMode mode Cash J co payMode CredftCard Figure 11 Component behaviour of CashDeskApplication 14 Knapp et al C cot E port behaviour Component Coordinator E static structure saleRegistered cdld String p ProductwithStackttemTO m PaymentMode saleRegistered cald String p peel aweaban 3 ProductwwithStockttemTO m PaymentMode Coordinator lt enableExpress Boolean false decideExpressMode Boolean updateSaleHistory products ProductithStockitemTO mode PaymentMode i expressModeEnabled cashDeskld cds C CD x TComponent Coordinator E component behaviour J s lt orthagonal gt gt 2 param cd cds CashDeskR o sheskP ashDes cd saleRegistered cashDeskld String p ProductvvithStockltemTO mode PaymentMode lt port gt gt lt easync gt gt Ol 7 entry 7 _ cd saleRegistered c cD CashDeskR cd cashDeskid cashDeskld casnDeskIT String p i ProductWithStockltemT cashDeskld String lexpressModeEnabled cashDeskid String E E JOmo J PaymentMod lt sasync gt gt oO CashDeskP not enableExpress d enableExpress i cd expressModeEnabled cd id saleR
3. Any auxiliary attributes and operations in order to properly define the port behaviour are added as internal features As an example consider the port C CD showing stereotype lt port gt in Fig 12 describing the coordinator s view on a cash desk Its provided and required interfaces attached to the port by using the ball and socket notation respectively declare only asynchronous operations i e on calling these operations the caller does not wait for the callee to handle the call for succinctness we use a stereotype lt async gt to express that all operations of an interface are meant to be asynchronous it also shows an internal attribute for storing the identity of a cash desk The behaviour of port C CD is described by the UML state machine in Fig 12 top right Besides the UML state machine fea tures we use on the one hand a special completion trigger lt tau gt for modelling internal choice of the port s owning component which is enabled on state completion but in contrast to completion triggers used for those transitions not showing a trigger is not prioritised over other events On the other hand we assume all state machines to behave 4 Knapp et al like UML 2 0 s protocol state machines in the sense that it is an error if an event occurs in a state where it cannot be handled by one of the outgoing transitions Simple component A simple component see Fig 1 b consists of port properties sometimes referred
4. Fig 7 Due to this topology most of this section is devoted to the specification of the component CashDeskApplication CashDeskLine A CashDeskLine Fig 6 consists of at least one cash desk connected to a coordinator which decides on the express mode status of the cash desks The com posite component CashDeskLine declares two relay ports delegating the communica tion between the cash desks the inventory i CDA I and the bank b CDA Bank The connector declarations in Fig 6 are annotated with the stereotype adapter of kind seq meaning that the communication between the ports of the cash desks and the relay ports i and b respectively is implemented by a sequential adapter In contrast the 10 Knapp et al CashDeskLine Gj static structure J lt component gt gt a CashDeskLine cashDesks CashDesk 1 5 coordinator Coordinator 1 3 co coa c 1 MHH cas c c 1 i CDA 0 1 E zzadapter gt ind seq romo b CDA Bank 1 M ssadapter gt kind seq b CDA Bank mM Figure 6 Static structure of the component CashDeskLine communication between the cash desks and the coordinator does not need to be adapted because each CashDesk instance is linked via its CDA C port to its own instance of the coordinator port C CD To share the bank connection among the desks of a cash desk line follows the CoCoME requirement
5. architectural programming language JAVA A which allows programmers to repre sent software architectures directly in the implementation language and thus helps to prevent architectural erosion 4 In contrast to interface based component approaches like COM CORBA Koala KobrA SOFA see 5 for an overview the primary distinguishing feature of ROOM and hence of the JAVA A component model is the consistent use of ports as explicit architectural modelling elements Ports allow designers to segment the communication interface of components and thus in particular the representation of different faces to other components Moreover ports are equipped with behavioural protocols regulat ing message exchanges according to a particular viewpoint Similar to JAVA A Arch Java 6 and ComponentJ 7 are architectural programming languages which integrate This research has been partially supported by the EC 6th Framework project SENSORIA Software Engineering for Service Oriented Overlay Computers IST 016004 and the GLOWA Danube project 01LW0303A sponsored by the German Federal Ministry of Ed ucation and Research 2 Knapp et al architectural concepts into Java However neither ArchJava nor ComponentJ provide means for port protocol or component behaviour specification aside from source code Taking components to be strongly encapsulated behaviours communicating through ports fosters modular verification which is o
6. at most the behaviour of one port of C is restricted by the connection and the interac tion behaviours of all other connections reflect the behaviour of all other ports of C then deadlock freeness is preserved by the component composition This fact is expressed by the following theorem for the proof see 13 which shows that indeed for the global deadlock check it is enough if the subcomponents are locally checked for deadlock freeness and correctness and if the architect of the composite component checks each single port connection on the basis of the interaction behaviour of the connected ports Theorem 1 Deadlock freeness of composite components Let CC be a composite component with component structure as shown in Fig 18 Let the following hold 1 The components C1 Cn are correct w rt their ports qi Qi dn Qn resp and C is correct w r t to each of its ports p Py Pn Pa 2 All 1 O transition systems representing the behaviours of Ci Cn and C are deadlock free 3 For alli 1 n 1 the interaction behaviour of P and Q reflects the behaviour of P 4 The ports P and Qn are behaviourally compatible Then the I O transition system representing the behaviour of CC is deadlock free This theorem is related to a result of Bernardo et al 14 which is also motivated by the derivation of global properties from local ones not using an explicit port concept however In 14 a significantly stronger
7. barcode int saleRegistered cashDeskld String p ProductithStockitemTO mode PaymentMode seasync gt gt O CashBoxP s lt async gt gt O CoordinatorP BankR O debitCard transactionid String Debit cashBoxClosed icashAmountEntered amount double final boolean ipaymentMode mode PaymentMode expressModeEnabled cashDeskld String validateCard cardinfo String pin int String InventoryR Oo Sees igetProductvVithStockltem barcode long ProductWithStockttemTO saleFinished nt leObj SaleTO productBarcodeEntered barcode long ssasync gt raccountSale saleObj SaleTO saleStarted lt sasyno gt gt oO lt lt async gt O lt async gt gt C seasync gt gt Ol CardReaderP CardReaderR LightDisplayR CashBoxR creditCardScanned cardinto String expressModeEnabled expressModeEnabled Shang AEE EE enout Gol pinEntered pin int Eeee expressModeDisabled saleSuccess ssasync gt gt Oo ssasync gt gt Ol CDGuIR PrinterR invalidCreditCard saleFinished Q lexpressModeEnabled saleStarted runningTotalChanged productName String price double total double cashBoxClosed saleStarted cashAmountEntered amount double final boolean saleSuccess runningTotalChanged productName String price double total double cashAmountEntered amount doubl
8. Component Inventory E static structure J lt component gt a lt lt port gt spart gt Inventory LData l Manager storeld long pctx PersistenceContext Mtctx TransactionContext s lt port gt gt m l Manager 0 1 pe I PD 0 1 d l Data 1 id long l StockManager sm l StockManager 0 1 s l Sale 0 1 productOrder ProductOrder product Product stockitem Stockltem saporis eon O store StoreData LPD ProductExchangeP SaleP a barcode long ManagerP g lowStockitems Collection lt Stockitem gt StockManagerP ProductExchangeR DataR coe Set lt ComplexOrderEntry gt e lt port gt L Sale ManagerP O changePrice s StockitemTO ProductvVithStockltemTO SaleP E TOJ le DOSE CE TOG SK 25 CONNER MENTO COMPERTO igetProductv ithStockltem barcode long ProductwithStockttemTO zesignal gt gt accountSale s SaleTO StockManagerP oO rollinReceivedOrder o ComplexOrderTO DataR Oo getPersistenceContext PersistenceContext ProductExchangeP Ol queryOrderByld id long c PersistenceContext ProductOrder queryProductByld id long c PersistenceContext Product orderedProductsAvailable coe Set lt ComplexOrderEntry gt queryStockltem storeld long barcode long c PersistenceContext Stockttem lt lt async mar
9. The concrete form of the used FSP processes is not shown here but can be examined in 10 PEPA PEPA Performance Evaluation Process Algebra 8 is a process algebra that allows for quantitative analysis of the CoCoME using Continuous Time Markov Chains CTMC For the quantitative analysis of Sect 1 4 2 we used the IPC tool 9 1 5 2 Architectural Programming JAVA A 3 19 is a Java based architectural programming language which features syn tactical constructs to express JAVA A component model elements see Sect 1 2 directly in source code Thus the implementation of a component based system using JAVA A is straightforward Additionally JAVA A programs gain robustness with respect to ar chitectural erosion it is obvious to software maintainers which parts of the code belong to the architecture and therefore need special attention during maintenance We implemented a subset of the CoCoME consisting of one component CashDesk including all of its sub components and a simplified component Inventory to highlight JAVA A as implementation language for component based systems Fig 21 shows the source code of the top level composite component SimplifiedStore which contains the CashDesk and the Inventory The assembly 1 2 3 declares the sets of component and connector types which may be used in the configuration of the composite component The initial configuration consisting of one cash desk connected to one inventory is established in th
10. are acyclic star topologies as shown in Fig 18 containing one central component C with n ports such that each port is connected to the port of one of the components C for 4g STs 38 ee 1 01 E c C g cici E qt pt Pt pi Pi JH gi ai CETS en Cn By qitt ait pitt Pitt pn Pn J Jon an MRT rk Rk Figure 18 Star topology of composite component We assume that all single subcomponents C and C are correct w r t their ports and that their local behaviours are deadlock free Then if all connected ports are be haviourally compatible the composite component CC can only deadlock if at least two ports Pa Pa pg Pg of the central component C are connected to ports qa Qa qs Qg of components Ca and Cg resp such that the behaviours specified for both port types Qa and Qg properly restrict the behaviour of Pa and of Pg in an incompatible Only 7 transitions occurring in an alternative may not be removable according to the well known fact that alternatives are i g not compatible with the observational equivalence Modelling the CoCoME with the JAVA A Component Model 23 way This may happen if C introduces a dependency between P and Pg that is in compatible with the simultaneous restrictions imposed by the connections with Qa and Qg on both sides of C An example for such a situation is provided in 13 If however
11. condition is used requiring what we call be haviour reflection for all connections between components with no exception where behavioural compatibility is sufficient as in the above theorem A further generalisation of the theorem to arbitrary many non behaviour reflecting but behavioural compatible connections is given in 13 which however needs further assumptions We can directly apply Thm 1 to analyse the behaviour of the composite compo nent CashDesk cf Fig 7 where CashDeskApplication plays the role of the central component C As pointed out above all subcomponents of CashDesk are correct w r t their respective ports and their behaviour is deadlock free We also have analysed with HuGO RT and the LTSA tool see Sect 1 5 1 the given connectors between the ports of CashDeskApplication and the ports of the other subcomponents of CashDesk It turns out that the port CDA CB of CashDeskApplication is behaviourally compatible with the port CB CDA of the CashBox component and that for all other connected ports the interaction behaviour even reflects the behaviour of the corresponding port of CashDeskApplication Hence Thm shows that the component CashDesk does not deadlock We can also show see 10 that the CashDesk component is correct w r t its relay ports 10 Note that it is sufficient to consider the behaviours of the ports of Ca and Cg instead of considering the observable behaviour of the components Ca and Cg since both
12. data as well as to mark products for delivery to other stores i e playing the passive role of being asked for product exchange Both messages are eventually received during a connection with the component ProductDispatcher see Fig 5 responsible to coordi nate the product exchange among the stores see 11 Fig 1 6 inventory amp component behaviour J gt Further regions omitted E TK N entry alowStocktem ristmetyO d lowStockttems d queryLowStockttems storeld pctx i d markProductsAsincoming coe else pe products dlowStockitems getProducts pe orderAtOtherStores storeld pe products else pe orderedProductsA vailable coe lt Set lt ComplexOrderEntry gt f e pe markProductsF orDelivery coe Set lt ComplexOrderEntry gt i i d markProductsUnavailableinStock coe Figure 14 Component behaviour of the Inventory regions omitted The component behaviour specification of Inventory comprises of six orthogonal regions essentially each of them modelling the interaction with one possible commu nication partner along the ports of the component For a lack of space Fig 14 shows only two of them Again for more details we refer to 10 The regions shown illustrate part of the interplay between the ports d and pe in the course of executing a product exchange among stores The upper region specifies the component s behaviour with re s
13. in 11 Fig 1 6 which shows a multiplicity of 1 for the particular required Bank interface port respectively CashDesk CD The CashDesk component specified in Fig 7 is the most complex composite of the trading system The component consists of six components modelling the hardware devices as described in the CoCoME and one component modelling the cash desk application A cash desk has three relay ports to allow for the communication with a bank inventory and coordinator component The component and port multiplic ities of the static structure in Fig 7 reflect the requirements of the CoCoME Since an exceptional process for Use Case 1 Process Sale 11 explicitly mentions that the in ventory might not be available the relay port i may sometimes not be connected The optional ports of CashBox Scanner and CardReader model the communication of an operator with the particular hardware device In case of a cash desk actually deployed these ports might be connected with some low level interrupt handler Component CashDeskt Ej static structure J lt acomponent gt gt 2 CashDesk cda CashDeskApplication 1 3 ch CDA CB 1 cdg CDA CDG 1 b CDA Bank 1 i CDA 0 1 co CDA C 1 N N Ye me CDA Bank 1 E CDA 0 1 X co CDA C 1 Figure 7 Static structure of the component CashDesk Modelling the CoCoME with the JAVA A C
14. stock manager requests The behaviour specifications of these ports are trivial and omitted here The ports may be used for instance to connect simulation components in order to test the developed system or of course to connect actual control interfaces in the deployed system 4 Note that our component Inventory models Inventory Application Store of 11 see Sect 1 3 1 16 Knapp et al The ports of type Data and I Sale are used to connect to the data layer of a store component and to the cash desks of the store respectively As the port behaviour of l Data in Fig 13 exemplifies for two operations of the interface DataR any operation call on the data layer is transactional i e is framed by an explicit transaction start tctx beginTransaction and end tctx commit the remaining operations of DataR are applied analogously Connections via l Sale support the reception of messages required during the sale process at a cash desk The component declares a port pe PE in order to cope with product exchange among stores as described in Use Case 8 of the CoCoME The port behaviour specifica tion in Fig 13 uses an orthogonal state with two regions to model the two distinct roles of an inventory the port may request to order some products at the other stores of the enterprise i e play the active role of initiating product exchange on the other hand it provides a trigger for a data base update with possibly cached and not yet submitted
15. tau gt PaymentMode saleStarted ff not final jpaymentMode mode PaymentMode mode Cash cashAmountEntered cft final a ET cashAmountEntered amount sashan noii double final boolean final mode Cash lt etaur gt M lt staur gt lt stau gt gt double final boolean nat final final F pay cashAmountEntered amount final lt n changeAmountCaiculatedichangeAmounty OJ 1 salesuboess0 JinvalidCreditCard productBarcodeEntered paymentMode mode barcode long mode Cash PaymentMode f paymentMode mode mode Cash soli y PaymentMode else gt T saleStarted expressModeDisabled estau gt y arse eeu expressModeDisabled Ly i expressModeEnabled x e A saleStarted Pi tks Figure 9 Behaviour of the CDA ports CB and CDG CDA Port Behaviour The state machine CDA CB in Fig 9 specifies the communica tion between the cash desk application and the cash box CB In general the state machine for a port receives events and signals named in the provided interface of that port and sends out signals and events named in the required interface of that port After initially having received the signal saleStarted defined in the port s provided interface CashBoxP in Fig 8 the port may receive arbitrary many manually entered product bar codes befor
16. we will need a simple form of relabelling of an I O transition system A denoted by n A where the labels of A are just prefixed by a given name n thus obtaining a copy of A An I O transition system A is deadlock free if for any reachable state there is an outgoing sequence of transitions T a 7 with some label a T preceeded and followed by arbitrary many 7 actions The obser vational equivalence relation is compatible with deadlock freeness and moreover it gt Internal actions are not invisible to construct particular component views they can however be hidden The product of two I O transition systems is used to model their parallel composition with synchronisation on corresponding input output labels 18 Knapp et al is preserved by the above mentioned operators on transition systems For the precise technical definitions we refer to 10 Let us first consider how behaviour specifications of ports are represented by I O transition systems As pointed out in Sect 1 2 a port has a provided and a required interface For calls of operations of the provided interface we use input labels for send ing an operation request according to the required interface of a port we use output labels In most cases the label is just the name of an interface operation where we have abstracted from operation parameters and results which is possible if the transitions in the original state machine do not depend on the arguments and results of the
17. 1 Modelling the CoCoME with the JAVA A Component Model Alexander Knappt Stephan Janisch Rolf Hennicker Allan Clark Stephen Gilmore Florian Hacklinger Hubert Baumeister and Martin Wirsing 1 Institut fiir Informatik Ludwig Maximilians Universitat M nchen hacklinger hennicker janisch knapp wirsing ifi lmu de Laboratory for Foundations of Computer Science University of Edinburgh a d clark Stephen Gilmore ed ac uk 3 Informatik og Matematisk Modellering Danmarks Tekniske Universitet Lyngby hub imm dtu dk 1 1 Introduction The JAVA A approach aims at semantically well founded and coherent modelling and programming concepts for components based on sound theoretical foundations it en hances the widely used UML 2 0 component model by modular analysis and verifi cation techniques and a Java based architectural programming language Our JAVA A component model is inspired by ideas from Real Time Object Oriented Modeling ROOM 1 components are strongly encapsulated behaviours and any interaction of components with their environment is regulated by ports We took up the ROOM model in its version integrated into the Unified Modeling Language 2 0 UML 2 0 2 though in a simplified form which however keeps the main structuring mechanisms and focuses on strong encapsulation as well as hierarchical composition In 3 we de vised an algebraic semantic framework for this model furthermore we introduced an
18. Bank 1 I av DataBase 1 Component Store jj static structure j lt lt component gt gt a Store cdl CashDeskLine 1 5 i Inventory 1 i CDA 0 4 s l Sale 0 1 d Data 1 b CDA Bank 1 pe PD 0 1 sm StockManager 0 1 m l Manager 0 1 b CDA Bank 1 pe LPD 0 1 dio DataBase 1 poy Figure 5 Static structure of the components Enterprise and Store configurations with stores that are independent of any enterprise In this case there is definitely no other store to exchange products with 1 3 3 Cash Desks The Embedded System Part Any store instantiated as part of the trading system comprises a cash desk line which in turn represents a set of cash desks monitored by a coordinator Each cash desk consists of several hardware devices managed by a cash desk PC The specification of the cash desk line models the embedded system part of the CoCoME with characteristic features of reactive systems such as asynchronous message exchange or topologies with a dis tinguished controller component The former is illustrated by the subsequent behaviour specifications for ports and components the latter is exemplified directly in the static structure of the composite component CashDesk with the cash desk application playing the role of the controlling component at the centre
19. Performance Analysis on the DEGAS Choreographer Platform In Fitzgerald J S Hayes LJ Tarlecki A eds Proc Int Symp Formal Methods Europe FM 05 Volume 3582 of Lect Notes Comp Sci Springer Berlin 2005 286 301 Knapp A HUGO RT Web page http www pst ifi lmu de projekte hugo 05 02 07 Hacklinger F JAVA A Taking Components into Java In Proc 13 ISCA Int Conf Intelligent and Adaptive Systems and Software Engineering IASSE 04 ISCA Cary NC 2004 163 169
20. ac uk ipo 05 02 07 Baumeister H Clark A Gilmore S Hacklinger F Hennicker R Janisch S Knapp A Wirsing M Modelling the CoCoME with the JAvA A Component Model http www pst ifi lmu de Research current projects cocome 05 02 07 Reussner R Krogmann K Koziolek H Rausch A Herold S Klus H Welsch Y Hummel B Meisinger M Pfaller C Mirandola R Chapter 3 CoOCoME The Common Component Modelling Example In CoCoME Book 2007 Magee J Kramer J Concurrency State Models and Java Programs John Wiley amp Sons 1999 Hennicker R Janisch S Knapp A On the Compositional Analysis of Hierarchical Components with Explicit Ports 2007 Submitted http www pst ifi lmu de Research current projects cocome 06 22 07 Bernardo M Ciancarini P Donatiello L Architecting Families of Software Systems with Process Algebras ACM Trans Softw Eng Methodol 11 4 2002 386 426 Hennicker R Baumeister H Knapp A Wirsing M Specifying Component Invariants with OCL In Bauknecht K Brauer W Miick T eds Proc GI OCG Jahrestagung Vol ume 157 I of books ocg at OGI Austrian Computer Society 2001 600 607 Bidoit M Hennicker R A Model theoretic Foundation for Contract based Software Components 2007 Submitted http www pst ifi lmu de people staff hennicker Buchholtz M Gilmore S Haenel V Montangero C End to End Integrated Security and
21. act the functionality of this component is exclusively to generate reports for the enterprise manager Therefore we decided to model Store and Enterprise as functional components on their own An enterprise may contain a number of stores comprising an inventory and a cash desk line Reporting then is part of Enterprise but not of Store as this seems to model the application domain of the required trading system more naturally The Data layer of the CoCoME is represented by the component Data with ports modelling the enterprise and the store related data aspects Notice that as required in the CoCoME different instances of the Data component may share the same instance of a DataBase component This issue depends on a concrete system configuration only Last the GUI layer is represented by the operator ports of the components Enterprise and Store Further structural deviations concern the original component Data Persistence which is in our approach not modelled explicitly but integrated with the port modelling of the Data component instead Also the sequence diagram 11 Fig 1 6 concerning the product exchange among stores of the same enterprise Use Case 8 shows a compo nent ProductDispatcher which is not mentioned in the structural view of the CoCoME We modelled this component as part of the enterprise component 1 3 2 Trading System Stores and Enterprises This section describes the specifications for the root component TradingSystem as w
22. as shown in Fig 15 Hence the interaction behaviour of the two ports is represented by the transition system of their port product which is 8 Our approach would also allow a more general condition where the required operations of one port are included in the provided operations of the other one which however is not needed for the current case study Modelling the CoCoME with the JAvA A Component Model 21 _saleRegistered e expressModeEnabled_ tau tau saleRegistered saleRegistered expressModeEnabled _ tau Figure 17 Port product of CDA C and C CD shown in Fig 17 bottom Obviously the port product has no deadlock and therefore the two ports are behaviourally compatible In general the potential capabilities for interaction of a port will not be used when the port is connected to another port In this case the behaviour specified for that port is restricted by the interaction with another port It is however often the case that this restriction applies only to one side of a connection while the behaviour of the other port is not restricted and hence fully reflected by the interaction Given two ports PR and P with behaviours represented by I O transition systems Ap Ap respectively the interaction behaviour of P and P reflects the behaviour of P if the port product is observationally equivalent to the behaviour of P i e Ap Ap Ap This property plays an essential role for the composit
23. atic structure modelling for simple non composite components we designed component and port behaviours hand in hand in case of the embedded system part accompanied by formal analysis Finally the sim ple components were applied for the design of the composite components yielding a first draft of the complete architecture Within the next iterations the alternative and exceptional processes of the use case descriptions were taken into account to extend and correct the initial design In case of ambiguous or unclear requirements our design followed the prototype implementation of the CoCoME Since we fully agree with the data model provided in 11 we omit specifications of data types transfer objects for data exchange and enumerations Our specifications comprise UML 2 0 class and composite structure diagrams to specify the static structure of components ports and interfaces and UML 2 0 state ma chine diagrams to specify the behavioural view for ports and components Familiarity with terms notions and functional requirements of the trading system 11 is assumed For lack of space we do not discuss the specifications of components and ports shown in grey in Figs 3 7 Instead we restrict our attention on a detailed presentation of the embedded system part which is also the focus of our functional analysis Additionally we provide a representative extract of our model for the information system part of the CoCoME Specifications not discussed he
24. components are assumed to be correct w r t their respective ports 24 Knapp et al Following our analysis method we now go one step up in the component hierar chy and consider the composite component CashDeskLine cf Fig 6 which has con nected subcomponents of type CashDesk and Coordinator Obviously the structure of CashDeskLine fits again to the component structure assumed in Thm 1 Hence we can directly apply Thm 1 since we know that CashDesk is correct and deadlock free Coordinator is correct and deadlock free see paragraph on the analysis of simple com ponents and that the connection between the ports of type CDA C and C CD reflects the behaviour of CDA C see paragraph on the analysis of connectors Thus component CashDeskLine does not deadlock and according to the reflection of the appropriate port behaviour it is also correct w r t its relay ports Note again that we did not take into account here multiplicities of component decla rations which means in this example that we have disregarded the number of CashDesk instances that are connected to one Coordinator instance This abstraction works be cause first the Coordinator instance has as many port instances of type C CD as there are cash desks connected and more importantly the interactions of the coordinator with the single cash desks are independent More formally this means that if there are n cash desks connected to the coordinator then arbitrary interleaving
25. cribed in 11 is shown The right hand side shows the corresponding modelling within our approach From deviations with our static model almost naturally some de viations in behavioural aspects follow We omit a detailed discussion here and refer to 10 for component wise details on this issue As the most important deviation in the embedded system part we did not model the event bus component which is used in the CoCoME for the communication between the subcomponents of the cash desk line on the one hand and between those the coor dinator and external components on the other hand Instead of a functional component our approach provides explicit models of component communications and interactions using port and component behaviour specifications We consider the integration of an event bus to be an implementation decision where the implementation should guarantee that the specified communication structure of the design model is respected Explicit modelling of the cash desk s internal interaction structure constitutes the internal topology of our composite component CashDesk see Fig 7 deviating from the cash desk s inner structure as shown in 11 Fig 1 6 During the modelling of the subcomponent s communication it soon became apparent that in our approach the most appropriate topology for the CashDesk is the one specified in Fig 7 The central functionality of handling sales almost always requires the cash desk application to re cei
26. declarations in particular as indicated by the tagged value kind seq the adapter component sequentialises the different calls A sample runtime configuration of the composite component CashDeskLine is given in Fig 2 This configuration shows two instances of component CashDesk and a single instance of component Coordinator The CDA C port instances of the cash desks are connected to two different instances of the C CD coordinator port The CDA Bank Modelling the CoCoME with the JAVA A Component Model 5 CashDeskLine CDA Bank CDA I a CashDesk z T Bank CashDesk a A CDA I CDA Bank Cahier CDA C o PODAC Coordinator a C CD C CD Figure 2 Sample configuration of component CashDeskLine of Fig 6 port instances of the cash desks are adapted to one relay port instance of the cash desk line by the auxiliary adapter component A CDA Bank Similarly the CDA I port instance of the cash desk to the right the other cash desk does not show a CDA I port instance in accordance with the multiplicity of the port feature declaration i is relayed 1 3 Modelling the CoOCoME We started the design of the CoCoME from the use case descriptions and sequence diagrams as given in 11 After and during st
27. e final boolean changeAmountCalculated amount double invaliditem saleSuccess jlexpressModeDisabled Figure 8 Static structure of the CDA component CashDeskApplication CDA The cash desk application links all internal components of a cash desk and communicates with components external to the cash desk such as a bank the inventory or the coordinator In order to facilitate the particular communica tion CashDeskApplication declares one port for each Figure 8 top shows an overview of the component with its private state as well as its ports and interfaces the ports state attributes and the interface details are given in the middle and lower region respectively As a naming convention we have used component abbreviations such as CDA CB for the port types and the suffixes R P for interfaces required provided by a port In the following we briefly describe representative port behaviours of the CDA Thereafter we discuss the specification of the component behaviour which interrelates the constituent port behaviours within a single state machine 11 12 Knapp et al CDA CBl E port behaviour J cda cD E port behaviour expressModeDisabled productBarcodeEntered mmm kai bared long J invvaliter Pa saleStarted yl Y 1 saleStarted0 4 C i saleSuccess 5 J saleFinished tau C ashBoxClosed paymentMode mode lt lt
28. e constructor of the composite component 1 4 11 Components which are declared with the additional keyword act ive will be started after the initialisation process which basically consists of initialising and connecting the components composite component SimplifiedStore 2 assembly components Inventory CashDesk connectors Inventory Sale CashDesk CDAI 4 constructor Store initial configuration 6 active component Inventory inv new Inventory active component CashDesk cd new CashDesk 8 connector Connector con new Connector con connect inv Sale cd CDAI Figure 21 JAVA A composite component SimplifiedStore 28 Knapp et al In Fig 22 we give a very brief overview of the JAVA A implementation of the com ponent CashDeskApplication In lines 3 20 the port CDACB is declared see Fig 9 Provided operations annotated with the keyword async instead of a return type are asynchronous The port protocol lines 10 19 is specified using the language UTE In order to verify the absence of deadlocks of the connection of two ports the JAVA A compiler is closely integrated with HUGO RT see Sect 1 5 1 The operations declared in a port s provided interface must have a realisation in the respective port s component The implementation of the provided operation saleStarted of the port CDACB is shown in lines 21 24 In the body of the private helper method processSaleStarted lines 25 31 required port o
29. e moving to the next state due to the reception of saleFinished manu ally entered product bar codes are part of an exceptional process in Use Case 1 of the CoCoME The next step within the sale process is the selection of card or cash pay ment as the payment procedure If payment mode Cash was selected the port waits for messages concerning the cash amount received from the customer It sends back infor mation concerning the change amount calculated by sending changeAmountCalculated defined in CDA CB s required interface CashBoxR in Fig 8 assumes that the cash box is subsequently opened and finally waits for the cash box to be closed again If payment mode CreditCard was chosen the port changes to a state where the chosen mode may be cancelled by switching to cash payment and additionally a 7 transition may be trig gered internally whereupon the cash box should be prepared to receive a saleSuccess as a signal for the successful clearing of the sale process via card payment In both cases the port waits afterwards for the next saleStarted and until then allows to disable the express mode the cash desk may have been switched into in the meantime In contrast to the behaviour at an input port Fig 9 also shows an example for an output port behaviour the specification of CDA CDG which is intended to connect to the cash desk s GUI In fact the behaviour is very similar to the specification of CDA P connecting to the printer not
30. e obtain up to the prefix cd the transition system in Fig 15 which represents the behaviour of the port type C CD This shows the correctness of the Coordinator component Indeed we have checked with the LTSA tool cf Sect 1 5 that all simple components occurring in the CashDesk and CashDeskLine composite components cf Sect 1 2 are correct The definition of the observable behaviour of a component at a particular port can be generalised in a straightforward way to arbitrary subsets of the port declarations of a component and in particular to the case where all ports of a component are simulta neously considered to be observable For a component C the latter is called the fully observable behaviour of C and denoted by obs C Obviously the above definitions of correctness and observable behaviour apply not only to simple but also to composite components considered in the next step Analysis of composite components The analysis of composite components is related to the task of a system architect who puts components together to build larger ones Before we can analyse the behaviour of a composite component it is crucial to consider the connections that have been established between the ports of their subcomponents Analysis of connectors For the analysis of connectors one has first to check whether the connections between the ports of components are syntactically well defined After that we can analyse the interaction behaviour of two c
31. ed continuous time Markov chains to quantify performance Currently we are developing support for modelling runtime reconfigurations of component networks This will be necessary if the CoCoME requirements would be extended e g to use cases for opening and closing cash desks Also the current com ponent model does not directly integrate means for specifying non functional proper ties Our component model assumes that all connectors are binary which due to the possibility to define ports with an arbitrary multiplicity is no proper restriction How ever our analysis method actually supports multiplicities greater than one only if the actions of parallel executing instances of the same port or component declaration can be arbitrarily interleaved which was indeed the case in the example In the centre of our behavioural analysis was the interaction behaviour of components with asynchronous message exchange via their ports For synchronous data oriented behaviours we still should add assertion based techniques e g in terms of pre and post conditions whose integration in a concurrent environment however needs further investigation Acknowledgements We would like to thank the organisers for the detailed preparation of the common component modelling example We gratefully acknowledge many very useful and detailed comments made by the referees of a previous version of this study We also would like to thank Mila Majster Cederbaum for many fruit
32. egistered cald String p ProductWithStockltemTO m PaymentMode Figure 12 Static structure and behaviour specifications of Coordinator received at the cash box port cb the submachine Scanltems repeatedly receives prod uct bar codes and notifies the printer and the GUI about product details like name and price Thereafter the payment mode must be chosen resulting in a transition to the corresponding submachine CardPayment may be left at any state by the reception of cb paymentMode Cash modelling the cashier s ability to switch from card to cash pay ment e g in case of problems with the credit card Before the sale process is completed the component tries to account the sale at the inventory using port i within AccountSale If the inventory is not available the sale information is stored locally and delivered dur ing the next sale processes Finally in SwitchMode the component waits for a signal to switch into express mode to disable a previous express mode or to start a new sale Coordinator C The cash desk line see Fig 6 of a store consists of a number of cash desks and an instance of Coordinator see Fig 12 which decides on the mode of the cash desks express or normal The component declares its port of type C CD with multiplic ity to allow to connect an arbitrary number of cash desks which should be monitored by this coordinator Note that even if the coordinator decided for express mode t
33. ell as the two fundamental components Stores and Enterprises all of them being composed from further components TradingSystem The composite component TradingSystem in Fig 4 provides flexi ble instantiation possibilities for different system configurations As will be evident from the specifications of the composite components Enterprise and Store described hereafter the former contains among others a number of stores and a Store in turn contains further components such as the CashDeskLine In fact a system configuration following the hierarchy further down from one instance of Enterprise already suffices to meet the original CoCoME requirements for a trading system with an enterprise and a number of stores which belong to this enterprise In this case the sets of simpleStores and simpleStoresDB would be empty as these are used only in case of extended system configurations with stores independent from any enterprise The bank component required for card payment at the cash desks of a store is con sidered external to the trading system Therefore the component TradingSystem declares 8 Knapp et al Component TradingSystem fj static structure scomponent gt TradingSystem enterprises Enterprise a HD s coa Bank 1 4 b CDAABank 1 independentStores Store l 3 F b CDA Bank 1 db DataBase 1 L_H pe PD 0 1
34. esented by the I O transition system Ap Intuitively the component C is correct w r t its port declaration p P if the component behaviour supports the behaviour specified for that port Appar ently this is the case if the component s behaviour observable at port p is observationally equivalent to the behaviour specification of P up to an appropriate relabelling Formally the observable behaviour of C at port p denoted by obs C can be constructed by hiding all labels of Ag which do not refer to p Using the hiding operator obs C is just Ac H where the set H of hidden labels consists of the internal labels of Ac together with all input or output labels g op of Ac such that q p Since the transition system obs C has no internal labels and up to the prefix p the same input and output labels as Ap we can now require that it is observationally equivalent to p Ap i e obsp C p Ap where p Ap is the copy of Ap explained above In this case we say that the component C is correct w rt its port declaration p P Let us illustrate how we can check the correctness of the component Coordinator w r t to a port instance cd of type C CD First we consider the observable behaviour of the Coordinator at the port instance cd which is just the transition system shown in 20 Knapp et al Fig 16 where all labels which are not prefixed by cd are replaced by r If we min imise this transition system w r t observational equivalence then w
35. ful discussions on the topic of interacting systems and their verification 1 Selic B Gullekson G Ward P T Real Time Object Oriented Modeling John Wiley amp Sons New York 1994 2 Object Management Group Unified Modeling Language Superstructure Version 2 0 Tech nical report OMG 2005 3 Baumeister H Hacklinger F Hennicker R Knapp A Wirsing M A Component Model for Architectural Programming In Barbosa L Liu Z eds Proc 2nd Int Wsh Formal Aspects of Component Software FACS 05 Volume 160 of Elect Notes Theo Comp Sci 2006 75 96 30 10 11 12 13 14 15 16 17 18 19 Aldrich J ArchJava http www archjava org Seco J Caires L A Basic Model of Typed Components In Bertino E ed Proc 14 Eu Knapp et al Perry D E Wolf A L Foundations for the Study of Software Architecture ACM SIGSOFT Softw Eng Notes 17 4 1992 40 52 Lau K K Wang Z A Survey of Software Component Models Second Edition Technical Report CSPP 38 School of Computer Science The University of Manchester 2006 05 17 07 rop Conf Object Oriented Programming ECOOP 00 Volume 1850 of Lect Notes Comp Sci Springer Berlin 2000 108 128 Hillston J A Compositional Approach to Performance Modelling Cambridge University Press 1996 Bradley J Clark A Gilmore S User manual for IPC The Imperial PEPA Compiler http www doc ic
36. he port may receive yet another sale registration from the same cash desk because the com munication partners are executing concurrently In this case the sale registration has precedence over the coordinator s decision the port recomputes its internal decision The component behaviour shown alongside the port behaviour in Fig 12 illustrates the modelling of internal actions of a component which are hidden by r transitions in the port behaviour specification For each cash desk the component keeps track of the particular sale history and decides upon this history to eventually switch a cash desk into express mode The update of the sale history is synchronised annotation sequential due to the concurrent execution of the port instances cd in cds 1 3 4 Inventory The Information System Part The information system part is modelled with an inventory at the core The inventory plays a crucial role in the Use Cases 3 4 7 and 8 see 11 Figs 1 6 1 6 1 6 1 6 which Modelling the CoCoME with the JAVA A Component Model 15 describe how to order products receive ordered products change the price of a prod uct and how products might be exchanged among the stores of a enterprise The most prominent new modelling aspect with respect to the embedded system part in Sect 1 3 3 is the specification of synchronous message call receptions The specifications of Data Reporting ProductDispatcher and DataBase can be found on our web page 10
37. ionality of component behaviours considered below An obvious consequence of this definition is that if the interaction behaviour of P and P reflects the behaviour of P P resp and if the behaviour of the port A P resp is deadlock free then A and P are behaviourally compatible For instance let us consider again the port product of CDA C and C CD in Fig 17 bottom After minimisation of the transition system w r t observational equivalence with the LTSA tool we obtain just the transition system of the port CDA C cf Fig 17 top Hence the interaction behaviour of CDA C and C CD even reflects the behaviour of the port CDA C Analysis of the behaviour of composite components In contrast to simple components the behaviour of a composite component is not explicitly specified by the developer but can be derived from the behaviours of the single parts of the composite component For that purpose we construct the product of the transition systems representing the ob servable behaviours of all subcomponents declared in a composite component whereby the single behaviours of the subcomponents observed at their ports are synchronised according to the shared labels determined by the connectors Hence we focus on the interactions between the subcomponents via their connected ports and on the actions on the relay ports of the composite component while the internal behaviour of the sub components is not relevant see 10 for the detailed defin
38. is allowed and thus deadlock freeness of the cash desk line does not depend on n Let us now come back to the original proposal of the CashDeskLine structure which has used an event bus for communication 11 We have refrained from using the event bus in the design model as we believe that the introduction of an event bus is an imple mentation decision to be taken after the design model has been established and analysed Indeed we could introduce right now an implementation model which implements the communication between the components of the CashDesk and CashDeskLine in terms of an event bus provided that the bus follows the first in first out principle Then ob viously the order of communications between the single components specified in our design model would be preserved by the implementation model and hence the deadlock freeness of the design model would also hold for the event bus based implementation This concludes the behavioural analysis of the asynchronous part of our model for the CoCoME which was in the centre of our interest For the synchronous information oriented part we suggest to apply pre post condition techniques which have been lifted to the level of components in our previous 15 and recent 16 work 1 4 2 Non Functional Requirements We perform quantitative analysis of the Process Sale Use Case 1 by modelling the ex ample in the process algebra PEPA 8 and mapping it onto a Continuous Time Markov Chain CTMC fo
39. iting for credit card validation the extra functional properties state that we have a histogram representing the distribution over the expected durations stating that with probability 0 9 validation will take between 4 and 5 seconds and with probability 0 1 it will take between 5 and 20 seconds We encode distributions such as these in the process algebra PEPA as an immediate probabilistic choice followed by a validation occurring at expected rate 4 5 is mid way between 4 and 5 and 12 5 is mid way between 5 and 20 so we use these as our means 7 0 9 immediate validate 1 4 5 7 0 1 immediate validate 1 12 5 Whichever branch is taken the next activity is validation the only difference is the rate at which the validation happens In Fig 19 we show how 700000 values from a uniformly distributed interpretation of the histogram for credit card validation would differ from the exponentially distributed interpretation In our experience a distribution such as that shown in Fig 19 left is unlikely to occur in practice For example it has the surprising property that delays of four seconds are very likely but delays of three seconds are impossible Also there is a very marked difference between the number of delays of five seconds and delays of six In contrast distributions as seen from our sample in Fig 19 right occur frequently because they are a convolution of two heavy tailed distributions Other histogram specified conti
40. itions 22 Knapp et al Of course one may again construct the observable behaviour of a composite com ponent which then could be used for further analysis but also for the construction of the behaviour of another composite component on the next hierarchy level When climbing up the hierarchy of composite components one can always first perform a minimisation of the observable behaviour of the subcomponents before the behaviour of the com posite component on the next level is constructed This technique can indeed be very efficient to reduce the state space of nested components because depending on the ap plication many or even all r transitions may be removed In fact our experience shows that in this way there is often not even an increment of the size of the state space 13 In the following we focus on checking the deadlock freeness of the behaviour of a composite component It is well known that in general the deadlock freeness of sub components does not guarantee the deadlock freeness of a global system as nicely illustrated by Dijkstra s philosophers example Indeed this is unfortunately still the case if all components are correct w r t their ports in the sense from above and if all ports are connected in a behaviourally compatible way as soon as more than two subcomponents are involved Hence we are looking for particular topologies of com ponent structures where deadlock freeness is preserved An appropriate candidate
41. kProductsForDelivery coe Set lt ComplexOrderEntry gt queryStockltemByld stordeld long c PersistenceContext Stockttem lt sasync triggerDatabaseWrite queryLowStockltems storeld long PersistenceContext Collection lt Stockttem gt queryStoreByld storeld long c PersistenceContext StoreData markProductsincoming coe Set lt ComplexOrderEntry gt ProductEschengoR O markProductsunavaiiabieinStockt coe Set lt ComplexOrderEntry gt lt zasync gt orderAtOtherStores storeld long products Set lt Product triggerDatabaseWrite l Data 5 port behaviour 1 PEL 55 port behaviour J triggerDatabaseWrite i petx getPersigtenceContext tetx petx getTransactionContext Sale E port behaviour J markProducts oe pe Set ComplexOrderEntry gt accourtSalet 2 SaleTO itctx beginTrar i ftetx commitQ forderAtOtherStores storeld products J productOrder 3 orderedProducts4vailable coe J product queryProductByld id pctx Set lt ComplexOrderEntry gt Figure 13 Static structure and port behaviour of the component Inventory Inventory I The component Inventory is a model of the store s portion of the ap plication layer of the CoCoME As depicted in the static structure of Fig 13 Inventory provides two optional ports m l Manager and sm I StockManager to allow for man ager and
42. l system Our analysis process consists of the following steps 1 For each simple component we analyse the behaviour specification of each of its ports the behaviour specification of the component itself and the relationships between the component behaviour and the behaviour specified for each of its ports 2 For each composite component we analyse the interaction behaviour of connected ports the behaviour of the composite component which can be inferred from the behaviours of its constituent parts and the relationships between the behaviour of the composite component and the behaviour of each of its relay ports The semantic basis of our study are the given UML state machines for the behaviour specifications of ports and components In order to treat them in a formal way we represent them by labelled I O transition systems which are automata with an initial state and with distinguished input or provided output or required and internal la bels Additionally we assume that there is a special invisible or silent action 7 Two I O transition systems A and B over the same I O labelling are observationally equiv alent denoted by A B if there exists a weak bisimulation relation between A and B e g in the sense of 12 where all actions apart from 7 are considered to be visible We also use standard operators on I O transition systems like relabelling hiding and the formation of products In some cases
43. ne of the aims of the JAVA A approach Using our semantic foundations we employ the model checking tools HUGO RT and LTSA to verify that components comply to their ports and that connected ports can communicate successfully by a compositionality theorem we can then lift these prop erties to hierarchical composite components For quantitative properties we represent the component semantics though rather abstractly in the PEPA process algebra 8 and use continuous time Markov chains for performance analysis with the IPC tool 9 The second aim of the JAVA A approach is the representation of software architecture entities in a programming language We use the code generation engine HUGO RT to translate the behaviour of components into Java code the usage of the same tool for verification and code generation helps in transferring design properties into the code The remainder of this chapter is structured as follows After a short introduction to the JAVA A component model in Sect 1 2 we present selected parts of our model of the CoCoME trading system in Sect 1 3 including the CashDeskLine and the Inventory In Sect 1 4 we show how the formal algebraic basis of our model allows one to thor oughly analyse and verify important qualitative and quantitative properties In partic ular we show that the composite component CashDeskLine is correct and deadlock free as an example for performance analysis we study the use of express checkouts and show
44. ng the port declarations of the static structure in Fig 8 it shows the dependencies and inter linkages between the different ports of the CDA For example messages sent via ports p or cdg such as p saleStarted and cdg saleStarted are sequen tially arranged after the message cb saleStarted was received at port cb Furthermore port attributes as well as component attributes such as itemCounter are assigned as an effect and afterwards used as actual parameters in messages sent Since the specification of the cash desk application s behaviour is rather involved we used submachines to factor out the major steps of the entire sale process For lack of space we refer to 10 for their detailed specification However a brief description may provide an intuitive understanding of the component s behaviour after saleStarted was Component CashDeskApplication component behaviour J Scanitems ico saleRegisterei cashDeskld co products co payMode ch saleStarted N r entry entry i p saleStarted co products new List lt ProductvvithStockttemTO cdg saleStarted itemCounter 0 7 cdg total 0 0 oo SwitchMode oo ch saleStarted y cb paymentMode mode PaymentMode mode Cash ee mode CreditCard CJ CashPayment cb paymentmode mode CardPayment oo entry Cdg amount 0 0 cdg tinal false ch amountEntered 0 0 ch changeAmount 0 0
45. nment via its ports any input label of a component has the form p i where p is a port name and 2 is an input label of the port Similarly the output labels of a component have the form p o For the definition of input and output labels of components we do not take into account here the multiplicities of ports This is possible if we assume that actions of different port instances of the same port declaration are independent from each other which is indeed the case in our example In the following we will always omit multiplicities in port declarations In contrast to ports components can have internal labels which are just given by some name representing an internal action of the component Again for 7 For the representation of the transition systems we have used the LTSA tool cf Sect 1 5 which does not support the symbol used in UML state machines In order to indicate that i is an input label we use i_ and symmetrically to indicate that o is an output label we use _o Modelling the CoCoME with the JAVA A Component Model 19 the purpose of model checking we assume that arguments results and or guards of internal operations are encoded into appropriate labels As an example we consider the behaviour specification of the Coordinator com ponent see Fig 12 The behaviour specification uses an entry action and a pseudo state for a guarded alternative which both have to be resolved in the corresponding transition system For represe
46. nting the entry action we introduce the internal label entry and for representing the two guarded alternatives we introduce two internal labels enableExpress describing the decision that the express mode should be enabled and notEnableExpress expressing the converse case Operation calls have now the prefix cds of the port on which the operation is received or sent The whole transition system representing the behaviour of the Coordinator component is shown in Fig 16 cd saleRegistered_ entry enableExpress cd saleRegistered_ notEnableExpress ESS 4 _cd expressModeEnabled Figure 16 I O transition system for component Coordinator Analysis of Simple Components In the first step of our model analysis we consider simple components which are the basic building blocks of our system model For each simple component we check the deadlock freeness of the behaviour specifications of each of its ports and of the component itself Obviously this condition is satisfied for all simple components and ports of our behavioural model for the CoCoME A more subtle point concerns the relationships between the behaviour of a com ponent and the behaviour specified for each of its ports which must in some sense fit together To consider this issue more closely let C be a component with associated be haviour represented by the I O transition system Ac and let p P be a port declaration of C such that the behaviour specification associated to P is repr
47. nuous distributions are treated similarly We first make a weighted probabilistic choice and then delay for a exponentially distributed time 350000 rrin oot 350000 300000 300000 250000 250000 200000 200000 150000 150000 100000 100000 50000 50000 0 12345 6 7 8 9 101112131415 1617181920 123 45 67 8 9 101112131415 1617181920 Figure 19 Specified left and sampled right distributions for credit card validation 26 Knapp et al Analysis From our process algebra model we obtain a finite state continuous time Markov chain represented as a matrix Q to be analysed to find the probability of being in each of the states of the model At equilibrium the probability flow into every state is exactly balanced by the probability flow out so the equilibrium probability distribution can be found by solving the global balance equation nQ 0 subject to the normal isation condition m x 1 From this probability distribution can be calculated performance measures of the system such as throughput and utilisation From this information we can assess a service level agreement for the system A service level agreement typically incorporates a time bound and a probability bound on paths through the system behaviour We considered the advantage to be gained by using the express checkout where customers in the queue have no more than 8 items to purchase As would be expected the sale is always likely to be com
48. omponent Model Component CashDeskApplication a static structure J P lt lt component gt gt a aero cb CDA CB 1 CashDeskApplication GuiR expressMode boolean false CashBoxP temCourter int 0 cdg CDA CDG 1 saleHistory SaleTO ordered O Js c0a Sit peCOAR TT fe ScannerP a il PrinterR er epacrfy i CDA I 0 1 b CDABank 1 co cbA C ty 4 CDALD IN CardReader i A ai L EN LightDisplayR CardReaderR InventoyR BankR CoordinatorR O CoordinatorP lt lt port gt lt lt port gt lt sport gt gt lt sport gt lt lt port gt CDA S CDA CR CDA C CDA Bank CDA CDG cashDeskld String transactionld String productName String s lt port gt gt products ProductvvithStockitemTO cardinfo String price double CDA CB payMode PaymentMode pin int motal double p TEPE TEE debit Debit amount double Edel caleba pos final boolean append head double tail double double CDAJ zzport gt gt CDA P lt lt port gt gt barcode long CDA LD productinfo ProductvVithStockitemTO amountEntered double saleObj SaleTO final boolean productName String price double total double changeAmount double Ssasynce gt O lt lt asynce gt O ScannerP CoordinatorR productBarcadeScannedi
49. onnected ports In the following let us consider a connection between two port declarations p P and p P occurring in components C and C respectively The connection is syntactically well defined if the operations of the required interface of A coincide with the operations of the provided interface of P and conversely To study the interaction behaviour of the two ports let Ap and Ap be the I O transition systems representing the behaviour of P and P respectively Any communication between the connected ports is expressed by synchronising output labels of one port with the corresponding input labels of the other port Hence the interaction behaviour of Ap and Ap can be formally represented by the port product Ap Ap of Ap and Ap see 10 for the definition of products A first semantic condition which should be required for a port connection is that any two port instances can communicate with each other without the possibility to run into a deadlock which means that the port product is deadlock free In this case we say that the ports are behaviourally compatible Let us for instance consider the composite component CashDeskLine cf Fig 6 which has one connector between the port CDA C of the CashDesk component and the port C CD of the Coordinator The transition system representing the behaviour of the port CDA C cf Fig 10 is shown in Fig 17 top and the transition system representing the behaviour of the port C CD w
50. operation In the other cases we must assume for the purpose of model checking later on that the impact of arguments and or results and or guards occurring on UML transitions can be resolved by a finitary case distinction which is encoded by appropriate labels Note that transitions with the invisible action 7 can occur in the behaviour specification of a port in order to model a possible internal choice of the port s owner component which is not visible at the port but may have an impact on the future behaviour of the port As a concrete example we consider the component Coordinator and the behaviour specification of its port C CD see Fig 12 The corresponding I O transition system shown in Fig 15 is directly inferred from the behaviour specification According to the given behaviour specification of the port the silent action T represents a non visible choice whether an express mode should be enabled or not saleRegistered_ tau tau saleRegistered_ _expressModeEnabled Figure 15 I O transition system for port C CD Let us now look to the behaviour specifications of simple components and their representation by I O transition systems A simple component contains a set of port declarations of the form p P mult where p is a port name P its port type and mult specifies the port multiplicity indicating how many instances of that port a component instance can have Since a component can only communicate with its enviro
51. ort properties Composite components do not show a behaviour of their own their behaviour is deter mined by the interplay of the behaviours of their contained component instances and the connections i e connector instances The ports offered by a composite component are exclusively relay ports i e the mirroring of ports from the contained components which must not be declared to be connected by some connector property As an example consider the composite component CashDeskLine showing stereo type lt component gt in Fig 6 It declares via the component properties cashDesks and coordinator components CashDesk and Coordinator as sub components where each in stance of CashDeskLine must show at least one instance of CashDesk Port property co of CashDesk is connected to port property cds of Coordinator meaning that at runtime each port instance in co of a cash desk in cashDesks is connected to a port instance in cds of coordinator The port declarations i and b of CashDesk are relayed However as in fact there may be several cash desks but there is to be only a single port in stance of CDA Bank we would have to introduce an adapter component which declares a port with multiplicity 1 to be relayed to the outside of CashDeskLine and a port with multiplicity 1 matching the multiplicity of cashDesks to be connected to the differ ent b instances of the different cashDesks We abbreviate this by using the stereotype adapters on connector
52. pect to the inventory s check if the stock is getting low for some products The check occurs cyclical after some not further specified time period x The lower region shows the direct forwarding of a product order actually to be executed Note that we do not show the message exchange related to the transactional data communication with port d For this purpose the operation calls on d would simply be framed by begin and commit transitions analogously to the port behaviour of I Data Modelling the CoCoME with the JAVA A Component Model 17 1 4 Analysis 1 4 1 Analysis of Functional Requirements For the analysis of the functional requirements we focus on the semantical properties of our CoCoME model specified by the behaviour specifications of ports and compo nents in Sect 1 3 We consider the asynchronous part of our model for the CoCoME and we will check deadlock freeness and component correctness For the synchronous information oriented part we believe that the behavioural aspects of message exchange and parallel execution which are in the centre of our interest here are not so relevant The basic idea of our approach is to proceed hierarchically starting from the analy sis of local properties of simple components and their ports from which we can then derive by a compositionality theorem properties of composite components Thus fol lowing the hierarchical construction of components we obtain results for the behaviour of the globa
53. perations are in voked These invocations leave the component s boundaries and therefore the checked exception Connect ionException has to be handled simple component CashDeskApplication 2 int itemCounter 0 port CDACB 4 provided async saleStarted async productBarCodeEntered int barcode 6 async saleFinished j async paymentModeCash 8 required void changeAmountCalculated double amount void saleSuccess 10 protocol lt behaviour states initial init 12 simple a simple b simple e simple h transitions init gt a 14 a gt b trigger saleStarted b gt b trigger productBarCodeEntered e gt h effect out saleSuccess 18 h gt b trigger saleStarted be ake b gt 20 Pran void saleStarted implements CDACB saleStarted 22 Event event Event signal send saleStarted new Object this eventQueue insert event 24 pless void processSaleStarted 26 try CDAP saleStarted 28 CDACDG saleStarted 30 catch ConnectionException e e printStackTrace Figure 22 The JAVA A simple component CashDeskApplication We have used HUGO RT to generate Java based implementations of the state ma chines to realise the components behaviour Thus the components behaviour adheres strictly to the specifications given in the previous sections However to use the spec ified state machines for code generation a few minor adoptions ha
54. pleted more quickly at the express checkout but the advantage is not as great as might be expected At the express checkout 50 of sales are completed within 40 seconds as opposed to the 44 seconds spent at a normal checkout see Fig 20 right In our model we included the possibility of customers with 8 items or fewer choosing to go to a normal checkout instead of the express checkout because we have seen this happening in practice This goes some way to explaining why the difference in the results is not larger Differences between the express checkout and a normal checkout Differences between the express checkout and a normal checkout 0 08 0 6 express checkout se express checkout normal checkout e normal checkout lt 0 07 P j3 y 0 06 a we r we 04 a gt 0 05 a l gt P amp 0 04 Pri Pl S o3b a re oe Q a 2 p uii 7 003 prag at a wi 0 2 we pono K 0 02 F F pine ot 0 1 F 0 01 ff ene a o o 0 1 2 3 4 5 6 7 8 9 10 0 5 10 15 20 25 30 35 40 45 50 Time time Figure 20 Graphs showing how the advantage of using the express checkout 8 items or fewer over using a normal checkout 100 items or fewer varies over 10 left and 50 seconds right 1 5 Tools 1 5 1 Qualitative and Quantitative Analysis HuGo RT HuUGO RT 18 is a UML model translator for model checking theorem proving and code generation A UML model containing active classes with state ma chines collaborations interac
55. r performance analysis The analysis shows that the advantage of ex press checkout is not as great as might be expected Currently however this analysis has to be performed manually a closer integration could be achieved by decorating UML state machines and sequence diagrams with rate information using the UML per formance profile as in the Choreographer design platform 17 allowing a PEPA model to be extracted from the UML diagrams Model Markovian models associate an exponentially distributed random variable with each transition from state to state The random variable expresses quantitative Modelling the CoCoME with the JAVA A Component Model 25 information about the rate at which the transition can be performed Formally a ran dom variable is said to have an exponential distribution with parameter where gt 0 if it has the probability distribution function F with F x 1 e if x gt 0 and F x 0 otherwise The mean u of this exponential distribution is p ne x e dx 1 2 Thus if we know the mean value of the duration associ ated with an activity then we can easily calculate from this the rate parameter of the exponential distribution 1 w In the case where we only know the mean value then the exponential distribution is the correct distribution to use because any other distribution would need to make additional assumptions about the shape of the expected distribution However for ex ample in the case of wa
56. re can be found on our web page 10 1 3 1 Architectural Deviations Two of the essential features of our component model are on the one hand its strict use of ports as first class citizen to encapsulate parts of component behaviour and on the other hand the distinction between component port types respectively and their instantiation These features enabled us to model some aspects of the trading system in 6 Knapp et al TradingSystermn TradingSystem CashDeskLine _ _ Store CashDeskLine CashDesk CashDesk CardReaderController CashBoxController CashDeskApplication CashDeskApplication CashDeskGUl LightDisplay Controller PrinterController ScannerController Coordinator Coordinator Ev entBus not modeled Inventory explicit functional components Enterprise and Store Application spit up into enterprise and store application Reporting Enterprise Store Store Inventory Data Enterprise Data instantiated in Enterprice Store Data instantiated in Store Persistence integrated in ports of Data GUI modelled as operator ports onl Reporting ports of Enterprise Reporting Store ports of Store inventory DataBase Figure 3 Component hierarchy of given left and modelled right architecture a more convenient way In the following we describe and justify structural deviations from the original modelling along Fig 3 On the left hand side the component hierarchy as des
57. s the component uses a relay port with multiplicity 1 and instantiates one port for each store Hence in contrast to the cash desks as part of the CashDeskLine Fig 6 the different stores of an enterprise do not share the same bank connection Store As depicted in Fig 5 the component Store is a composition of a CashDeskLine see Sect 1 3 3 an Inventory see Sect 1 3 4 and an instance of the component Data The inventory is connected to the Data instance hiding the concrete data base from the application as required in the CoCoME In contrast to the enterprise context the port e Enterprise of Data is not used when instantiating the component as part of a Store The optional operator ports of Inventory remain unconnected as we did not model explicit GUI components These would be connected to the particular ports for testing purposes in the deployed system we may also connect actual operator interfaces The component Store uses mandatory relay ports to connect to a bank component and a data base Relaying the port I PD of component Inventory is optional in order to take into account the requirements of the exceptional processes in Use Case 8 enter prise server may be temporally not available Optionality is also required for system Modelling the CoCoME with the JAVA A Component Model 9 Enterprise Bj static structure J lt component gt a Enterprise stores Store a p HPD 10 11 ed b CDA
58. see Fig 1 a describes a view on a component like particular function ality or communication the operations offered and needed in the context of this view Modelling the CoCoME with the JAVA A Component Model 3 id operations operations 7 provided Port gt Operation Interface 0 1 A gt Feature properties Property required behavior 7 0 1 gt Behavior i a Port Multiplicity Simple Element properties Component Property _ gt meee pons Pot PET pont 1 subsets Property 1 properties z operations Operation b Simple component type Component 4 Simple Composite Components Component Component Component Property relayPorts Port Property V Property 2 ports connectors Connector a Property 1 type ports Connector Port c Composite component Figure 1 JAVA A component metamodel and the mandatory sequencing of operation calls from the outside and from the inside The operations offered by a port are summarised in its provided interface the opera tions needed in its required interface The sequencing of operations being called from and on a port is described in a port behaviour
59. shown here Both ports signal the status of the sale process such as saleStarted or saleFinished and both show mostly internal choice transitions The main difference is that only the GUI port signals problems with the credit card invalidCreditCard Also besides the light display it is the GUI which is notified in case of mode switches from or to express mode Modelling the CoCoME with the JAVA A Component Model 13 CDA E port behaviour J CDA CI E port behaviour J CDA Bank EF port behaviour j i debit debitCard transactionid transactionld null i saleRegistered cashDesktd products payMode itransactionid validateCard _ cardinfo pin expressMode aleObj saus setau gt Figure 10 Behaviour of the CDA ports l C and Bank The communication with components external to the cash desk is prescribed by the port behaviour specifications for CDA I CDA Bank and CDA C shown in Fig 10 The port behaviours of CDA I and CDA Bank demonstrate our modelling of synchronous communication The behaviour of CDA C is used in Sect 1 4 1 to illustrate our formal analysis of functional requirements For a discussion on the behaviour specifications of the remaining ports CDA S CDA CR CDA P and CDA LD not relayed to the environment we refer to 10 CDA Component Behaviour Figure 11 specifies the component behaviour of the cash desk application Usi
60. that their advantage is surprisingly small In Sect 1 5 we briefly present the model checking and architectural programming tools we used for the CoCoME and finally in Sect 1 6 we summarise our results and discuss further research issues The complete model of the CoCoME can be found at 10 1 2 Component Model In the JAVA A component model components are strongly encapsulated behaviours Only the exchange of messages with their environment according to provided and re quired operation interfaces can be observed The component interfaces are bound to ports which regulate the message exchange by port behaviour and ports can be linked by connectors establishing a communication channel between their owning components Components can be hierarchical containing again components and connections In the following we briefly review JAVA A s component metamodel see Fig 1 Although being based on corresponding concepts in the UML 2 0 and in fact easily mappable we at least strive to give a more independent definition which only relies on well known UML 2 0 concepts In Fig 1 UML concepts modified by the JAVA A com ponent model are shown with a white background while unmodified UML concepts are shown with grey background We assume a working UML 2 0 knowledge 2 when ex plaining some of the specialities of our modelling notation and semantics An algebraic semantics framework for the JAVA A component model can be found in 3 Port A port
61. tions and OCL constraints can be translated into the sys tem languages of the real time model checker UPPAAL the on the fly model checker SPIN the system language of the theorem prover KIV and into Java and SystemC code The input can either be directly be given as an XMI 1 0 1 1 file or in a textual format called UTE for an example see Fig 22 In the CoCoME we use HUGO RT for two purposes On the one hand we check the deadlock freedom of connectors by translation into a model checker however as Modelling the CoCoME with the JAVA A Component Model 27 currently HUGO RT s model checking support is limited to finite state systems ab straction has to be applied manually to infinite parameter domains On the other hand we use code generation into Java for component behaviours see Sect 1 5 2 LTSA For producing the graphs of the I O transition systems used in the behavioural analysis of our model and for the analysis of component correctness and behaviour reflection of ports we have used the Labelled Transition System Analyser LTSA 12 The LTSA tool supports the process algebra FSP 12 and indeed we have defined appropriate FSP processes for most of the transitions systems used in our model for the CoCoME In this way we have expressed port products by parallel composition with synchronisation on shared labels and we have proved observational equivalence of transition systems by exploiting the minimisation procedure of LTSA
62. to as port declarations internal attributes and operations and a behaviour linking and using these ingredients Port properties like all properties are equipped with a multiplicity setting lower and upper bounds on how many port in stances of a particular type exist during runtime permitting dynamic reconfiguration As an example consider the simple component Coordinator showing stereotype lt component gt in Fig 12 Besides an internal attribute and two internal operations it declares a port property cds of type C CD with unlimited multiplicity The behaviour of Coordinator is laid down in the state machine of Fig 12 bottom right In fact as indicated by the stereotype lt orthogonal gt with tag param cd cds this behaviour description abbreviates a composite orthogonal state with as many orthogonal regions containing the given behaviour as there are currently port instances in cds Note also that the internal operation updateSaleHistory is declared to be sequential that is all calls to this operation are sequentialised Composite component A composite component see Fig 1 c groups components simple as well as composite by declaring component properties and connectors be tween ports of contained components by declaring connector properties A connector which is always binary describes the type of a connector property which links two port properties such that the ports of the connector match the ports of the p
63. ve been necessary i e calls to required port operations are delegated to internal helper operations e g 1L Of course most of the component s body is omitted here However the complete implemen tation is available online 10 12 In contrast to Sect 1 3 in the JAVA A implementation port names are written without hyphens due to Java naming conventions Modelling the CoCoME with the JAVA A Component Model 29 processSaleStarted in Fig 22 lines 25sqq and parameter values of incoming operation calls are stored in helper variables The complete JAVA A implementation of the simplified CoCoME is available online 10 1 6 Summary Our approach to modelling the CoCoME has been based on a practical component model with a strong focus on implementability and modular component wise veri fication In fact our UML based component model was originally introduced for the architectural programming language JAVA A supporting encapsulation of components by ports Based on the semantic foundations we have that our strategy for modular verification of properties of hierarchically constructed components works for the archi tectural patterns used in the CoCoME The semantic basis of our functional analysis was given in terms of I O transition systems to which we could apply standard operators for instance for information hiding thus focusing only on the observable behaviour of components on particular ports For non functional properties we us
64. ve some signal or message respectively from an input component such as the cash box and to send a corresponding notification to an output component such as the cash desk GUI or the printer Furthermore we dropped the distinction of functional and controller components within the cash desk component of the CoCoME In our approach controller compo nents such as the CashBoxController 11 e g Fig 1 6 1 6 linking the middleware and the hardware devices could be modelled with ports Modelling the CoCoME with the JAVA A Component Model wi The main structural deviation from the CoCoME requirements of the informa tion system part concerns the layered approach to the modelling of the component Inventory on the left hand side of Fig 3 The layers Application Data and GUI represented by components distinguish between an enterprise part and a store part within the component Data this distinction is manifested directly in the com ponents Enterprise and Store Within the components Application and GUI the dis tinction is between Reporting and Store The former is according to the deployment of Inventory Application Reporting on the EnterpriseServer see 11 Fig 1 6 not only part of the enterprise context but also located at the store server as part of Inventory Application However according to the use case descriptions and sequence diagrams of 11 Reporting seems actually not to be used in the store context In f

1 Modelling the CoCoME with the JAVA/A Component Model*

Contents

Download Pdf Manuals

Related Search

Related Contents