Design in CommUnity with Extension Morphisms - Formal Methods and Hybrid Real-Time Systems - page 463

get_pay [get_g, s_nickle, s_dime, s_quarter, s_dollar, s_cent]:
get_g, false -> get_g' = false ∧ s_nickle' = s_nickle + i_nickle
∧ s_dime' = s_dime + i_dime ∧ s_quarter' = s_quarter + i_quarter
∧ s_dollar' = s_dollar + i_dollar ∧ s_cent' = s_cent + i_cent
Notice that we need to add a new channel s_cent into the slot component to store
the cents and make the corresponding assignment to this channel. However, based on
the definition of extension morphism, there will exist an extension morphism from the
old component to this extended component (the proof is similar to the case above).
For the same reason, we can modify the following actions of the slot component as
well (and add the channel o_cent):
send_pay [get_g, o_pay]:
¬ get_g , false -> get_g' = true ∧ o_pay' = 100*i_dollar +
25*i_quarter + 10*i_dime + 5*i_nickel + i_cent
send_change [change_g]:
¬ change_g, false -> change_g' = true ∧ ( change_res = true ⇒
item_g' = true ∧ s_nickle' = s_nickle - o_nickle ∧ s_dime' =
s_dime - o_dime ∧ s_quarter' = s_quarter - o_quarter ∧
s_dollar' = s_dollar - o_dollar ∧ s_cent' = s_cent - o_cent)
Since we have divided the functionality of the system in an appropriate way, we
can simply reuse the vending machine subsystem and the controller component.
4 Conclusions
Extension morphisms were originally motivated by their use in the application of
aspects [8]. The examples developed in [8] were related to the application of a moni-
toring and a performance aspect to an unreliable communication system. We would
like to impose behaviour on the existing architecture of an unreliable medium be-
tween a sender and receiver, to make the communication reliable by implementing a
reset in the communication when packets are lost. The mechanism we used was very
simple, and required a “reset” operation in the sender, which can be achieved by
component extension. In order to complete the enhanced architecture to implement
the reset acknowledgement mechanism, we need a monitor that, if it detects a missing
packet, issues a call for reset. The idea is that, if a message is not what the monitor
expected, then it will go to a “reset” cycle, and wait to see if the expected packet ar-
rives. If the expected packet arrives, then the component will start waiting for the next
packet. (Note that, since the superposed monitor is spectative , i.e., it has no effect on
the underlying component - simply “observing” it.) Because of the properties of ex-
tension, we can guarantee that, if the augmented system works without the need for
reset in the communication, i.e., no messages are lost, then its behaviour is exactly the
same as the one of the original architecture with unreliable communication.
As we hope to have demonstrated in this paper, extension morphisms have a life of
their own, independently of their usefulness in defining some aspects. They provide
an interesting and predictable mechanism for software architects interested in change
and evolution of their designs.