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.