Formal Modelling and Visualization of Elevator System Based on Event-B
Ju-Yi Yao, Sheng-Rong Zou, Xue Geng · 2022
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.