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－公式的一个模型检查过程。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 108 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/7286]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 李广元. LTLC:面向实时与混成系统的连续时序逻辑[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2001. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。