用带时钟变量的线性时态逻辑扩充Object-Z

• 作者: 文志诚 李长云 满君丰
• 来源期刊: 计算机应用研究
• 关键词: Object-Z 用带时钟变量的时态逻辑 实时系统 形式规格说明 形式验证
• 年，卷（期）: 2009,（5）
• 所属期刊栏目: 软件技术研究
• 页码范围: 1764-1769
• 页数: 6页
• 分类号: TP311
• 语种: 中文
• DOI: 10.3969/j.issn.1001-3695.2009.05.047

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	满君丰	湖南工业大学计算机与通信学院	69	258	9.0	12.0
2	李长云	湖南工业大学计算机与通信学院	130	747	12.0	21.0
3	文志诚	湖南工业大学计算机与通信学院	49	279	10.0	14.0