扩展线性时段不变式的模型检验研究进展

Advances in model checking of Extended Linear Duration Invariants

扩展线性时段不变式是时段演算中的一类重要公式.时段演算是周巢尘院士于20世纪90年代提出的一种用于嵌入式实时软件设计的演算系统,它开创性地将积分概念引入计算机实时软件的分析中,从而能够描述处理连续时间区间性质,是国际上公认的描述和分析实时系统的主流方法之一.由于时段演算内容丰富并且相关的综述和专著已出版,文章旨在对扩展线性时段不变式这一时段演算子集的模型检验问题的研究情况进行论述:①介绍时段演算、线性不变式及其扩展;②分别论述线性时段不变式以及扩展线性时段不变式的模型检验研究情况,其中重点介绍扩展的线性时段不变式,在离散时间语义和连续时间语义下的近期验证成果.

Extended Linear Duration Invariants (ELDIs) is an important subset of Duration Calculus(DC), proposed by academician Chaochen Zhou in 1990s. It introduces the notion of duration, the integral of state expression over the reference interval, and has become one of the main methods to specify and analyze real-time systems. Due to the rich content of DC and the publication of related reviews and monographs, we hereby focus on the research process of model checking of ELDIs. In this paper, we first introduce DC, LDIs and their extensions, and then discuss the research on model checking of LDIs and ELDIs, with emphasis on recent achievements in model checking of ELDIs in discrete time and continuous time semantics.