Langsec research from 1983: http://en.wikipedia.org/wiki/Communicating_finite-state_machine
In computer science, a communicating finite-state machine is a
finite state machine labeled with "receive" and "send"
operations over some alphabet of channels. They were
introduced by Brand and Zafiropulo, and can be used as a model
of concurrent processes like Petri nets. Communicating finite
state machines are used frequently for modeling a
communication protocol since they make it possible to detect
major protocol design errors, including boundedness,
deadlocks, and unspecified receptions.
The advantage of communicating finite state machines is that
they make it possible to decide many properties in
communication protocols, beyond the level of just detecting
such properties. This advantage rules out the need for human
assistance or restriction in generality.
It has been proved with the introduction of the concept itself
that when two finite state machines communicate with only one
type of messages, boundedness, deadlocks, and unspecified
reception state can be decided and identified while such is
not the case when the machines communicate with two or more
types of messages. Later, it has been further proved that when
only one finite state machine communicates with single type of
message while the communication of its partner is
unconstrained, we can still decide and identify boundedness,
deadlocks, and unspecified reception state.
It has been further proved that when the message priority
relation is empty, boundedness, deadlocks and unspecified
reception state can be decided even under the condition in
which there are two or more types of messages in the
communication between finite state machines.
Boundedness, deadlocks, and unspecified reception state are
all decidable in polynomial time (which means that a
particular problem can be solved in tractable, not infinite,
amount of time) since the decision problems regarding them are
nondeterministic logspace complete.
Communicating finite state machines can be the most powerful
in situations where the propagation delay is not negligible
(so that several messages can be in transit at one time) and
in situations where it is natural to describe the protocol
parties and the communication medium as separate entities.
--
http://www.subspacefield.org/~travis/
Split a packed field and I am there; parse a line of text and you will find me.
pgpi68X8wP8pQ.pgp
Description: PGP signature
_______________________________________________ langsec-discuss mailing list langsec-discuss@mail.langsec.org https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
