Mathematical Model

This model views the CAETI system as sequences of CAETI messages being exchanged by processes that are attached to bi-directional connections. A connection is a logical communication path that is identified by a pair of CAETI addresses. (A process may be attached to more than one connection.) There is a mapping from the sender and receiver parameters of messages into CAETI addresses.

Message Traffic.

The message traffic at a CAETI address is modeled as two independent sequences of CMA messages. One is the sequence of all inbound messages that have arrived at the address, and the other is the sequence of all outbound messages that have been sent from the address.

The traffic for a particular address a can be modeled as an ordered pair (x,y) where x is the inbound message sequence, and y is the outbound sequence. Every CAETI address is unique. At any given moment, only some of these addresses will be in use by CAETI processes. Therefore, the CAETI system is modeled as a mapping from CAETI addresses into the pair of inbound and outbound CAETI message sequences that have occurred at that address as follows:

 CAETI-system = { (a, (x, y)) }

where

a is an address in use by a CAETI process,
x is the sequence of messages inbound through address a,
y is the sequence of messages outbound through address a,

Because every CAETI address is unique, CAETI-system is a mapping from CAETI addresses into pairs of CMA message sequences.

Address Mapping.

There is a function address-map(a) that maps CAETI addresses into the sender and receiver parameters (which are ASCII strings). There is also an inverse function un-map(s) that maps these strings back into CAETI addresses. These functions have the property

 All a:a-caeti-address, un-map(address-map(a)) = a

The CAETI Message Type.

Field accesses into the record structure give the value of each message parameter.

 type a-CMA-msg =
  record (kind : a-CMA-type;
          sender : a-caeti-address;
          receiver : a-caeti-address;
          content : string;
          language : string := "text";
          ontology : string;
          reply-with : string;
          in-reply-to : string);

Message Types.

The allowed types of CMA messages are recognized by the relation is-CMA-msg(m) as follows:

 type a-CMA-msg = enum [ tell, ask, do subscribe, sorry ];

Outbound Messages.

This model assumes that every message sent from a CAETI address must be a CMA message. No other kinds of messages may be sent from a CAETI address. It also assumes that the sender parameter of every CMA message correctly identifies the CAETI address from which it was sent. In particular, every message m in the sequence of outbound messages y from address a has the following properties:

 a-CMA-msg(m) & address-map(sender(m)) = a

Inbound Messages.

This model assumes that if a message arrives at a CAETI address, then it arrives at the address identified by its receiver parameter, it was sent from the address identified by its sender parameter, and it was not modified in transit. In particular, every message m in the sequence of inbound messages x at address a has the following properties:

 address-map(receiver(m)) = a & occurs-in(m, outbound(CAETI-system,a))

where

 outbound(s,a)

is the function that gives the outbound sequence y that is associated with address a in system s, and

 occurs-in(m,y)

is true iff message m occurs somewhere in the message sequence y.

Because every inbound message must be some outbound message, every outbound message of interest will be a CMA message.