面向同步系统的时钟约束动态逻辑系统研究
发布时间：2022-12-07 19:27
实时系统、嵌入式系统等反应式系统（Reactive Systems）往往具有“同步”特性,即模块间通信时间可忽略不计,同一时刻多个信号可同时发生.同步系统模型作为同步编程语言（如Esterel、Signal等）的基础,被广泛应用于反应式系统,特别是嵌入式系统的建模中.随着近年来物联网、信息物理系统等分布式实时嵌入式系统的蓬勃发展,同步系统的建模、规约与验证变得愈发重要.在同步系统中,基于“时钟约束”的系统规约在系统的安全性和可靠性方面扮演着关键角色.时钟约束规约语言（Clock Constraint Specification Language,简称CCSL）是一种基于“时钟”和时钟约束关系的形式化规约语言.它被广泛地应用于同步系统的规约与验证.以往CCSL规约的验证技术主要基于模型检测.由于模型检测技术的局限性,这些验证技术不支持无限状态CCSL规约（亦称为“非安全”CCSL规约）的验证.对于状态空间较大的系统,基于模型检测的验证技术存在状态空间爆炸的问题.动态逻辑（Dynamic Logic,简称DL）是一种对程序动态行为进行刻画和推理的模态逻辑,其验证技术主要基于定理证明和SMT...
【文章页数】：220 页
【学位级别】：博士
【文章目录】：
摘要
ABSTRACT
第一章 绪论
1.1 研究背景与现状
1.1.1 同步系统模型
1.1.2 CCSL
1.1.3 动态逻辑
1.1.4 本文关注的研究问题
1.2 研究问题
1.3 主要贡献
1.3.1 研究思路
1.3.2 研究意义
1.3.3 主要工作
1.4 章节安排
第二章 预备知识
2.1 CCSL语言
2.2 Kripke框架
2.3 一阶动态逻辑FODL
2.4 Sequent演算
2.5 本章小结
第三章 面向顺序程序的时钟约束动态逻辑sCDL
3.1 引言
3.2 同步事件顺序程序SESP
3.3 sCDL公式的语法
3.4 sCDL逻辑的语义
3.4.1 sCDL逻辑的解释,Kripke框架和赋值
3.4.2 SESP程序的语义
3.4.3 sCDL公式的语义
3.4.4 可满足关系和替换定理
3.5 sCDL逻辑证明系统
3.5.1 路径公式规则
3.5.2 非路径公式的规则
3.5.3 其它逻辑规则
3.6 一个sCDL逻辑的案例分析
3.6.1 Feeder系统
3.6.2 sCDL逻辑的局限性
3.7 本章小结
第四章 时钟约束动态逻辑CDL
4.1 引言
4.2 CDL公式的语法
4.2.1 同步事件程序SEP
4.2.2 CDL公式的语法
4.3 CDL公式的语义
4.3.1 SEP程序的逻辑一致性
4.3.2 并行交互条件逻辑公式的构造与并行trec程序的语义
4.3.3 SEP程序的语义
4.3.4 CDL上的可满足关系与替换定理
4.4 CDL逻辑证明系统
4.4.1 CDL逻辑并行算子的规则
4.4.2 并行算子证明规则中的算法
4.4.3 SEP程序的可推导关系
4.5 CCSL规约在时钟约束动态逻辑中的表示
4.6 本章小结
第五章 CDL逻辑系统的分析
5.1 引言
5.2 CDL逻辑证明系统的可靠性
5.2.1 非并行算子证明规则的可靠性
5.2.2 并行算子证明规则的可靠性
5.3 CDL逻辑证明系统的相对完备性
5.3.1 相对完备性定理的证明
5.3.2 相对完备性定理中各条件的证明
5.4 本章小结
第六章 CDL逻辑系统的案例分析
6.1 引言
6.2 数字滤波器系统
6.2.1 系统功能介绍
6.2.2 系统行为、性质的建模
6.3 车载自动窗系统
6.3.1 系统功能介绍
6.3.2 系统行为、性质的建模
6.4 系统CCSL规约在CDL逻辑系统中的证明
6.5 本章小结
第七章 总结和展望
7.1 本文工作总结
7.2 未来工作的展望
参考文献
致谢
攻读博士学位期间发表论文和科研情况
【参考文献】：
期刊论文
[1]信息物理融合系统研究[J]. 李馥娟,王群,钱焕延. 电子技术应用. 2018(09)
[2]信息物理融合系统研究综述[J]. 王中杰,谢璐璐. 自动化学报. 2011(10)
[3]物联网技术研究综述[J]. 王保云. 电子测量与仪器学报. 2009(12)
[4]模型检测:理论、方法与应用[J]. 林惠民,张文辉. 电子学报. 2002(S1)
本文编号：3712701
【文章页数】：220 页
【学位级别】：博士
【文章目录】：
摘要
ABSTRACT
第一章 绪论
1.1 研究背景与现状
1.1.1 同步系统模型
1.1.2 CCSL
1.1.3 动态逻辑
1.1.4 本文关注的研究问题
1.2 研究问题
1.3 主要贡献
1.3.1 研究思路
1.3.2 研究意义
1.3.3 主要工作
1.4 章节安排
第二章 预备知识
2.1 CCSL语言
2.2 Kripke框架
2.3 一阶动态逻辑FODL
2.4 Sequent演算
2.5 本章小结
第三章 面向顺序程序的时钟约束动态逻辑sCDL
3.1 引言
3.2 同步事件顺序程序SESP
3.3 sCDL公式的语法
3.4 sCDL逻辑的语义
3.4.1 sCDL逻辑的解释,Kripke框架和赋值
3.4.2 SESP程序的语义
3.4.3 sCDL公式的语义
3.4.4 可满足关系和替换定理
3.5 sCDL逻辑证明系统
3.5.1 路径公式规则
3.5.2 非路径公式的规则
3.5.3 其它逻辑规则
3.6 一个sCDL逻辑的案例分析
3.6.1 Feeder系统
3.6.2 sCDL逻辑的局限性
3.7 本章小结
第四章 时钟约束动态逻辑CDL
4.1 引言
4.2 CDL公式的语法
4.2.1 同步事件程序SEP
4.2.2 CDL公式的语法
4.3 CDL公式的语义
4.3.1 SEP程序的逻辑一致性
4.3.2 并行交互条件逻辑公式的构造与并行trec程序的语义
4.3.3 SEP程序的语义
4.3.4 CDL上的可满足关系与替换定理
4.4 CDL逻辑证明系统
4.4.1 CDL逻辑并行算子的规则
4.4.2 并行算子证明规则中的算法
4.4.3 SEP程序的可推导关系
4.5 CCSL规约在时钟约束动态逻辑中的表示
4.6 本章小结
第五章 CDL逻辑系统的分析
5.1 引言
5.2 CDL逻辑证明系统的可靠性
5.2.1 非并行算子证明规则的可靠性
5.2.2 并行算子证明规则的可靠性
5.3 CDL逻辑证明系统的相对完备性
5.3.1 相对完备性定理的证明
5.3.2 相对完备性定理中各条件的证明
5.4 本章小结
第六章 CDL逻辑系统的案例分析
6.1 引言
6.2 数字滤波器系统
6.2.1 系统功能介绍
6.2.2 系统行为、性质的建模
6.3 车载自动窗系统
6.3.1 系统功能介绍
6.3.2 系统行为、性质的建模
6.4 系统CCSL规约在CDL逻辑系统中的证明
6.5 本章小结
第七章 总结和展望
7.1 本文工作总结
7.2 未来工作的展望
参考文献
致谢
攻读博士学位期间发表论文和科研情况
【参考文献】：
期刊论文
[1]信息物理融合系统研究[J]. 李馥娟,王群,钱焕延. 电子技术应用. 2018(09)
[2]信息物理融合系统研究综述[J]. 王中杰,谢璐璐. 自动化学报. 2011(10)
[3]物联网技术研究综述[J]. 王保云. 电子测量与仪器学报. 2009(12)
[4]模型检测:理论、方法与应用[J]. 林惠民,张文辉. 电子学报. 2002(S1)
本文编号：3712701
本文链接：https://www.wllwen.com/kejilunwen/ruanjiangongchenglunwen/3712701.html
