PTSC语言形式化语义的仿真设计

PTSC语言形式化语义的仿真设计

论文摘要

随着计算机系统的日益复杂,对其进行形式化描述也逐渐困难。实时概率并行语言(PTSC)由朱惠彪教授等提出,集概率,实时和基于共享变量的并行机制于一体,可用于描述复杂系统的特性。朱惠彪教授等已经研究了PTSC的代数定律和规范型,并在此基础上研究了操作语义的生成,从理论上证明了其代数语义和操作语义的正确性和一致性。本文分别通过Prolog和Maude实现了PTSC语言形式化语义的仿真,以程序的形式展示其语义的生成过程,给予一个更加生动鲜活的展示使读者对于语义有更清晰的理解,从实践的角度支持以上理论的正确性。本文中对语义的仿真主要由四部分构成。首先通过程序的形式构造PTSC的语法结构,在此基础上仿真各程序语句包括一般顺序结构,卫兵选择语句以及并行组合的变迁规则,通过这些变迁规则由原程序直接生成操作语义变迁规则。然后通过仿真代数规范型生成规则实现由一般程序到规范型的转换。最后,程序仿真了基于规范型生成操作语义的推导规则,从而推导出操作语义,即对操作语义和代数语义的连接的仿真。由于PTSC语言中包含不确定选择,以及不同的并行调度机制,因此对于同一PTSC程序可能会有多个不同的执行路径,在仿真程序中需要能够展现所有可能的执行路径。在Prolog实现的仿真中,这一点通过Prolog自带的回溯匹配实现,而在Maude实现的仿真中,结合其等式规则,重写推导规则及search搜索功能来实现。Prolog灵活的结构及操作符自定义属性使得仿真程序更加接近原操作语义。而Maude本身的等式和重写推导机制给仿真程序的实现带来便捷,同时因支持面向对象编程,使得仿真程序更具模块化,结构更加清晰。同时,在对语义正确性的验证方面,本文通过实现语义的仿真器,从而可以采用测试的方法通过测试用例来验证语义的正确性。

论文目录

  • 摘要
  • Abstract
  • 第一章 引言
  • 1.1 研究背景
  • 1.2 本文研究目标及贡献
  • 1.3 本文结构
  • 第二章 相关技术背景介绍
  • 2.1 实时概率并行语言PTSC简介
  • 2.2 Prolog简介
  • 2.3 Maude简介
  • 2.4 本章小结
  • 第三章 基于Prolog的PTSC语言语义仿真
  • 3.1 基于Prolog语义仿真的框架和设计思想
  • 3.2 基于Prolog对PTSC语法定义的仿真
  • 3.3 基于Prolog对PTSC操作语义的仿真
  • 3.4 基于Prolog对PTSC的代数语义及操作语义生成的仿真
  • 3.5 本章小结
  • 第四章 基于Maude的PTSC语言语义仿真
  • 4.1 基于Maude语义仿真的框架和设计思想
  • 4.2 基于Maude对PTSC语法定义的仿真
  • 4.3 基于Maude对PTSC操作语义的仿真
  • 4.4 基于Maude对PTSC代数语义及操作语义生成的仿真
  • 4.5 本章小结
  • 第五章 总结与展望
  • 5.1 总结
  • 5.2 展望
  • 参考文献
  • 作者研究生阶段参加的项目及发表文章情况
  • 发表论文情况
  • 参加的科研项目
  • 致谢
  • 相关论文文献

    • [1].基于非线性动力学建模的PTSC滤波与无功补偿系统研究[J]. 科技创新与应用 2019(22)
    • [2].浅谈煤矿调度的“PTSC”工作法[J]. 山东煤炭科技 2011(06)

    标签:;  ;  

    PTSC语言形式化语义的仿真设计
    下载Doc文档

    猜你喜欢