LTLC：面向实时与混成系统的连续时序逻辑

发布时间：2020-11-16 07:08

　　 混成系统是一种既包含离散成分又包含连续成分的计算系统，数控系统等一些与其外 部连续变化的物理环境不断交互的嵌入式系统就是其典型的代表．实时系统是一类特殊的 混成系统，其连续成分是一组用来表示时间约束条件的时钟．由于这些系统在工业及国防 领域有着重要而广泛的应用，它们的安全性和可靠性越来越引起人们的关注，因而对这些 系统进行形式化分析以确保其安全性和可靠性也成为近年来的一个研究热点． 为了描述实时及混成系统的性质和行为，十多年来，各种不同的时序逻辑如：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，并证明了 前两者的可满足性问题是可判定的．这三个子语言可分别用来表示有穷状态反应系统、有穷 控制状态实时系统以及混成系统．本文所给的关于 LTLC/B－公式的可满足性判定过程可 用于检查有穷状态反应系统之间的一致性以及有穷状态反应系统与其规范之间的一致性； 所给的关于LTLC/R-公式的可满足性判定过程可用于检查有穷控制状态实时系统之间的 一致性以及有穷控制状态实时系统与其规范之间的一致性． 此外，本文还给出了在样本控制模式下（在此模式下，混成系统的跳跃转换只发生在 整数时间点上）多速率混成系统关于 LTLC/H－公式的一个模型检查过程．
【学位单位】：中国科学院软件研究所
【学位级别】：博士
【学位年份】：2001
【中图分类】：TP302.1;TP302.2
【文章目录】：
'>

第一章 引 言
    1.1 反应系统
    1.2 实时和混成系统
    1.3 本文的目标、贡献和组成
第二章 线性时序逻辑LTL简介
    2.1 线性时序逻辑LTL
    2.2 LTL公式的可满足性的判定
第三章 连续语义线性时序逻辑LTLC
    3.1 预备概念
    3.2 LTLC的语法
    3.3 LTLC的语义
    3.4 利用LTLC/B－公式表示有穷状态反应系统
    3.5 LTLC/B－公式的可满足性判定
    3.6 小结
第四章 实时系统
    4.1 基本概念
    4.2 时间模块及其验证
    4.3 时间模块的模型检查与LTLC/R公式的可满足性判定
    4.4 小结
第五章 混成系统
    5.1 基本概念
    5.2 混成模块
    5.3 使用LTLC验证混成系统的性质
    5.4 多速率成模块的样本模型检查
    5.5 小结
第六章 相关工作
    6.1 实时逻辑
    6.2 实时和混成系统的验证
第七章 总结
攻读博士学位期间发表和录用的文章
致 谢
'>

【相似文献】

相关期刊论文 前10条

1 李林辉;刘东;杨冬亮;孙希意;;基于Web计算框架的调度日报系统[J];电力系统自动化;2011年15期

2 吴永刚;陆慧娟;程倬;陈江;;基于时间自动机的实时系统建模及验证[J];计算机时代;2011年06期

3 ;[J];;年期

4 ;[J];;年期

5 ;[J];;年期

6 ;[J];;年期

7 ;[J];;年期

8 ;[J];;年期

9 ;[J];;年期

10 ;[J];;年期

相关博士学位论文 前10条

1 李广元;LTLC：面向实时与混成系统的连续时序逻辑[D];中国科学院软件研究所;2001年

2 赵剑;混成系统基于模型诊断的若干问题研究[D];吉林大学;2012年

3 田聪;命题投影时序逻辑的判定性、复杂性、表达性及模型检测[D];西安电子科技大学;2010年

4 舒新峰;投影时序逻辑的完备公理系统与形式验证[D];西安电子科技大学;2010年

5 杨琛;打结不变的命题投影时序逻辑与模型检测[D];西安电子科技大学;2010年

6 万良;基于行为时序逻辑TLA的系统、规则与协议检测的研究[D];贵州大学;2009年

7 陈冬火;超协调时序逻辑及其模型检测方法[D];中国科学院研究生院（成都计算机应用研究所）;2006年

8 张海宾;混合系统的形式化验证[D];西安电子科技大学;2007年

9 龙士工;串空间理论及其在安全协议分析中的应用研究[D];贵州大学;2007年

10 徐鸣;程序验证与系统分析中的若干符号计算问题[D];华东师范大学;2010年

相关硕士学位论文 前10条

1 杨琳琳;基于时序逻辑的安全协议验证方法的研究[D];南京航空航天大学;2010年

2 费丽娟;构件组装中“特征干扰问题”的时序逻辑检测方法研究[D];华中师范大学;2004年

3 尹红丽;基于时序逻辑的协商公理体系多Agent系统的形式化模型[D];云南师范大学;2004年

4 伍晓敏;基于VSK-t逻辑的Agent形式化模型[D];云南师范大学;2004年

5 王帆;基于UML的形式化规范说明研究[D];天津大学;2004年

6 黎吾平;模型检测在软件方面的应用[D];吉林大学;2008年

7 刘凯;混成电力系统及其静态电压稳定性研究[D];贵州大学;2008年

8 李根;基于SPIN的命题投影时序逻辑模型检查[D];西安电子科技大学;2008年

9 董护斌;面向实时系统的实时区域时态逻辑：RRTL[D];西北大学;2002年

10 吴宏;基于LSC的模型检验研究与实现[D];国防科学技术大学;2004年

本文编号：2885776

boshi