Name
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. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1109/GCCE.2014.7031135 | GCCE |
Keywords | Field | DocType |
control engineering computing,formal verification,lifts,éclair test capability,s-ring model,spin input model,elevator group controller model checking system,servers,elevators,scalability,model checking,data models | Data modeling,Spin-½,Model checking,Computer science,Server,Parallel computing,Elevator,Group controller,Scalability,Embedded system | Conference |
Citations | PageRank | References |
0 | 0.34 | 3 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Nagafuji, K. | 1 | 2 | 0.87 |
| Yamaguchi, S. | 2 | 12 | 7.14 |