Formal Modelling and Visualization of Elevator System Based on Event-B
- Resource Type
- Conference
- Authors
- Yao, Ju-Yi; Zou, Sheng-Rong; Geng, Xue
- Source
- 2022 IEEE 2nd International Conference on Computer Systems (ICCS) Computer Systems (ICCS), 2022 IEEE 2nd International Conference on. :123-130 Sep, 2022
- Subject
- Computing and Processing
Visualization
Computational modeling
Reliability theory
Animation
Set theory
Reliability engineering
Elevators
Formal method
Event-B
ProB
- Language
When designing complex systems with high security requirements, it is essential to use reliable formal modeling methods to verify whether the resulting system is what the designer wants. This paper presents a case study of an elevator system based on Event-B and Rodin platform. Event-B method is a formal modeling method based on set theory and predicate logic. Its main features are layer by layer refinement and theorem proof. Event-B is supported by Rodin platform. We use ProB to perform animation simulation and model check on the machine to ensure the correctness and effectiveness of the model. Finally, BMotionWeb is used to visualize the model to further enhance the model's comprehensibility and interactivity, so that designers can find hidden errors more quickly.