Harnessing rCOS for Tool Support—The CoCoME Experience - Formal Methods and Hybrid Real-Time Systems - page 102

identified components. This then transforms the model of the use case contracts
into a logical component architecture as shown in Fig. 11. The rCOS specification
of the refined component SalesHandler can be given as
component SalesHandler required interface ClockIf

{ date() }

required interface BankIf { authorize(..) }

required interface StoreIf { update(..), find (..), addSale(..) }

provided interface SaleIf }

protocol { ( [ ?enableExpress ( ?startSale (?enterItem) ( max ) ? finishSale ?cashPay) ∗
|

{ startSale, enterItem, finishSale , cashPay, cardPay

?disableExpress ( ?startSale (?enterItem) ∗ ? finishSale
[?cardPay ?cashPay ] ) ∗ ]) ∗

| }

class Cashdesk implements SaleIf
This notation thus combines aspects of an rCOS component (provided/required
interface and class implementing the provided methods) and contract (proto-
col). Call-ins in the protocol are indicated by a question mark. A process can be
recognized by a protocol which starts with a call-out, denoted by an exclama-
tion mark following the method name. Further decomposition of the component
Inventory into the three layer architecture consisting of Application ,
data representation component Store and Database is shown in Fig. 12.
Notice that in the logical component models, interfaces are object-oriented inter-
faces, meaning that the interactions are through direct object method invocations.

Detailed Design. In the detailed design, refinement translates the specifica-
tions in the logical design into an object-based programming language resembling
Java. In this step, class decomposition, refactoring [12] and data encapsulation,
that proved as refinement rules in the object-oriented rCOS [14], can be applied.

enableExpress( )
disableExpress( )
startSale( )
enterItem(Long,Long)
finishSale( )
cashPay(Double,Double)
cardPay(Card)

<< Light >>

CheckOutIf LightIf

<< SalesHandler >>

:CashDesk
mode: String
enableExpress( )
disableExpress( )
startSale( )
enterItem( )
finishSale( )
cashPay( )
cardPay( )

sale

1 1

:Sale
complete: Boolean
total: Double
date: Date

date( )

1

<< Clock >>

1
0..1

pay

:Payment

valid( )

1

line

<< Bank >>

*

:CashPa y ment
amount: Double
change: Double

:LineItem
barcode: Long
quantity: Long
subtotal: Double

:CardPa y ment
card: Card

lines

*

CashDeskIf

OrderIf

<< Inventory >>

SupplierIf

:Item
barcode: Long
price. Double
amount: Long

cat

ManageIf

:Store

<<Supplier>>

1 *

Fig. 11. The logical component-based model