Title :
Éclair: An elevator group controller model checking system based on S-ring and SPIN
Author :
Nagafuji, K. ; Yamaguchi, S.
Author_Institution :
Grad. Sch. of Sci. & Eng., Yamaguchi Univ., Ube, Japan
Abstract :
We developed a model checking system for elevator group controllers, named Éclair. Éclair can perform model checking of a given S-ring model by invoking SPIN. In this paper, we described how to convert the S-ring model into a SPIN´s input model. We also showed the test capability of Éclair from the viewpoint of scalability.
Keywords :
control engineering computing; formal verification; lifts; Éclair test capability; S-ring model; SPIN input model; elevator group controller model checking system; Data models; Elevators; Floors; Model checking; Scalability; Servers; Shafts;
Conference_Titel :
Consumer Electronics (GCCE), 2014 IEEE 3rd Global Conference on
Conference_Location :
Tokyo
DOI :
10.1109/GCCE.2014.7031135
