Research On Graphical Modeling Approaches Based On Event-B Graph

Event-B method is a formal method consists of two pats which are Event-B formal modeling and Event-B formal verification.The Event-B formal modeling is a process of describing requirement description with Event-B formal language.However,the traditional modeling method can't solve the problems in Event-B modeling,such as intricate modeling process,difficulty in model maintenance and modificationas as well as poor readability of the model and so on.At present,the problems faced in Event-B modeling are manily solved by the improvement of the Event-B modeling method amd the Event-B model.Based on the Event-B model,Event-B graph model is proposed in this research.The Event-B graph model represents the Event-B model with a graphical structure.Based on Event-B graph model,a graphical modeling method is proposed in this research.Event-B graph based graphical modeling method provides a graphical analysis and modeling process from requirement analysis to model establishment for Event-B modeling.At the same time,the equivalence proof between the Event-B graph model and the Event-B model is also proved to guarantees the formal verification of Event-B graph model.Compared to representing the system into Event-B model,representing the system into Event-B graph model has more advantages,such as the modeling process of Event-B graph model is more comprehensible,the Event-B graph model featuring graphical structure is more intuitive and clear,the maintainability and modification of Event-B graph model are easier and so on.Based on the ERTMS design standard,this reaearch also abstract a requirement analysis from the Hybrid ETCS-3 control protocol.Based on the graphical modeling method of EventB graph,this research completes the model construction and verification of Hybrid ETCS-3 control protocol.From the modeling and verification result of the control protocol of Hybrid ETCS-3,this research completes the jugement of the security and reliability of system as well as gain the conclusion of the jugement.The results have shown good potential and significance for the verification of the safety and reliability of the promotion of train control system.