Bodin E.pdf112.8 KB

The work is devoted to an attempt to use Golang programs for the specification and verification of distributed systems. The A.P. Ershov Institute of Informatics Systems, SB RAS, has been developing this approach for years. A distributed system described in terms of an SDL specification, which is first translated to...

main.pdf372.01 KB

Bodin has applied SPIN to solve puzzles like the Japanese river puzzle, an advanced version of the famous wolf-goat-cabbage puzzle. Defining a Promela model can become cumbersome and debugging can be very time-consuming, since SPIN does the syntax check (e.g. type checking) only at runtime and developers might have decided...