| Presentation | 2022-03-28 Formal Verification of Control Policy of Elevator Systems using Statistical Model Checking Yuki Kitahara, Masaki Nakamura, Kazutoshi Sakakibara, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | When designing an elevator system, efficient control laws can be expected to be obtained by considering the probability distribution of passenger occurrence. UPPAAL SMC is a Statistical Model Checking tool based on stochastic time automata that can handle time constraints and stochastic transitions. UPPAAL SMC can perform statistical analysis on models that include stochastic events through scenario-based simulation. In this study, we examine the design formal verification of elevator control law using UPPAAL SMC, a Statistical Model Checking tool that can handle time constraints and stochastic transitions. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Elevator / MCE / Model Checking / Statistical Model Checking / UPPAAL |
| Paper # | MSS2021-57,NLP2021-128 |
| Date of Issue | 2022-03-21 (MSS, NLP) |
| Conference Information | |
| Committee | MSS / NLP |
|---|---|
| Conference Date | 2022/3/28(2days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | Online |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | MSS, NLP, Work In Progress (MSS only), and etc. |
| Chair | Atsuo Ozaki(Osaka Inst. of Tech.) / Takuji Kosaka(Chukyo Univ.) |
| Vice Chair | Shingo Yamaguchi(Yamaguchi Univ.) / Akio Tsuneda(Kumamoto Univ.) |
| Secretary | Shingo Yamaguchi(Hokkaido Univ.) / Akio Tsuneda(NEC) |
| Assistant | Masato Shirai(Shimane Univ.) / Hideyuki Kato(Oita Univ.) / Yuichi Yokoi(Nagasaki Univ.) |
| Paper Information | |
| Registration To | Technical Committee on Mathematical Systems Science and its Applications / Technical Committee on Nonlinear Problems |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Formal Verification of Control Policy of Elevator Systems using Statistical Model Checking |
| Sub Title (in English) | |
| Keyword(1) | Elevator |
| Keyword(2) | MCE |
| Keyword(3) | Model Checking |
| Keyword(4) | Statistical Model Checking |
| Keyword(5) | UPPAAL |
| 1st Author's Name | Yuki Kitahara |
| 1st Author's Affiliation | Toyama Prefectural University(Toyama Pref. Univ.) |
| 2nd Author's Name | Masaki Nakamura |
| 2nd Author's Affiliation | Toyama Prefectural University(Toyama Pref. Univ.) |
| 3rd Author's Name | Kazutoshi Sakakibara |
| 3rd Author's Affiliation | Toyama Prefectural University(Toyama Pref. Univ.) |
| Date | 2022-03-28 |
| Paper # | MSS2021-57,NLP2021-128 |
| Volume (vol) | vol.121 |
| Number (no) | MSS-443,NLP-444 |
| Page | pp.pp.13-18(MSS), pp.13-18(NLP), |
| #Pages | 6 |
| Date of Issue | 2022-03-21 (MSS, NLP) |