A formal method of developing elevator group controllers based on S-ring and SPIN

We propose a formal method of developing elevator group controllers. In this method, we use a simplified elevator system model, called S-ring, to mathematically describe a group controller and its requirements. We also utilize a model checking tool, called SPIN, to exhaustively check whether the group controller satisfies the requirements. We give two application examples and illustrate the effectiveness of our method.