中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
LTLC:面向实时与混成系统的连续时序逻辑
作者: 李广元
答辩日期: 2001
专业: 计算机软件与理论
授予单位: 中国科学院软件研究所
授予地点: 中国科学院软件研究所
学位: 博士
关键词: 实时系统 ; 混成系统 ; 时序逻辑 ; 实时逻辑 ; 规范语言 ; 系统刻画语言 ; 可满足性 ; 可判定性 ; 模型检查
摘要: 混成系统是一种既包含离散成分又包含连续成分的计算系统,数控系统等一些与其外部连续变化的物理环境不断交互的嵌入式系统就是其典型的代表。实时系统是一类特殊的混成系统,其连续成分是一级用来表示时间约束条件的时钟。由于这些系统在工业及国防领域有着重要而广泛的应用,它们的安全性和可靠行性越来越引起人们的关注,因而对这些系统进行形式化分析以确保其安全性和可靠性也成为近年来的一个研究点。为了描述实时及混成系统的性质和行为,十多年来,各种不同的时序逻辑如:Metric Interval Temporal Logic, Real-Time Temporal Logic, Integrator Computation Tree Logic和Hybrid Temporal Logic 等相继提出,尽管这些时序逻辑作为远见规范语言用于描述实时及混成系统的性质时都还比较合适,但它们不适合用来表示实时及混成系统的实现,因为它们缺乏表示系统状态的动态变化的能力。在现在文献中,实时和混成系统通常常是用时间自动机、混成自动机、时间转换系统和相位转换系统等来表示的。但这些系统刻画语言却不适合作为规范语言来使用,因为它们不能表示实时和混成系统的一些重要性质(如安全性和活性等)。这样在基于逻辑方法的和混成系统的研究中,系统和它的性质通常是用两个不同的语言来表示的。本文定义了一个具有连续语义的线性时序逻辑,记为LTLC,它是Manna和Pnueli所提出的线性时序逻辑LTL的一个推广。LTLC既能表示实时和混成系统的性质,又能很方便地表示实时和混成系统的实现,它能在统一的语义框架中表示出从高级的需求远东到低级的实现模型之间的不同抽象层次上的系统描述,并且能用逻辑蕴涵来表示不同抽象层次的系统描述之间的语义一致性。本文还定义了LTLC的三个子语言:LTLC/B、LTLC/R及LTLC/H, 并证明了前两者的可满足性问题是可判定的。这三个子评议可分别用来表示有穷状态反应系统、有穷控制状态实时系统以及混成系统。本文所给的关于TLC/B-公式可满足性判定过程可用于检查有穷状态反应系统之间的一致性以及有穷状态反应系统与其规范之间的一致性;所给的善于TLC/R-公式的可满足性判定过程可用于检查有穷控制状态实时系统之间的一致性以及有穷控制状态系统与其规范之间的一致性。此外,本文还给出了在样本控制模式下(在此模式下,混成系统跳跃转换只发生在整数时间点上)多速率混成系统关于LTLC/H-公式的一个模型检查过程。
英文摘要: Hybrid systems are computational systems consisting of both continuous and discrete components. Typical examples are digital controllers that interact with continuously changing physical environments. Real-time systems are a subclass of hybrid systems where the continuous components of the system are clocks which are used to express the timing constraints on the system. Because of their extensive application in industry and national defence, real-time and hybrid systems mostly focus on the safety and reliability properties. So the formal analysis of these systems becomes an interesting topic. In order to specify real-time and hybrid systems, many temporal logics, such as Metric Interval Temporal Logic, Real-time Temporal Logic, Integrator Computation Tree Logic, and Hybrid Temporal Logic have been proposed. Though these logics are good at specifying properties of real-time and hybrid systems, they are not suited for describing the implementations of such systems. They lack the ability to describe the dynamic change in the state of real-time and hybrid systems. In the literature, real-time and hybrid systems are usually described by Timed Automata, Hybrid Automata, Timed Transition Systems and Phase Transition Systems. However, these system description languages cannot be used as specification languages, because they lack the ability to express some important properties (such as safety properties and liveness properties) of real-time and hybrid systems. Thus, real-time and hybrid systems and their properties are usually described by different languages. In this thesis, a new linear temporal logic with continuous semantics, called LTLC, is introduced. It is an extension of Manna and Pnueli's linear temporal logic. It can express both the properties and the implementations of real-time and hybrid systems. With LTLC, systems can be described at many levels of abstraction, from high-level requirement specifications to low-level implementation models, and the conformance between different descriptions can be expressed by logical implication. Three sub-languages of LTLC, called LTLC/B, LTLC/R and LTLC/H, are defined and the satisfiability problems for the first two are proved to be decidable. They are used to represent finite-state reactive systems, finite-location real-time systems and hybrid systems respectively. Our decision procedure for LTLC/B can be used to check whether a finite-state reactive system meets a required specification or whether a finite-state reactive system conforms with another system. Our procedure for LTLC/R can do the similar things for real-time systems with finite control locations. In addition, a model-checking procedure for multirate hybrid systems is also given. It can decide whether a formula in LTLC/H is true with respect to a given multirate automaton whose jump transitions happen only at integer times.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/7286
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
LW004415.pdf(1480KB)----限制开放-- 联系获取全文

Recommended Citation:
李广元. LTLC:面向实时与混成系统的连续时序逻辑[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2001-01-01.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[李广元]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[李广元]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace