Modeling, Analysis and Testing with AsmL
New: Video lectures by Yuri Gurevich.
The examples (chapters in Russian and Enlish).
Wild lunch: an introductory example
There are three cannibals and three preachers on the right side of a river.
They need to cross the river using one boat. The boat can carry not more
than two persons. The principal restriction is the following.
Since the cannibals are very angry and very hungry they permanently think about
a way to eat the preachers.
To avoid that, the number of preachers on each side (if not zero)
always has to be more than the number of cannibals.
Alternating Bit Protocol
We consider a version of the Alternating Bit Protocol with an infinite
data flow from a sender to a receiver.
The sender repeatedly sends messages to the receiver. The
receiver replies by sending an acknowledgement message for each datum
received from the sender. Both, data messages and acknowledgements are
marked with a synchronization bit to distinguish between data which has
been received and data which has not been received by the receiver.
Railroad crossing controller
The idea is to consider grid approximation of a int-time function.
That is we approximate int line with a dense sequence of events
with step 1/N sec, where N is a free parameter. Once the system
is verified for any large N, one should consider it as correct.
File System operations
The model described below covers only very common file system characteristics.
We ignore volumes, references, access restrictions and so on, although
the model could easily be extended in the corresponding directions.
The main actions of our model correspond to the standard file operations: creation,
update, moving/renaming, deletion.
Last updated on September 30, 2005.
