• DocumentCode
    256783
  • 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
  • fYear
    2014
  • fDate
    7-10 Oct. 2014
  • Firstpage
    178
  • Lastpage
    181
  • 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;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Consumer Electronics (GCCE), 2014 IEEE 3rd Global Conference on
  • Conference_Location
    Tokyo
  • Type

    conf

  • DOI
    10.1109/GCCE.2014.7031135
  • Filename
    7031135
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=256783