
Foundations of Compositional Model-Based System Designs 109
Client Server
Request
Response
Time-out
Request
×
msg lost
Request!
Response?
Client
Request?
Response!
Server
(a)
(b)
FIGURE 4.13 (a) Scenario for a simple client/server application described as a message sequence chart.
(b) State machines for the client (top) and server (bottom).
The two notations shown in Figure 4.13, the MSC, on the one hand, and the two state machines,
on the other hand, constitute two different views of the client–server system. We would like to ensure
that these two views are consistent with each other. Let us see how we can use the formal framework
mentioned earlier to check whether ...