离散时段演算的符号模型验证

SYMBOLIC MODEL CHECKING OF DISCRETE DURATION CALCULUS

模型验证是对有限状态系统的一种形式化确认方法．近几年，模型验证方法已逐步扩展到实时系统应用中．为解决实时系统的模型验证问题，本文采用离散时段演算作为实时系统规格说明的形式语言，用时间自动机作为实时系统的实现模型，对模型验证问题进行了细致的分析，并提出了一种具有实际应用价值的方法──商技术．该方法可以避免当多个时间自动机并行组合时可能产生的状态空间组合爆炸问题，同时还可以简化整个模型验证问题．

Model-checking is a useful formal technique for verifying finite-statesystems. It compares system specifications given as logic fromulae with models ofrepresenting the actual behaviors of the systems. Model-checking has beenextended to real-time systems for a few years. The major hindrance to model-checking forreal-time systems is that time is continuous so that state space of a real-time systemis infinite.Fortunately,timed automata have been used lobe models of real-timesystems, and state-region graph technique is given for solving that problem. But, thenew technique was faced with some potential explosion problems arising from sometimed automata parallel composition. This paper uses discrete duration calculus asformal language to specify real-time systems, and timed automata as implementmodels of real-time systems. The paper analyses model-checking for real-timesystems concretely, proposes a practicable method, which is quotient technique, thatcan avoid explosion of state space when many timed automata are composedparalleled. This method can also simplify whole question of model-checking.