论文研究用带时钟变量的线性时态逻辑扩充ObjectZ.pdf

Object-Z是形式规格说明语言Z的面向对象扩充，适合描述大型面向对象软件规格说明，但它不能很好地描述连续性实时变量和时间限制。线性时态逻辑能够描述实时系统，但不能很好地处理连续时间关系，也不能很好地模块化描述形式规格说明。首先用时钟变量扩充线性时态逻辑，接着提出了一个方法——用带时钟变量的时态逻辑(LTLC)来扩充Object-Z。用LTLC扩充的Object-Z是一个模块化规格说明语言，是Object-Z语法和语义的最小扩充，其最大优点在于它能方便地描述和验证复杂的实时软件规格说明。