实时系统规范语言STeC的Maude语义模型和静态分析设计及其工具实现

发布时间：2024-03-30 08:30

　　信息系统融合系统的网络化、系统化和信息化等特性使得软件系统的复杂程度不断增加。尤其是时间和空间等物理元素的引入使得经典的建模方法无法满足其时空一致性需求,最近陈仪香教授引入了实时系统的规范语言Spatio-temporal Consistence Language for Real-time Systems(STeC)对时空一致性进行建模和分析。 本文从形式化角度对STeC语言进行研究,使用重写逻辑建立了STeC语言的Maude语义,利用Maude解释器对STeC模型进行仿真,开发了工具对STeC模型进行时空一致性的静态分析,搭建了STeC语言的一体化工具,在此基础上对中国高铁等例子进行建模分析和逻辑推理。 首先,本文提出了STeC语言的Maude语义模型。Maude语义主要使用关系等式理论和重写逻辑理论进行定义,其中对离散时间进行建模分析。通过有效的拓展,本文将STeC语言转化为可执行的基于Maude的形式化描述,使用Maude自动推导功能,验证STeC模型的逻辑正确性。 其次,本文对STeC模型进行静态分析,包括词法、语法分析,时空一致性分析和时钟满足性分析。借助目前主流的词法分析...

【文章页数】：83 页

【学位级别】：硕士

【文章目录】：
论文摘要
ABSTRACT
第一章 绪论
    1.1 选题的背景和意义
    1.2 研究现状
    1.3 论文主要研究内容和章节安排
    1.4 本章小结
第二章 预备知识
    2.1 实时系统规范语言STeC
    2.2 重写逻辑理论
    2.3 Maude语言
    2.4 本章小结
第三章 STeC语言的Maude语义模型
    3.1 STeC语言的Maude语义
    3.2 用例研究
    3.3 本章小结
第四章 STeC语言的静态分析
    4.1 STeC语言解释器
    4.2 STeC词法分析
    4.3 STeC语法分析
    4.4 STeC性质分析
    4.5 本章小结
第五章 STeC一体化工具的设计与实现
    5.1 工具总体情况介绍
    5.2 用例分析
    5.3 本章小结
第六章 总结与未来展望
    6.1 总结
    6.2 进一步工作
附录
    附录一 STeC语言语法的Maude语义
    附录二 STeC语言操作语义的Maude语义
    附录三 实时系统规范语言STeC静态分析工具软件设计书
参考文献
后记
攻读硕士学位期间发表论文和科研情况



本文编号：3942088