Model Checking on Duration Properties of Real-time Systems
实时系统时段性质的模型检验

Model Checking is a widely used technology to verify the design's correctness automatically. Real-time systems' properties include instant properties and duration properties. It is no doubt that checking real-time systems for the latter is much more difficult than the former. This paper introduces the main work on checking some duration properties of real-time systems for decades with comparison, and discusses the future work at last.