For the specification of the behavior of a component that has several interfaces, it is useful to subdivide this specification into the following aspects:
These ideas were first presented in my early papers on protocol specifications (survey, general transition model, protocol specification for OSI) and a more general paper with Raynal (Bochmann, G. v. and Raynal, M., Structured specification of communicating systems, IEEE Trans. Computers C-32, 2(Febr. 1983), pp. 120-133.). The description of the interface constraints for component-based system design is also discussed in a paper with Braek (Service discovery and component reuse with semantic interfaces ( R. T. Sanders, R. Braek, G. v. Bochmann and D. Amyot ) Proc. of the SDL Forum, Norway, July 2005, Springer Verlag, LNCS 3530, pp. 85-102.).
When we discussed reachability analysis, we considered the composition of arbitrary behaviors. Communication services may also be defined by formal models. In my paper on Finite State Description, I used a state machine model to represent a simple communication link between the two communicating protocol entities. Such a service has (at least) two interfaces (for the two communicating entities) and each of its states corresponds to certain messages that are in transit; the initial state being the "empty" state (no message is transit), and the transitions correspond to the message send and receive operations.
A more complex communication services have been defined in the OSI standardization work. As discussed in the introduction to this course (communication architecture), it is important to define the desired communication service before designing the protocol that is intended to provide this service. When the TCP protocol was designed (in the later 1970ies) the designed had the intuitive understanding of the desired communication service, namely the dynamic establishment of connections over which data transfer is reliable. However, this service was never formalized. In the context of the subsequent OSI standardization work, the OSI Transport service was defined as a formalization of the intuitive notion that had been around for long time. I discussed the formalization of communication services (and the relation to the corresponding protocol design) in my paper "General transition model ...".
It is important to note that the behavior of communication services are in general (with some little exceptions) concatenation-invariant - this means that if one concatenates two services together by connecting two of their interfaces (as shown below), then one obtains a global service that has the same functional behavior. An example is the communication service that behaves like a FIFO queue; one may say that a queue is a very basic "communication service" (what is entered on one side comes out at the other end). Two concatenated queues still have (globally) the behavior of a FIFO queue.
Clearly the non-functional properties are not invariant - for instance, the transmission delay adds up, while the maximum throughput of the composition is the minimum of the two maximum throughputs. For a detailed discussion see my paper from 1990 on communication gateway design and deriving protocol converters C.
There are examples of communication service features that are not concatenation-invariant. Below are three types of acknowledgement features. They are the following (the numbers indicate in which order the different service primitives are executed): (A) local acknowledgment that data was received by the service, (B) acknowledgment that data was sent and was received at the destination (by the communication service destination implementation), and (C) acknowledgement that the data was received by the destination user (who provides an explicit acknowledgement interaction with the service.
The lower part of the figure shows the concatenation of these three types of acknowledgement services. Note that the concatenation is normally implemented in the form of a communication gateway (shown as rectancular boxes). We can see from the structure of the gateways that the type A and type C acknowledgement services are concatenation-invariant, but type B is not (its acknowledgement service response only assures that the data has arrived at the gateway, but nothing can be confirmed about the reception at the destination).
In an early paper, Zafiropulos and West (1980) describe a tool to be used by a protocol designer. This designer will develop the behavior of two (or more) state machines interactively by introducing sending transitions from the different states of the machines. The tool will determine automatically in which state (or states) of the destination machine each output message could be received. These receptions are indicated by the tool, and the designer has to select the state that should be entered after the reception of the message (either a state that already exists, or a new state for the machine in question). Thus, all possible receptions must be handled by the designer and the resulting design will have no non-specified receptions. Deadlocks were also detected by the tool - they can be resolved by introducing an output transition in one of the machine states involved in the deadlock - but this is not necessarily a good solution (one may also change the earlier behavior of one of the involved state machines).
In an early paper, Gouda and Yu (1984) describe a method for avoiding non-specified receptions that are due to competing initiatives. Competing initiatives are situations where different actors in the distributed system take different initiatives simultaneously (a general discussion of such situations was given in On the realizability of collaborative services ( H. N. Castejòn, G. v. Bochmann and R. Braek ), Journal of Software and Systems Modeling, Vol. 10 (12 October 2011), pp. 1-21.). Examples of such situations are the problems encountered when the two sides start an initiative while the design of the protocol has only considered the case that such an initiative happens on one side at any given time (see examples "another example", the communication protocol discussed at the end of this page).
Gouda starts out with a state machine for one side of the protocol (where each transition either sends a message or receives a message). The states of a state machine are classified as follows: A state is an input state if all transitions starting in this state are input transitions; similarly for output states. States with input transitions and also output transitions are called "mixed".
He then proposes to construct an initial version for the behavior of the other side by exchanging input and output operations. These two machines will then communicate with one another by the exchange of messages (no message loss is assumed). Assuming that the original machine has no mixed state, Gouda's paper then shows that these two state machines work correctly with one another - that is, they are in the same respective state when no message is in transit, and there are no non-specified receptions, nor any deadlock (unless there is a state in the original specification without any transition - a kind of final state).
Then the paper notes that a mixed state corresponds to a situation of competing initiatives. Both sides can send a message, and these output transitions will go in most cases to different states. This leads in general to non-specified receptions. The paper proposes the following design methods to solve such problems:
Further explanations: example in slides 29 etc. in Concordia-Tutorial R and original paper from 1984 C.
The following problem is considered, also called equation solving: A component MA of a system is given, and the behavior of the component MB is to be found such that both components (interacting over the internal interfaces IC ) have a behavior that satisfies the requirement specification MC (which is a given behavior).
This method was first proposed by Merlin and Bochmann for the design of communication protocols (but it was never really used for this purpose). Later, it was independently proposed by Ramadge and Wonham for solving the problem of controller design. It was also used for the design of communication gateways. (For more details, see slides) While the solution to this problem was first described for system behaviors specified by state machines, I recently showed that the formulation of this problem in logic leads to much simpler proofs of correctness,a nd this for different types of communication beween the components involved.
Completely rewritten: February 10, 2013