Lego Mindstorms
Here are some pictures of a device that does the “Tower of hanoi” for a small stack of CDs.
Here is a short movie showing the device in action.
Fischertechnik
Some time ago, Alexander Schmidt and I built a small elevator model. It was controlled by a small Esterel program. The output of the Esterel compiler was automatically transformed into code for a BASIC stamp controller.
The generated code is amenable to formal verification. In contrast to many elevator verification case studies in the literature, it is in general not true that the elevator will serve every request.
We wrote a short paper about this: