A formal method of developing elevator group controllers based on S-ring and SPIN. - Shingo Yamaguchi 001; Kazuya Nagafuji (GCCE, 2013)

Éclair: An elevator group controller model checking system based on S-ring and SPIN. - Kazuya Nagafuji; Shingo Yamaguchi 001 (GCCE, 2014)