带有时钟变量的线性时序逻辑与实时系统验证
DOI:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

国家自然科学基金资助项目(60073020);国家"九五"重点科技攻关项目(98-780-01-07-01);国家863高科技发展计划资助项目(863-306-ZT02-04-1)


A Linear Temporal Logic with Clocks for Verification of Real-Time Systems
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    为了描述实时系统的性质和行为,10多年来,各种不同的时序逻辑,如Timed Computation Tree Logic,Metric Interval Temporal Logic和Real-Time Temporal Logic等相继提出来.这些时序逻辑适于表示实时系统的性质和规范,但不适于表示实时系统的实现模型.这样,在基于时序逻辑的实时系统的研究中,系统的性质和实现通常是用两种不同的语言来表示的.定义了一个带有时钟变量的线性时序逻辑(linear temporal logic with clocks,简称LTLC).它是由Manna和Pnueli提出的线性时序逻辑在实时情况下的一个推广.LTLC既能表示实时系统的性质,又能很方便地表示实时系统的实现.它能在统一的语义框架中表示出从高级的需求规范到低级的实现模型之间的不同抽象层次上的系统描述,并且能用逻辑蕴涵来表示不同抽象层次的系统描述之间的语义一致性.LTLC的这个特点将有助于实时系统的性质验证和实时系统的逐步求精.

    Abstract:

    In order to specify real-time systems, many temporal logics such as Timed Computation Tree Logic, Metric Interval Temporal Logic and Real-Time Temporal Logic have been proposed. Although these logics are good at specifying properties of real-time systems, they are not suitable for describing the implementations of such systems. Thus, the specifications and the implementations are usually described by different languages for real-time systems. In this paper, a new linear temporal logic with clocks, called LTLC,is introduced.It is anextension of Manna and Pnueli's linear temporal logic.It can express both the properties and the implementaions ofreal-time system.With LTLC,systems can be described at many at many levels of abstraction,from high-level requirement specificatons to low-level implementation models,and the conformance between different descriptions can be expressed by logical implication.This aspect of LTLC will be beneficil to the verification and the stepwise refinements of real-time systems.

    参考文献
    相似文献
    引证文献
引用本文

李广元,唐稚松.带有时钟变量的线性时序逻辑与实时系统验证.软件学报,2002,13(1):33-41

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2000-07-20
  • 最后修改日期:2001-06-20
  • 录用日期:
  • 在线发布日期:
  • 出版日期:
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号