论文部分内容阅读
多线程离散事件模拟语言(Multithreaded Discrete Event Simulation Language,下文均简称MDESL)是一种类似于硬件描述语言Verilog的基于统一程序理论(UTP)的语言,由朱惠彪教授于2005年提出。MDESL有两个很重要的特征,其一是事件驱动模型计算,其二是共享变量并发。这种实时性语言不仅能够进行普通的编程建模,而且能够描述硬件的结构和行为。统一程序理论(Unifying Theories of Programming,下文均简称UTP)是一种典型的形式化方法,其详细讨论了程序的指称语义,代数语义和操作语义,证明了三者的一致性,并提出语义连接理论(Linking Theory)来描述语义模型间的关系,给出了一种能描述串行语言、并行语言、通信语言、逻辑语言、函数程序语言的统一数学模型。PVS(原型验证系统,Prototype Verification System,以下简称PVS)主要包括规约语言和定理证明器两部分,其规约语言基于高阶逻拜,具有丰富的类型系统,表达能力很强；其定理证明器以交互方式工作,同时又具备高度的自动化水准。它是一种提供了高效的撰写形式规约和交互式形式验证的系统,这为在计算机科学中严格、高效地应用形式化方法提供自动化的机器支持。以前对于指称语义的证明许多都是通过手工逻辑推理验证的,对于操作语义常是用基于双向模拟的方法验证。而在对PVS, UTP基础知识熟悉掌握的基础上本文在第二章详细介绍了MDESL语言的语法和语义,同时通过一个典型例子的编写规范,编译,类型检查和验证四个步骤简单介绍了PVS的规约语言的建模,及用PVS定理证明器的证明过程。在第二章基础上利用PVS对MDESL语言进行了指称语义分析与建模,从第三章基础环境的建模到第四章的谓词建模和高阶逻辑的三元组建模。整个模型分为五个THEORY (Env, Skippre, Command, Tripro, Skip),他们将分别在第三章,第四章被介绍到,其关系图如第三章图3.2,而整个模型的建模结构思路如第三章图3.1。随后在第五章介绍了五个THEORY中的典型的定理(共四个),经过一步步分析说明证明思路,详细介绍了PVS定理证明器的证明步骤和证明策略。验证了模型的正确性以及MDESL语言指称语义的正确性。对MDESL语言的指称语义建模并没有结束,未来的工作重心还将包括引入事件驱动模型,并发操作等更加复杂的结构,甚至对操作语义与指称语义的连接的建模与定理验证。