关键词: 观察者模式,实时系统,UPPAAL,Train-Gate,模型检测

Abstract: The verification of complex real-time system is always high-profile.A common way to describe the verification properties is using temporal logic,and the way is complex and difficult for laypeople.Observer patterns is an additional subsystem.It can transform the complex verification properties into simple reachability problem.The use of observer patterns can avoid using complex verification algorithm.The observer patterns proposed by Etienne and Nouha Abid were applied to the real-time system,Train-Gate system.UPPAAL was used to construct the observer models according to some scenarios in Train-Gate.Comparative experiment was used to compare the verification result with and without observer patterns.The experiment result shows that the use of observer patterns and verification properties both can get correct results.And the use of observer patterns can save time and it’s easier to accept for laypeople.Therefore,the use of observer patterns is feasible in the real-time systems like Train-Gate verification.

Key words: Observer patterns,Real-time system,UPPAAL,Train-Gate,Model checking