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

:Cashdesk

Cashier

enableExpress()

loop

[*]

disableExpress()

alt

[not(ExMode)]

enableExpress()

complete
¬ExMode

startSale() startSale() startSale() startSale()

loop

[*]

startSale()

¬ExMode ExMode complete

ExMode

loop

[1..max]

enterItem(Barcode, Quantity)

finishSale()

cashPay(Amount, Amount)

¬c om ple te
¬ExMode

¬c om ple te
ExMode

[ExMode]

disableExpress()

loop [*]

startSale()

complete
ExMode

complete
¬ExMode

loop

[1..*]

enterItem(Barcode, Quantity)

finishSale()

alt

cardPay(Card)

enterItem(Bar c ode, int)

enterItem(Barcode, int)

<max

cashPay(Amount, Amount)

*

¬c om ple te
¬ExMode

¬c om ple te
ExMode

Init

finishSale()

finishSale()

Fig. 6. Sequence Diagram Fig. 7. State Diagram

The model of logical design should be further refined by class decomposition,
data encapsulation and refactoring. We call this step the detailed design .The
detailed design also involves replacing the object-oriented interfaces with con-
crete and appropriate interaction mechanisms (or middlewares) such as RMI,
CORBA or shared event channels.Verification and validation, such as runtime
checking or testing (unit testing), can be applied to components before and after
introducing the concrete middlewares.
Code can be constructed for each component and static analysis, unit testing
and runtime checking can be done on the components.
Before or after coding, the design of the GUI, the software controller of the
hardware devices and their interactions with the application software compo-
nents can be modeled and designed. This is done in a purely event-based model
following the theory of embedded system design. The business components, GUI
components, hardware controllers and middlewares are integrated and deployed.

Requirements Modelling of POST. A use case is modelled as a contract
of a component, that corresponds the concepts of use case controller class in
our earlier object-oriented modelling [7]. To help practical software engineers to
understand the formal models, the protocol of a use case contract is illustrated
by a UML sequence diagram that defines all the possible traces of the interaction
between the actors and the system in the use case. The guarded design speci-
fication of each interface method is further divided into the guard, the control
state transition, and the data functionality. The guards and the control state
transitions are shown by a UML state diagram, and the data functionality of a