Introducing input-output into LTS

There are different ways of introducing the notion of input and output interactions into the formalism of LTS.

Role of interaction parameters

The LOTOS language (see C ) uses rendezvous communication, where interactions may have parameters. Each participating component may impose constraints on the acceptable parameter values. As an example, we consider two processes A and B that communicate over a joint port called P by the joint interaction g (integer par) which has one parameter of integer type. We consider different cases:

  1. Nondeterministic value creation: In this case of a simple rendezvous, a common value will be created nondeterministically
  2. Value constraints: both parties may impose constraints on the values of interaction parameters
  3. Value passing: one party has no contraint, the other imposes a particular value to the parameter

It is clear that in case 3, the parameter of the interaction g is output for component A and input for component B.

Informal distinction of input and output

The designer chooses names for the interactions that implicitly indicate whether the interaction is input or output.

Formal notation for distinguishing input and output for rendezvous communication

Because of the above difficulty, several people have introduced a formal notation for distinguishing input and output, but retaining the communication primitive of rendezvous, that is, the input and output operations are performed by the participating components as a single, atomic action. Examples of such notations are the following:

Important note: Here it is assumed that interactions are always rendezvous, that is, both parties must be ready to participate in the rendezvous.

Considering interactions as events

In UML, the concept of an events is widely used. An event is an action that happens. It is usually triggered by some process, and handled by another process (that is, the latter performs some processing that is appropriate for taking this event into account). In a typical state machine defined in UML, an input to a state machine is an event (it is initiated by some process in the environment of the machine), and the machine will handle the event by performing a corresponding state transition (defined by the state machine model).

Based on this semantics of interactions, one can say that for each interaction:

It is important to note that the question whether an output will be produced by the outputting component is solely determined by that component, and not by the component that receive that output as input.

There are two underlying semantic models:

Completely defined state machines

Definition: A state machine, e.g. LTS, is completely defined if in each state there is a transition for all transition labels that are part of the alphabet of the state machine. Otherwise, it is called a partially defined state machine.

A completely defined machine accepts in each of its states, all interactions. An LTS is normally not completely defined. Two completely defined LTS will never deadlock when they communicate.

Definition: An IOA or a CFSM is completely defined if in each state there is a transition for eqch inputs in the input alphabet of the machine.

IOAs are often considered to be completely defined, however, this represents in many case an overspecification. In hardware design one talks about don't care condition for the output of a component for certain input values. It means, it does not matter what the output would be - the output is not specified for those input values.

In component-based system development, one knows normally what kind of components are used in the environment of a given system component. Therefore the behavior of the environment is known, and it can be predicted that certain inputs to the given component will not be produced by the envirnment when the given system is in certain states. Therefore it would be an overspecification if one would define the required state transitions for handling such inputs in those states.

This leads one to consider that the specification of a components includes assumptions about the environment and guarantees about the (output) behavior of the given component (but only for the case that the environment follows these assumptions). See specification with assumptions and guarantees.

Specifying assumptions and guarantees with partially defined input-output state machines

Semantic model for partially defined input-output state machines: The states and transitions specified in the model define the guarantees about the behavior of the component that is specified. For each state of the model, it is assumed that the inputs for which there is no transition defined from this state will not occur during the execution of the system where the component is used. In case that such an input occurs in some exceptional situation, the behavior of the specified component is not defined - it may react arbitrarily, possibly going to a blocked state.

Verification of component-based designs: With this semantic model, when a component-based system is designed, it is important to verify that the assumptions made for each component are satisfied by the behavior of the components in its environment.

Verification algorithm: Similar to the Algorithm for checking trace inclusion, one completes the specification of the component behaviors by introducing a state Fail for each component, and then one performs reachability analysis. If any of the reachable states includes the Fail state of any of the involved components, there is a unspecified-reception design fault.

Example (the same as used for LTS reachability): Which interactions are input/output for A1 and A2 ? - To be selected, and reachability analysis to be adapted.

two LTS product

Reachability analysis considering the possibility of unspecified reception

Reachability analysis for IOA is in some sense similar as for LTS. Here transitions are labelled !m (output of the message m) or ?m (input of the message m). Transitions that have labels containing the same message are performed jointly.

However, there is one very important difference: Whether an output transition is performed is decided by the outputting component alone. If the component that should receive the message is in a state where it does not have an input transition for this message, one encounters a non-specified reception situation (which can be interpreted in different ways - see discussion). Note that similar situations for interacting LTS sometimes represent deadlocks (no transition is possible for the global system).

If Ii is the set of input messages of a component Ci, and Oi is the set of its output messages, we assume that Ii intersection Oi is empty and we define the alphabet Ai = Ii union Oi. In a composition, a given message may be output only for one component; but it may be input to several components (for instance, it may be output generated by the environment and be input to several components). We assume here that all messages between two components are also visible to the environment; this means that an interaction that is output by one component is also an output from the composition to the environment. Note: A hiding operation for the inter-component messages may be performed after the reachability analysis.

The composition of two IOA models, C1 and C2, with alphabets A1 = I1 union O1, and A2 = I2 union O2, respectively, can be modeled by a global IOA that represents the behavior of these two component IOA and their interactions, in the following called C. The model of C is the following IOA (Note: rules (1) and (2) are the same as for LTS):

  1. The states of C are of the form <s1, s2>, where s1 is a state of C1 and s2 is a state of C2.
  2. The initial state of C is the set of states <s1-initial, s2-initial> where si-initial are initial states of Ci (i = 1, 2).
  3. The transitions of C from a state <s1, s2> are the following:

Created: September 22, 2014