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

:Sto re :Product

:Cashier :CashDesk

s a le :Sa le

:Clo c k

startSale( )

date( )

li:Lin e Ite m

New( )

loop

en terItem(co d e,q ty )

find(code)

find(code)

New(code,qty)
setSubtotal( )
a d d Lin e (li)

fin is h Sale( )

setComplete( )
total( )

Alt

cashPay(amount,change)

getTotal( )
makeCashPay(amount,total)

:CashPayment

New(amount,change)
getChange( )
addSale(sale)
updateInventory(code,qty)

update(qty)

cardPay(card) :Ba n k

authorize(card,amount)

makeCardPay(card)

:CardPayment

updateInventory(code,qty)

addSale(sale)

update(qty)

Fig. 10. Design Sequence Diagram of Process Sale

thus model checking and simulation can be easily applied. The state diagram allows
verification of both safety and liveness properties.
As all three specifications mechanisms are based on regular techniques and can
be interpreted as defining languages of traces, we translate them manually into
CSP specifications and use the FDR model checker to prove trace equivalence
of the sequence and the state diagram. Likewise, we can generate PROMELA
specifications for the SPIN model checker to check additional properties such as
certain liveness or application specific properties.

Logical Design. The logical design step has two kinds of activities. First each
use case contract is refined from its functional specification through application
of design patterns, the Expert Pattern [9] in particular. This step delegates the
functionality responsibilities to the internal domain objects (i.e. those of the
fields). This derives a refinement of the use case sequence diagram into a design
sequence diagram . For example, applying the expert pattern to the use case
operation of UC1 we can refine it to the design sequence diagram shown in
Fig. 10. We can specify the other use cases and refine them in the same way. For
the formal refinement of the use cases in rCOS, we refer the reader to the rCOS
solution to CoCoME [8].
After the initial object-oriented refinement we can identify further compo-
nents. For use case UC1 ,wesingleoutthecomponent Clock and Bank
from the component SalesHandler . We also compose the use cases for “or-
der products”, “manage inventory items”, “produce sales reports” and “pro-
duce stock reports” into one component called Inventory . From the design
sequence diagrams of the use cases (and formally the refined design of the use
case operations specified in rCOS), we can organize the interaction among ob-
jects from the different components into provided and required interfaces of the