Protocols define the communication (what and when) between different parts of a system. Protocols can be stateful or stateless (e.g. TCP vs. UDP). Stateless protocols are very simple to model: there’s a start state, in which the part waits for an incoming message. This is the only state that takes inputs. Upon reception, there might be several transitions depending on the message received. The message processing can also be expressed as FSMs (without any input), and typically they either end in an error state or come back to the start state to accept the next input. In stateful protocols, the FSM is more complex, since inputs can be received in multiple states that capture the state of the protocol. For example a server in the TCP start state won’t accept any data transmissions.
To store the FSM that models side A of the protocol, I will use the following two relations
StartState(A, state) // This relation only contains one entry
Transitions(A, from-state, input, to-state, effects)
The states could just be denoted by integers. The input message type, which in the most naive implementation just enumerates all possible messages, could also be a regular expression to avoid the state explosion that is exponential in message size. Effects describe interactions of the part with the rest of the system, for example sending messages, printing to screen, logging etc. They’re executed upon entering the state they’re associated with.
I’ll use prefixes A and B to denote the FSMs of nodes A and B, in a symmetric protocol they’ll point to the same relations. Furthermore, the only effect considered is sending messages, and all transitions are transformed so that they receive or send a message:
Transitions(ASMTN), Transitions(AT U ) => Transitions(ASMUN)
Transitions(ASMTN) => Transitions(ASMZ ), Transitions(AZ TN)
Now we can express reachability in Datalog as follows:
reachable(SSUU) :- StartState(A, S), StartState(B, U)
reachable(SZUV), reachable(ZTVV) reachable(SZUU), reachable(ZTUV)
reachable(SSUZ), reachable(STZV) reachable(STUZ), reachable(TTZV)
Transition(AS TN), Transition(BUNV ) Transition(ASMT ),
With that, we can verify all safety properties (something bad never happens) that can be expressed as a combination of bad states. For example, we can express that B never reaches an error state, that A and B can’t be simultaneously in a critical section or that no deadlock happens. All properties hold if the queries return an empty result table:
● ?- reachable(STUV), StartState(A, S), StartState(B, U), isError(B, V)
● ?- reachable(STUV), StartState(A, S), StartState(B, U), isCriticalSection(T, V)
● ?- reachable(STUV), StartState(A, S), StartState(B, U), isBlocked(A, T), isBlocked(B, V)
Liveness properties (something good eventually happens) are much harder to capture, because they involve a notion of failures and time. Even with a better model (e.g. augment the Transitions table with time-outs, model the network as FSM with failures), we’re subject to some impossibility results like the halting problem, CAP and FLP .