Abstract:Informal verification methods for simulation models are vulnerable to subjective ingredients. The traditional model checking method has difficulty dealing with large-scale simulation models because of the state space explosion. The parallel model checking (PMC) method has been accepted and successfully implemented in industrial tools because of the completeness and high efficiency. Unfortunately, it is hard to use as it involves several difficulties, such as formal specifications, logics, and parallel computing. To solve the above problems, a parallel model checking method for simulation models based on event graphs is proposed in this paper. This method extends event graphs in synchronization and defines the syntax and semantics of the extended event graphs. It transforms the extended event graphs to distributed and parallel verification environment (DVE) model, and PMC method is successfully applied to simulation model verification filed. With this method, simulation participators can verify simulation models with PMC method without learning new formal modeling languages. The efficiency and completeness of simulation model verification are improved. The experimental results show the validity of this method, and the method can improve the application of PMC method in simulation field.