一、陈仪香教授与计算语义模型研究（论文文献综述）
温晋杰[1]（2020）在《空天运输遥操作系统净评估与可信度认定研究》文中研究说明为了统筹经济建设与国防建设协同发展,我国提出了“军民融合”国家战略,其核心是促进军民两个领域双向技术交流。空天运输是军民融合发展的重点领域和先导行业,在空天运输嫦娥系列任务中,一个关键组成部分是地面控制中心通过空天运输遥操作系统推送操控信息实现月面巡视器无人自动巡视和科学就位探测。但是,针对我国空天运输领域信息技术国产、自主和可控的发展需求,我国还没有相当的空天运输遥操作系统设计、实施、测试和维护等方面的质量评估方法、技术、体系和标准,在技术层面还缺乏军民融合准入/准出评估机制。围绕上述研究背景和研究问题,本文应用净评估理论,提出了空天运输遥操作系统系统净评估方法,定量认定了探月工程嫦娥系列任务遥操作系统的可信度,建立了空天运输遥操作系统净评估体系,意图保障嫦娥五号任务万无一失,为空天运输领域军民融合战略落地提供技术保障。本文的主要研究工作和创新点如下:（1）首次将净评估理论引入空天运输领域,提出了利用形式化方法建立空天运输遥操作系统净评估指标体系数学模型,借助自主可控的自动化工具采集系统可信证据,从而实现遥操作系统可信度认定的净评估方法。在嫦娥五号任务联调联试过程中,通过净评估方法准确定位了遥操作系统全生命周期的不可信因素,解决了系统质量不可控的问题,实现了遥操作系统联调联试零差错。（2）以遥操作系统相关的软件过程文档、国家军用标准和空天运输领域特性作为净评估指标来源,利用形式化Z语言构建了遥操作系统净评估指标体系数学模型,保障了评估指标的准确性和全面性,解决了嫦娥四号和嫦娥五号任务遥操作系统净评估指标二义性和需求动态变化的问题,为遥操作系统可信证据自动化采集打下基础。（3）以遥操作系统净评估指标体系数学模型为输入,搭建了国产自主可控的空天运输遥操作系统可信证据自动采集平台。在嫦娥四号任务执行前,该平台自动采集了科学客观的嫦娥四号遥操作系统可信证据,确保了嫦娥四号遥操作任务圆满完成。（4）利用偏差最小化方法提出了层次分析法和熵权法结合的组合赋权法。针对数学理论赋权方法的不实际性问题,在航天信息资源国产化的前提下,借助可视化技术实现了近十年来国家载人航天和探月工程历次航天任务数据的长期保存,完成了净评估前期知识积累。同时,构建了遥操作系统净评估虚拟仿真环境,通过回放和论证净评估过程,实现了工程实践数据持续优化数学理论赋权模型的研究方案,提高了净评估指标赋权的可靠性和可信性。（5）针对空天运输领域信息技术自主可控的核心需求,在Windows和国产麒麟操作系统上完成了探月工程嫦娥系列任务遥操作系统的设计、开发、测试、维护和评估,实现了跨平台且具有自主知识产权的航天任务信息推送平台,为嫦娥系列任务执行提供了安全保障。上述研究成果经探月工程二期实战检验,实现了遥操作系统可信度认定,精准实施并圆满完成了嫦娥三号和嫦娥四号任务,并通过了GJB 9001C-2017武器装备质量管理体系认证,为探月工程后续任务和火星探测任务信息系统的开发、质量评估和改进提供了技术框架。
熊家文[2]（2020）在《协作式工业控制系统建模、分解及验证技术研究》文中进行了进一步梳理随着国家在工业化发展进程上的不断深入,工业控制系统作为一种过程控制系统,被越来越广泛地应用于各行各业之中。由于工业控制系统通过各类执行机构能够对物理世界产生直接影响,其错误的运行将可能导致严重的安全事故,继而造成较大的经济损失、人员伤亡乃至重大的环境灾难。因此,在正式投入运行之前,其功能正确性、安全性及可靠性必须得到严格的保障。在当前的工业控制系统功能正确性保障工作中,主要采用的还是在设计阶段进行仿真以及在实现后进行测试的方法,但仿真与测试方法难以对系统行为进行深入而全面的考察,尤其对于具备复杂行为的系统,很难提供完备而严格的保障。因此,部分学者尝试引入形式化验证技术。但由于形式化验证技术具有较高的使用门槛,其实际应用并不广泛。且由于目前形式化验证技术存在一定的不足,大多数的现有工作都只关注了单个功能模块或程序的验证,而无法对多个任务协同的工业控制系统整体进行验证。而且,伴随着控制器技术、网络技术的发展,工业控制系统逐步从简单的单控制器控制系统发展为多控制器的分布式工业控制系统、现场总线工业控制系统乃至基于工业以太网的协作式工业控制系统,其复杂性日益提升,其功能正确性保障工作将面临更大的挑战,过去的方法将变得更加难以适用。因此,为了提高现代工业控制系统的功能正确性保障能力,本论文针对协作式工业控制系统,从设计方法及验证方法两方面,提出了两项功能安全性保障方法。首先提出了一套建模、分解方法,支持复杂工业控制系统的控制功能集中建模与特定资源约束条件下的自动分解,帮助用户以全局视角设计具备复杂交互关系的协作式工业控制系统,从而避免人为设计过程中可能引入的错误;其次提出了一种用户友好的轻量级形式化性质验证方法,从而方便用户对实现后的协作式工业控制系统进行快速性质考察;特别地,由于其基于系统运行日志的工作特性,在复杂控制系统的验证方面具有独特的优势。通过这两方面的功能正确性保障方法的辅助,工程师可以更加高效地开发出可靠的协作式工业控制系统。在创新性工作方面,具体包括了以下四个部分:1.提出了一种支持协作关系描述以及设备资源约束关系描述的建模语言CICSML,以支持协作式工业控制系统控制功能的统一抽象建模。该语言考虑了IEC 61131-3标准中描述的工业控制器软件特性,借鉴了结构化文本编程语言的语法,与工业控制系统软件实现存在较为直接的对应关系,可以轻松地转换为具体的实现代码。2.在建模语言的基础之上,提出了一种特定设备资源约束下的模型分解方法。该分解方法能够将单控制器复杂系统模型,按照给定设备资源约束,自动分解为多控制器的简单子系统模型集合。这些子系统模型通过自动生成的交互机制进行协作,共享给定的设备资源,从而形成多控制器协同的协作式工业控制系统。3.提出了一套轻量级的协作式工业控制系统形式化性质验证方法,主要结合工业控制程序仿真技术及规范挖掘技术,将形式化性质的验证过程从主动变为被动,从而极大地降低了复杂工业控制系统形式化性质验证的门槛。4.另外,提出了一种带过去时态的线性时态逻辑规范挖掘方法,改善了目标性质规范的表达能力,进一步增强了该轻量级性质验证方法。
向霜晴[3]（2020）在《软件定义网络的形式化建模与验证》文中研究表明软件定义网络（Software-Defined Networking,SDN）是一种新兴的网络架构,能够解决传统网络层级复杂,以至难以管理和创新的问题。该架构将控制逻辑从转发设备上分离出来,形成逻辑上集中的中心控制器,并提供网络可编程性。SDN的出现不仅推动了网络架构的更迭,更带来了网络开发方法的变革,可以预见在未来的网络开发流程之中,形式化方法必定处于极其重要的地位。本文通过形式化方法建模SDN并验证相关性质。对于与数据转发逻辑有关的性质,扩展了知名的软件定义网络编程语言NetKAT,提出了能描述虚拟局域网（VLAN）、拥有更强表达能力并且支持模型检测的语言PDNet,研究了PDNet的操作语义,并基于操作语义证明了PDNet和NetKAT在表达能力上的联系与差别。对于与SDN模块或应用的设计、功能和安全有关的性质,基于图灵奖得主C.A.R.Hoare教授提出的通信顺序进程（CSP）设计了系统建模框架,并在模型检测工具PAT（Process Analysis Toolkit）中进行了实现。基于该框架,本文建模并验证了开源控制器Floodlight的基础模块以及安全控制器TopoGuard的防御策略,以展示该框架的使用方法和实际价值。本文的主要内容和贡献包括以下三点:·提出了基于克莱尼代数（KA）的网络编程语言PDNet,来刻画数据层的转发逻辑。该语言对高级网络编程语言NetKAT（由康奈尔大学等研究机构提出）进行了扩展,从而能描述SDN的重要应用场景VLAN。同时,本文基于下推系统研究了PDNet的操作语义,并定义了语法导出规则。此外本文基于操作语义证明了PDNet的表达能力强于NetKAT。·总结归类了SDN三层架构以及外部环境中的软硬件设备,分析了各类对象在模型中的行为,提出了基于CSP的SDN系统建模框架。同时,本文建立了可实例化的数据层模型和四类主机模型,并为九种可能的攻击提供了建模方案,此外,为两种已知的,危害范围极广的攻击建立了攻击者模型。·基于系统建模框架,建模验证了开源控制器Floodlight的六个基本模块和安全控制器TopoGuard的攻击防御机制。对于Floodlight,我们验证了其基本模块的设计、功能与安全相关的性质。验证结果显示其拓扑发现和设备管理模块会受到链路攻击和主机攻击的危害,因此一大批与Floodlight使用类似的拓扑发现和设备管理方案的开源控制器都被这两种攻击影响。基于此,本文验证了为防御这两种攻击而设计的安全控制器TopoGuard,发现了两个严重问题,并提出了解决方案。
朱晓冉[4]（2019）在《基于重写逻辑的嵌入式操作系统建模与验证技术研究》文中研究说明随着信息科学技术的逐渐成熟,嵌入式系统正在进入一个高速发展的全新时代。在航空航天、医疗设备、汽车电子等安全攸关领域中,嵌入式系统的安全可靠性和稳定性愈发重要。操作系统作为嵌入式系统的核心部分,负责管理软硬件组件并向用户提供各种服务,使整个系统实时高效率地运行。因此,如何保证操作系统的安全性和正确性是构建可信嵌入式系统的关键问题。形式化方法以其高度数学化和严谨性的特点,被广泛应用于系统可靠性分析工作中。然而,受验证工具的限制以及操作系统自身特点的影响,形式化方法在操作系统验证中的应用仍面临许多挑战。例如,自动化验证工具的灵活性有一定局限性,很难建立在一定领域中通用的模型来分析操作系统的各个组成部分。另外,操作系统内核通常使用高级语言和汇编指令混合实现,为了统一高级与汇编程序的抽象模型,目前大多数方法是抽象汇编程序,或向下编译高级语言程序,然后反汇编并在统一的汇编程序上建立模型,而很难实现对原始代码程序的验证。本文基于操作系统验证工作中存在的挑战,结合重写逻辑理论的最新建模方法,以汽车电子操作系统为研究对象,对嵌入式操作系统的建模和验证技术进行了研究,建立了汽车电子操作系统规范以及内核实现的语义模型,在语义模型的基础上分别对操作系统规范、内核和应用的正确性进行了分析和验证。具体的,本文主要研究内容和贡献如下:·建立了完整的车载操作系统OSEK规范的语义模型。OSEK规范的语义模型定义了操作系统任务调度、资源管理、事件管理、错误处理、中断机制和报警机制相关的系统服务执行规则,并刻画了系统服务和应用程序的执行时间。对于自然语言规范中未定义或有二义性的行为进行了重定义,应用可达性检查方法分析了重定义行为的合理性。·提出了面向嵌入式操作系统内核的混合语言程序分析方法。定义了操作系统内核中抽象的汇编指令、C语言子集以及其混合语言的操作语义,语义规则覆盖了不同语言间子程序调用以及共享变量的执行情况。基于混合语言的操作语义,应用可达性逻辑证明系统可证明混合语言程序的可达性。结合基于重写逻辑理论的分析工具,自动化验证了内核中上下文切换程序的原子执行性。·实现了操作系统规范、内核和应用的自动化验证。基于完整的OSEK规范模型,分别验证了规范中任务调度、事件管理、资源管理和报警机制的正确性。对规范模型的验证,一方面为确定规范中未定义行为的执行规则提供了参考意义,另一方面可分析操作系统性质,减小系统层性质分析的验证代价。另外,基于内核和规范的语义模型,分别对普华基础软件公司所开发的OSEK操作系统内核与应用程序的代码进行验证,并发现了应用程序中潜在的缺陷,展现了本文方法的实用性。
杨志华[5]（2016）在《基于STeC的空天地一体化地球观测的验证与仿真》文中研究表明空天地一体化网络是基于空天地异构网络和来自空、天、地面以及海中的节点互连的网络,是安全攸关的系统,网络的可靠性和可信性是非常重要的问题。地球观测任务是基于空天地一体化网络的基础且关键的应用,而基于地球观测应用场景对该网络进行建模、仿真和验证研究则可以帮助确保系统的正确性和可靠性。相对比其他形式化建模语言,STeC语言由于其强调时间、空间及时空一致性信息,使得其更加适合应用于空天地一体化网络中地球观测任务的建模。首先,本文对实时系统规范语言STeC进行适当和必要的领域化,使其可以应用在空天地一体化网络领域中,使用该Domain-STeC完成对系统中两种场景下的地球观测任务的建模。其次,利用模型检测对系统性质进行验证分析。使用STeC工具对模型进行初步检查：包括词法、语法分析、时空一致性分析；并将模型转换成时间自动机模型,在UPPAAL中进行多种性质验证。再次,基于STeC语言和航天仿真工具STK进行二次开发,开发地球观测任务仿真控制工具,该工具除了提供对STK工具的基本控制功能之外,可以将STeC语言翻译成STK控制命令,使用STeC语句实时动态仿真任务中各智能体的行为,并在STK工具中图形化地动态显示任务执行过程。最后,基于STeC语言中的时空点概念引入时空曲线概念,使其能够描述地球观测任务中任务调度相关的区域覆盖问题,并探讨了三种简单情况下的任务的规划调度问题。
吴茜[6]（2016）在《基于质量演算的无线网络形式语义与分析》文中认为无线网络（Wireless Networks）是由一组无线的、可移动的网络节点组合而成的网络体系架构,该网络架构已经被广泛地应用于信息物理融合系统、人工智能、分布式计算、灾害恢复以及军事控制等领域。无线网络与传统的有线网络的区别在于：1)局部广播（Local Broadcast）通信模式：在无线网络中,每个网络节点具有一个消息传输半径,只有在消息发送节点的有效传输范围内的接收节点才能够通过使用与发送节点相同的无线信道接收到发送节点发送的消息；2)节点移动性：无线网络的拓扑结构不再是固定不变的,随着时间的流逝,网络节点会遵循一定的移动模式进行移动,导致整个网络拓扑结构的变化。由于无线网络具有以上两个重要特征,加上网络节点通常暴露于环境中,因此节点之间的通信链路会因为网络特征及环境的影响而具有不可靠性,使得网络节点无法在规定时间内收到预想消息,导致网络资源不可用及系统理想行为的失败,从而大大降低了无线系统的服务质量。特别是对于与安全息息相关的系统而言,不可靠链路可能会导致无线系统的瘫痪,甚至带来一系列多米诺效应。因此,如何刻画无线网络特征、降低网络链路不可靠性带来的影响并提高无线系统服务质量成为重要的研究点。在众多的研究方法中,形式化方法以其精确严密的特征被广泛地应用于各个领域。本文基于无线系统的质量视角,围绕上述研究点,提出无线网络的形式语义与分析方法。论文中提及的“质量视角”是指当分布式无线网络节点处于不可靠通信链路中而导致网络节点预想行为失败时,通过本地设备提供的缺省值机制来确保处于不可靠链路中的节点仍然可以给出一个合理的行为,降低不可靠链路带来的影响,从而提高网络服务质量。论文提出面向无线网络的质量演算,该演算不仅捕捉了无线网络局部广播及节点移动等特性,同时,将质量谓词作为卫兵与广播接收动作相结合,用来刻画当节点接收动作满足一定条件时,节点才能够继续执行后续进程,其与节点缺省值机制共同作用,降低了不可靠链路带来的影响。本文给出质量演算的操作语义及指称语义模型,并对无线网络相关性质进行研究。在静态分析理论的指导下,本文提出基于SAT技术的系统鲁棒性分析方法及基于数据的概率可信性分析方法,分别针对网络通信链路的可靠性以及接收到的数据的概率可信性进行了分析。最后,本文使用研究所得的理论与技术对无线网络在智能楼宇、车联网等实际生活中的案例进行了建模和分析,展示了该研究的实际意义和价值。本文的主要内容与贡献包括：·本文提出了面向无线网络的质量演算CWQ语言与mCWQ语言。CWQ语言引入了带有质量谓词的广播接收动作及网络节点的缺省行为机制,囊括了节点通信的物理因素,如节点位置、通信半径以及通信信道等信息,从进程层和网络层两个层面对无线网络进行了刻画,在捕捉了网络局部广播特性的同时,确保了网络节点面临不可靠链路时仍然可以给出合理的行为,以提高网络的服务质量。为了进一步捕捉无线网络的节点移动性,本文将CWQ语言扩展为带有移动特性的mCWQ语言,引入了时间算子及节点的移动模型,从而更好地刻画了网络拓扑结构的动态变化。·本文研究了无线网络质量演算的语义模型。本文提出了无线网络质量演算的操作语义和指称语义模型。首先给出了CWQ演算的标签转移语义及规约语义两种操作语义形式,并使用和谐定理证明了两个语义形式的一致性。之后,给出了mCWQ演算的参数化标签转移语义,通过语义的变迁规则直观地刻画了网络程序运行的过程及网络节点的运行轨迹；同时给出了mCWQ演算的指称语义模型。基于给定的操作语义及指称语义规则,本文对无线网络的相关性质进行了刻画和研究。·本文分析了无线网络通信链路的可靠性和数据概率可信性。本文提出了基于SAT技术的系统鲁棒性分析方法来避免整个网络由于通信链路的不可靠而到达一个错误状态,并使用SMT求解器Z3进行辅助判断。另外,由于无线网络的系统决策依赖于从各个节点接收到的数据,而网络的通信具有概率特性且接收到的数据具有不同的可信级别,因此,本文提出基于数据的概率可信性分析方法。在该方法中,节点的通信概率与收到的数据的可信级别概率被分开,使得新提出的分析方法具有更好的可扩展性并且更适用于对无线网络应用的分析。
黄滟鸿[7]（2014）在《面向实时嵌入式系统的中断语义理论研究》文中提出随着计算机的发展,实时嵌入式系统被广泛应用于各个行业。相较于通用计算系统,嵌入式系统对安全性、可靠性、实时性以及稳定性都提出了更高的要求。它不仅要求系统实现逻辑正确,而且要求任务运行时可满足相应的时间限制。在实时嵌入式系统中,为了让系统可以及时地与外界环境进行交互,人们引入了“中断机制”。中断机制作为系统与外部设备连接的桥梁,使得系统可以随环境的变化而动态地、实时地做出相应的响应。然而,中断产生的随机性与不确定性却为系统埋下了内存安全和时间安全等方面的隐患。近年来,众多学者从不同的角度、采用不同的方法对中断进行了研究,其目的就是为了在保证中断机制正常运行的同时,提高此类系统的安全性指标。本文以实时嵌入式系统中的中断机制为研究对象,在程序统一理论的指导下,提出可描述实时嵌入式系统的中断行为的抽象建模语言。该语言引入了时间、概率等信息,通过刻画程序的行为研究中断给程序行为、系统表现带来的时间安全问题。该语言中引进的概率程序算子结合了多种概率模型,不仅能更细致、准确地刻画中断环境的不确定性,也可以帮助系统设计者、开发者加深对中断的了解,减少中断对此类系统带来的安全隐患,显着提高此类系统的安全性。本文将提出的研究方法应用于汽车电子领域,结合基于AUTOSAR OS规范的操作系统与汽车发动机管理系统应用案例,验证了该研究方法的可行性与有效性。本文的研究方法有效地提高了系统设计、实现以及测试过程的工作效率,对实时嵌入式系统的开发起了重要的辅助作用。本文的主要内容与贡献包括：一、本文提出了三种用以描述实时嵌入式系统的中断机制的形式化语言：中断建模语言IML、带卫兵的中断建模语言gIML以及带概率的中断建模语言pIML；三种语言的依次提出展示了本文对中断的研究过程。gIML是IML的扩展,pIML是gIML的扩展；三种语言可用于研究不同抽象层次的中断机制。它们不仅包括了常见的程序,如带时间的赋值程序、串行组合程序,而且包括关于中断特征的程序,如解除屏蔽程序、屏蔽中断程序、概率打断程序。pIML中引入的概率信息,使得我们不仅能对中断行为进行定性分析,还能对中断行为进行更为准确、精致的定量分析。二、本文给出了三种中断建模语言的两种语义模型：操作语义和指称语义。操作语义的迁移规则直观地模拟了程序是如何运行的。而指称语义从更为抽象的层次利用数学论域中的对象来描述程序的行为。两种语义都包涵了时间、概率信息,分析与讨论了系统在中断环境下的时间安全问题。本文在操作语义框架下通过互仿真定义了程序的等价性,并推导出一些关于中断的代数规则。同时,这些代数规则也在指称语义的框架下得到了证明。本文还研究了操作语义与指称语义的一致性问题。三、本文提出了带概率的中断建模语言pIML的应用。pIML包含了时间、概率信息,从定量的角度清晰地展示了中断发生对程序运行造成的影响。本文利用工具Maude仿真了pIML的概率操作语义,仿真结果可以协助程序员观察与分析程序运行的状况。pIML的概率指称语义也可以直接用于计算程序在中断影响下的运行时间与对应概率。本文提出可以引入概率分布函数来模拟实际应用场景的中断环境,从而对程序行为进行定量分析,帮助程序员预测系统的表现。本文还以基于AUTOSAR OS规范实现的操作系统与汽车发动机管理系统为例,通过pIM（?）L描述的程序来展示中断的准时发生对实时系统的重要性。
朱龙飞[8]（2014）在《混成建模语言HyML及其语义理论研究》文中进行了进一步梳理信息物理融合系统是一种融合了感知、计算、通信、控制能力的物理设备系统,通过系统内物理进程与计算进程相互影响的反馈循环从而实现自治。随着信息技术的更新换代与不断发展,信息物理融合系统的应用领域也不断扩展,大到核工业复杂控制系统、国家智能电网等涉及国家乃至世界的复杂系统,小到自主感控与计算的植入式家庭医生设备、自动巡航系统。这些系统与我们的正常生产与生活密切相关,一旦出现问题可能会带来不可估量的损失。一般来说,这类系统的构成比较复杂,它的正确性不仅仅对某单一组件有要求,也与同一类组件之间、不同类组件之间的交互是否正确有关。相对于一般的软件系统,信息物理融合系统的异构性、交互的复杂性、一定的可预测性以及更高的安全性需求给这类系统的描述、设计、分析和验证带来了更大的挑战。如何保证信息物理融合系统的正确性成为国内外工业界和学术界的难题之一。在计算机科学领域里,程序理论和代数方法可以用来保证软件产品的正确性,在其理论指导下,有很多成功的开发实例。但是基于程序理论的开发或者验证方法多数针对离散系统,由于物理设备连续状态的引入,传统的方法不再奏效。控制领域有多年借用数学建模的方法去仿真模拟物理系统的经验,但是其对信息系统的关注研究较少。对于这类系统来说,只是单就某一类组件进行分析,即使这一类组件本身的研究已经很到位,但也极有可能是不安全的。要保证信息物理融合系统系统的正确性首先要解决的是如何将以一定方式交互的物理设备和信息系统融合在同一框架下做分析推理。本文提出了一种针对信息物理融合系统的基于事件交互机制的新型建模语言HyML,使得信息物理融合系统中的各个元素能够在同一个框架内进行分析推理。在程序统一理论的指导下,我们研究了混成建模语言HyML的指称语义以及代数语义,帮助程序开发人员从不同的角度认识理解语言,并且证明了代数语义相对于指称语义的一致性。然后给出了混成程序的规范型,并支持利用可证代数规则对程序进行简化。最后研究了利用可证代数规则进行程序分解的方法。本文针对信息物理融合系统的描述语言的研究为复杂系统语言研究及语义探索奠定了理论基础,并且展示了代数方法在语言理论研究中的重要性。本文的主要内容包括：·从信息物理融合系统的建模需求出发,提出了一种基于事件的新型建模语言HyML,该语言不仅可以刻画信息物理融合系统的异构功能性组件,而且实现了信息系统与物理系统交互模式的融合。新型的卫兵结构不仅继承了离散部分的交互模式即事件卫兵,还引入了混合卫兵支持连续部分与其他部分之间的交互。·给出了HyML语言面向观察的指称语义模型,研究了HyML的代数语义模型,并且证明了代数语义相对于指称语义的一致性,从而增强了我们运用代数规则完成程序转化的可靠性。·探索了在HyML框架内利用代数语义理论辅助可信系统开发的具体方案。提出了混成程序的规范型,并证明了所有混成程序都可以转化为规范型。提出了一种粗粒度的程序分解框架,利用可证代数规则将初始规范转换为物理程序与控制程序的并发组合,控制程序部分可进一步应用于后续的开发过程。
吴晓峰[9]（2014）在《面向无线网络的形式化方法研究》文中研究说明无线网络己经被广泛运用于人们日常生活中的许多方面。尤其是在缺少固定基础设施的情况下,无线网络和无线技术是合适的通信解决方案,并且正在被广泛应用于实现信息传输的各种通讯场景中。构成无线网络的基础物理器件是无线网络节点设备,这些无线节点设备为无线网络应用的实现提供了基础的通信功能。无线网络节点设备通常是以无线电波为载体进行广播式的信息发送,这种无线网络的广播信息发送模式与传统的有线以太网络中的全局广播信息发送模式有所不同。在无线网络中,信息数据的广播发送是局部的,也就是说每个无线节点所发送的信息的传输范围是有限的,只有那些处于节点传输半径覆盖范围内的部分接收节点才能够接收到所对应的节点广播发送的信息。受限于有限的信息传输范围,为了使得不在传输范围内的两个无线节点之间能够实现交互,就需要借助其他的中间节点来建立起一条能够传输信息的路由路径。路由协议是实现无线网络中路由路径的建立和维护的一种重要机制,主要是通过各种报文信息在无线网络中的广播来建立路由路径。形式化方法被认为是对无线网络系统进行描述和验证的一种可行并且合适的方式。本文研究面向无线网络系统的形式化方法。我们主要研究无线网络中与通信交互相关的无线网络特性,包括无线节点之间的广播通信交互行为以及无线网络中路由协议建立路由路径的机制。无线网络中无线节点之间的通信实现了无线网路中最根本的信息交互功能。我们考虑无线广播通信的各种物理特征,包括了无线节点的位置、通信范围、通信频率等物理因素。针对通信交互等无线节点底层物理行为的形式化描述和建模通常采用基于通信交互的进程代数演算系统。因此,我们扩展无线系统演算引入无线网络卫兵选择的概念,基于程序统一理提出了无线演算系统的代数语义和指称语义。我们给出了一系列无线系统演算的代数规则,研究从代数语义计算推导出操作语义的方法。无线网络中的路由协议借助无线节点之间的通信交互实现了无线网络中的全局信息交互。针对无线网络中路由协议在路由建立和维护路由路径时的特点,我们主要考虑路由协议实现路由时的各种路由信息数据的处理机制。因此我们采用形式化描述语言对无线网络AODV路由协议进行形式化建模、分析和验证工作并且将底层的无线节点的通信交互行为抽象为针对变量的赋值效果。通过使用这种在更高层次的抽象描述方式,我们能够更直接地分析无线网络路由协议的本质特性。本文的主要贡献包括：·我们提出了无线系统演算的代数语义,给出了一组用于描述无线系统演算并行组合线性展开的代数规则,并且定义了无线网络系统的规范型。借助无线网络系统的规范型,我们给出了从代数语义计算生成操作语义的方法,并且证明了代数语义和操作语义的一致性,从代数语义的角度保证了操作语义的正确性和完备性。我们使用重写逻辑工具Maude实现了从代数语义自动计算操作语义的过程。我们提出了无线系统演算的指称语义,引入了无线网络执行状态和执行轨迹的概念用来描述无线网络的行为。基于指称语义模型,我们证明了无线网络系统的代数性质。·我们使用形式化建模语言Z对无线网络中使用的AODV路由协议进行建模,并且使用基于Rely/Guarantee方法的形式化验证技术证明了协议的性质。通过形式化建模语言,我们在建模过程中消除了路由协议相关文档中自然语言描述的二义性。我们使用程序变量赋值的效果来描述无线节点之间的通信交互。我们对使用形式化语言Z构建的协议模型进行重写得到基于共享变量并行程序语言的改进协议模型。以共享变量并行程序所描述的路由协议形式化模型为基础,我们使用Rely/Guarantee推理规则证明了路由协议建立的路由路径不存在路由环路等性质。
栾天骄[10]（2013）在《实时系统规范语言STeC的Maude语义模型和静态分析设计及其工具实现》文中研究说明信息系统融合系统的网络化、系统化和信息化等特性使得软件系统的复杂程度不断增加。尤其是时间和空间等物理元素的引入使得经典的建模方法无法满足其时空一致性需求,最近陈仪香教授引入了实时系统的规范语言Spatio-temporal Consistence Language for Real-time Systems（STeC）对时空一致性进行建模和分析。本文从形式化角度对STeC语言进行研究,使用重写逻辑建立了STeC语言的Maude语义,利用Maude解释器对STeC模型进行仿真,开发了工具对STeC模型进行时空一致性的静态分析,搭建了STeC语言的一体化工具,在此基础上对中国高铁等例子进行建模分析和逻辑推理。首先,本文提出了STeC语言的Maude语义模型。Maude语义主要使用关系等式理论和重写逻辑理论进行定义,其中对离散时间进行建模分析。通过有效的拓展,本文将STeC语言转化为可执行的基于Maude的形式化描述,使用Maude自动推导功能,验证STeC模型的逻辑正确性。其次,本文对STeC模型进行静态分析,包括词法、语法分析,时空一致性分析和时钟满足性分析。借助目前主流的词法分析器Flex和语法分析器Bison设计和实现了STeC的词法以及语法分析部分,并且利用语法文件中定义的文法结构对时空一致性以及时钟满足性等性质进行了分析和验证。最后,本文将上述功能整合到一起,建立了一个一体化工具,称为实时系统规范语口STeC工具软件；该工具既可以对STeC模型进行静态分析,也可以后台调用Maude解释器运行STeC语言的Maude语义,对STeC模型进行逻辑正确性和形式化分析。本文对高铁G147的运行时刻表进行建模,通过一体化工具对其进行分析和推理验证,结果说明该工具是有效的和合理的。
二、陈仪香教授与计算语义模型研究（论文开题报告）
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
本文主要提出一款精简64位RISC处理器存储管理单元结构并详细分析其设计过程。在该MMU结构中,TLB采用叁个分离的TLB,TLB采用基于内容查找的相联存储器并行查找,支持粗粒度为64KB和细粒度为4KB两种页面大小,采用多级分层页表结构映射地址空间,并详细论述了四级页表转换过程,TLB结构组织等。该MMU结构将作为该处理器存储系统实现的一个重要组成部分。
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
三、陈仪香教授与计算语义模型研究（论文提纲范文）
（1）空天运输遥操作系统净评估与可信度认定研究（论文提纲范文）
| 摘要 |
| abstract |
| 第一章 绪论 |
| 1.1 课题背景及研究目的和意义 |
| 1.1.1 课题研究背景 |
| 1.1.2 课题研究目的和意义 |
| 1.2 空天运输遥操作系统发展现状 |
| 1.3 航天信息系统故障导致的灾难 |
| 1.4 信息系统质量评估国内外研究现状 |
| 1.4.1 国外研究现状 |
| 1.4.2 国内研究现状 |
| 1.5 论文研究内容与结构安排 |
| 1.5.1 研究内容 |
| 1.5.2 结构安排 |
| 第二章 遥操作系统净评估理论基础 |
| 2.1 信息系统可信性定义 |
| 2.1.1 面向用户主体的定义 |
| 2.1.2 面向系统客体的定义 |
| 2.2 信息系统质量模型 |
| 2.2.1 面向过程的系统质量模型 |
| 2.2.2 面向产品的系统质量模型 |
| 2.3 信息系统相关的标准 |
| 2.3.1 国际通用标准 |
| 2.3.2 国家军用标准 |
| 2.4 净评估理论 |
| 2.4.1 净评估的内涵及特性 |
| 2.4.2 净评估研究现状 |
| 2.5 探月工程嫦娥系列任务遥操作系统介绍 |
| 2.5.1 业务流程介绍 |
| 2.5.2 质量控制措施 |
| 2.6 遥操作系统净评估要素 |
| 2.6.1 战略自动化 |
| 2.6.2 文本数据挖掘 |
| 2.6.3 形式化方法 |
| 2.6.4 软件测试 |
| 2.7 本章小结 |
| 第三章 遥操作系统净评估指标体系构建及其形式化规约 |
| 3.1 形式化方法—Z语言 |
| 3.2 遥操作系统净评估指标体系结构的形式化规约 |
| 3.3 遥操作系统净评估指标内容及其形式化规约 |
| 3.3.1 软件过程文档 |
| 3.3.2 国家军用软件标准 |
| 3.3.3 空天运输遥操作系统领域特性 |
| 3.4 本章小结 |
| 第四章 遥操作系统可信证据采集平台 |
| 4.1 动态可信证据采集 |
| 4.1.1 功能类可信证据采集 |
| 4.1.2 性能类可信证据采集 |
| 4.2 静态可信证据采集 |
| 4.2.1 源代码类可信证据采集 |
| 4.2.2 文档类可信证据采集 |
| 4.2.3 环境类可信证据采集 |
| 4.3 本章小结 |
| 第五章 净评估指标权重计算 |
| 5.1 指标赋权法 |
| 5.1.1 单一赋权法 |
| 5.1.2 单一赋权法的组合方法 |
| 5.2 遥操作系统净评估指标赋权方法 |
| 5.2.1 AHP和 EWM的组合优化 |
| 5.2.2 不同赋权方法对比指标 |
| 5.3 构建对比判断矩阵的工程方法 |
| 5.3.1 航天信息资源国产化 |
| 5.3.2 航天系列任务信息传承与长期保存 |
| 5.3.3 知识本体构建评估知识库 |
| 5.3.4 空天运输遥操作系统净评估虚拟仿真环境 |
| 5.4 遥操作系统净评估指标赋权 |
| 5.4.1 权重计算 |
| 5.4.2 结果分析 |
| 5.5 本章小结 |
| 第六章 遥操作系统净评估 |
| 6.1 空天运输遥操作系统的设计和实现 |
| 6.1.1 开发环境搭建 |
| 6.1.2 跨平台系统设计 |
| 6.2 嫦娥四号遥操作系统实际工程应用 |
| 6.3 嫦娥五号遥操作系统净评估 |
| 6.4 本章小结 |
| 第七章 结论和展望 |
| 7.1 研究总结 |
| 7.2 研究展望 |
| 参考文献 |
| 致谢 |
| 个人简历、在学期间的研究成果及发表的学术论文 |
| 附录 A Z语言词汇表 |
| 附录 B 探月工程嫦娥系列任务 |
| 附录 C 开源的证据采集工具 |
| 附录 D 常见的指标赋权方法 |
（2）协作式工业控制系统建模、分解及验证技术研究（论文提纲范文）
| 摘要 |
| ABSTRACT |
| 第一章 绪论 |
| 1.1 研究背景 |
| 1.2 问题与挑战 |
| 1.2.1 工业控制系统的安全性问题 |
| 1.2.2 工业控制系统的复杂性挑战 |
| 1.3 国内外研究现状及相关工作 |
| 1.3.1 工业控制系统验证方面的相关研究 |
| 1.3.2 系统设计开发方法方面的相关研究 |
| 1.4 本文的主要工作及贡献 |
| 1.5 本文的组织结构 |
| 第二章 基本概念及准备知识 |
| 2.1 IEC 61131-3 标准 |
| 2.1.1 IEC 61131 标准 |
| 2.1.2 可编程逻辑控制器 |
| 2.1.3 IEC 61131-3 软件模型 |
| 2.1.4 PLC运行机制 |
| 2.1.5 PLC编程语言 |
| 2.2 程序切片技术 |
| 2.2.1 程序切片原理 |
| 2.2.2 程序切片简单示例 |
| 2.3 模型检测技术 |
| 2.3.1 模型检测的基本流程 |
| 2.3.2 模型检测简单示例 |
| 2.4 本章小结 |
| 第三章 协作式工业控制系统建模语言 |
| 3.1 设计动机与要求 |
| 3.2 CICSML建模语言 |
| 3.2.1 设计思想 |
| 3.2.2 基本概念 |
| 3.2.3 抽象语法 |
| 3.3 CICSML建模 |
| 3.3.1 建模流程 |
| 3.3.2 建模案例 |
| 3.4 本章小结 |
| 第四章 协作式工业控制系统模型分解方法 |
| 4.1 概要说明 |
| 4.2 分解可行性判定 |
| 4.3 资源分配 |
| 4.4 模型拆分方法 |
| 4.4.1 问题分析 |
| 4.4.2 任务拆分算法 |
| 4.5 模型协作关系生成方法 |
| 4.5.1 协作原理 |
| 4.5.2 通信语句生成方法 |
| 4.6 应用案例 |
| 4.6.1 集中建模 |
| 4.6.2 模型分解 |
| 4.6.3 协作关系分析 |
| 4.7 本章小结 |
| 第五章 基于性质规范挖掘的轻量级验证方法 |
| 5.1 引言 |
| 5.2 验证方法 |
| 5.2.1 基本形式 |
| 5.2.2 迭代验证流程 |
| 5.3 工具实现 |
| 5.4 应用案例 |
| 5.4.1 简单示例 1:转换开关 |
| 5.4.2 简单示例 2:两数排序 |
| 5.4.3 实例研究 |
| 5.4.4 性能评估 |
| 5.5 讨论:与传统验证方法对比 |
| 5.5.1 与仿真和测试相比 |
| 5.5.2 与模型检测相比 |
| 5.6 局限性 |
| 5.6.1 方法自身的局限性 |
| 5.6.2 当前实现的局限性 |
| 5.7 本章小结 |
| 第六章 带过去时态的线性时态逻辑规范挖掘方法 |
| 6.1 简介 |
| 6.2 带过去时态的线性时态逻辑 |
| 6.2.1 带过去时态的线性时态逻辑语法 |
| 6.2.2 带过去时态的线性时态逻辑的限界语义 |
| 6.2.3 对比一般纯未来时态的线性时态逻辑 |
| 6.3 挖掘方法 |
| 6.3.1 方法概要 |
| 6.3.2 核心算法 |
| 6.4 优化策略 |
| 6.4.1 公共子结构缓存加速策略 |
| 6.4.2 并行加速策略 |
| 6.5 工具实现与评估 |
| 6.6 本章小结 |
| 第七章 总结与展望 |
| 7.1 本文工作总结 |
| 7.2 不足之处与未来工作展望 |
| 附录A 语法定义 |
| A.1 CICSML的ANTLR语法定义 |
| A.2 带过去时态的线性时态逻辑的ANTLR语法定义 |
| 参考文献 |
| 致谢 |
| 攻读博士学位期间发表论文和科研情况 |
（3）软件定义网络的形式化建模与验证（论文提纲范文）
| 摘要 |
| Abstract |
| 第一章 绪论 |
| 1.1 研究背景和动机 |
| 1.2 研究现状和相关工作 |
| 1.3 本文的主要工作 |
| 1.4 本文的组织结构 |
| 第二章 背景知识 |
| 2.1 软件定义网络 |
| 2.2 虚拟局域网 |
| 2.3 形式语言与形式语义 |
| 2.4 NetKAT语言 |
| 2.5 本章小结 |
| 第三章 网络编程语言PDNet |
| 3.1 NetKAT的第二种操作语义 |
| 3.2 PDNet语言 |
| 3.3 NetKAT与PDNet对比与证明 |
| 3.4 本章小结 |
| 第四章 SDN系统建模框架 |
| 4.1 框架概述 |
| 4.2 转发设备模型 |
| 4.3 主机模型 |
| 4.4 攻击者模型 |
| 4.5 本章小节 |
| 第五章 Floodlight控制器的建模与验证 |
| 5.1 Floodlight基本模块 |
| 5.2 Floodlight模型 |
| 5.3 系统模型与验证 |
| 5.4 本章小节 |
| 第六章 TopoGuard安全机制的建模与验证 |
| 6.1 Topo Guard机制 |
| 6.2 Topo Guard模型 |
| 6.3 系统模型与验证 |
| 6.4 改进的Topo Guard建模与验证 |
| 6.5 本章小节 |
| 第七章 总结与展望 |
| 7.1 本文工作总结 |
| 7.2 后续工作展望 |
| 参考文献 |
| 致谢 |
| 研究成果 |
（4）基于重写逻辑的嵌入式操作系统建模与验证技术研究（论文提纲范文）
| 摘要 |
| abstract |
| 第一章 绪论 |
| 1.1 引言 |
| 1.2 研究现状与相关工作 |
| 1.3 本文研究内容 |
| 1.4 组织结构 |
| 第二章 基本概念和预备知识 |
| 2.1 重写逻辑和K框架 |
| 2.2 模型检测 |
| 2.3 可达性逻辑 |
| 2.4 精化关系 |
| 2.5 本章小结 |
| 第三章 OSEK OS规范模型与可达性检查 |
| 3.1 OSEK OS规范 |
| 3.2 OSEK OS规范的语义模型 |
| 3.2.1 语法定义 |
| 3.2.2 系统状态 |
| 3.2.3 任务调度的语义模型 |
| 3.2.4 资源管理的语义模型 |
| 3.2.5 事件管理的语义模型 |
| 3.2.6 错误处理的语义模型 |
| 3.3 操作系统规范的可达性分析 |
| 3.4 本章小结 |
| 第四章 OSEK OS实时性规范模型与约束提取 |
| 4.1 OSEK OS时间管理机制 |
| 4.2 时间管理机制语义模型 |
| 4.2.1 系统状态的扩展 |
| 4.2.2 报警机制的语义模型 |
| 4.2.3 中断机制的语义模型 |
| 4.2.4 系统服务执行时间 |
| 4.2.5 应用程序执行时间 |
| 4.3 规范模型可靠性分析 |
| 4.4 基于规范模型的测试用例生成 |
| 4.4.1 OSEK OS规范约束定义 |
| 4.4.2 OSEK OS测试用例生成 |
| 4.5 本章小结 |
| 第五章 OSEK OS内核语义模型与正确性分析 |
| 5.1 操作系统内核语义 |
| 5.1.1 抽象ARM指令的操作语义 |
| 5.1.2 抽象C语言的操作语义 |
| 5.1.3 混合语言的操作语义 |
| 5.1.4 基于操作语义的混合程序验证 |
| 5.2 内核模型的规范一致性检查 |
| 5.2.1 并发系统的规范一致性定义 |
| 5.2.2 规范一致性检查方法 |
| 5.2.3 调度机制的规范一致性检查 |
| 5.3 本章小结 |
| 第六章 OSEK OS及应用的自动化验证 |
| 6.1 系统规范的验证 |
| 6.2 系统内核的验证 |
| 6.2.1 操作系统内核的K语义 |
| 6.2.2 系统内核可达性验证 |
| 6.3 系统应用的验证 |
| 6.3.1 引擎控制系统的仿真 |
| 6.3.2 操作系统应用的验证 |
| 6.4 验证结果与分析 |
| 6.5 本章小结 |
| 第七章 总结与展望 |
| 7.1 总结 |
| 7.2 下一步工作 |
| 参考文献 |
| 致谢 |
| 发表论文和科研情况 |
（5）基于STeC的空天地一体化地球观测的验证与仿真（论文提纲范文）
| 摘要 |
| ABSTRACT |
| 主要符号对照表 |
| 第一章 绪论 |
| 1.1 研究背景 |
| 1.2 研究现状 |
| 1.2.1 空天地一体化对地观测研究现状 |
| 1.2.2 形式化方法研究现状 |
| 1.3 本文工作与主要贡献 |
| 1.4 组织结构 |
| 第二章 预备知识 |
| 2.1 空天地一体化网络 |
| 2.2 实时系统规范语言STeC |
| 2.3 航天任务仿真工具STK |
| 2.4 本章小结 |
| 第三章 地球观测任务的建模 |
| 3.1 任务需求描述 |
| 3.2 STeC语言的领域化 |
| 3.3 模型的建立 |
| 3.3.1 场景一 |
| 3.3.2 场景二 |
| 3.4 本章小结 |
| 第四章 模型性质的验证 |
| 4.1 基于STeC工具的模型检查和初步验证 |
| 4.1.1 STeC工具介绍 |
| 4.1.2 模型语法语义检查 |
| 4.1.3 模型时空一致性验证 |
| 4.2 基于UPPAAL工具的模型检测 |
| 4.2.1 UPPAAL工具简介 |
| 4.2.2 STeC模型到时间自动机的转化 |
| 4.2.3 模型性质验证 |
| 4.3 本章小结 |
| 第五章 地球观测任务的仿真 |
| 5.1 STK在航天任务仿真中的应用 |
| 5.2 仿真工具的设计与实现 |
| 5.2.1 仿真工具的设计 |
| 5.2.2 仿真工具的实现 |
| 5.3 工具功能展示 |
| 5.4 本章小结 |
| 第六章 地球观测任务规划 |
| 6.1 地球观测任务规划问题描述 |
| 6.2 STeC语言中的时空曲线 |
| 6.3 基于STeC的地球观测任务规划 |
| 6.4 本章小结 |
| 第七章 总结与展望 |
| 7.1 论文总结 |
| 7.2 下一步工作 |
| 参考文献 |
| 致谢 |
| 发表论文和科研情况 |
（6）基于质量演算的无线网络形式语义与分析（论文提纲范文）
| 摘要 |
| Abstract |
| 第一章 绪论 |
| 1.1 研究背景和动机 |
| 1.2 研究现状与相关工作 |
| 1.3 本文的主要工作与架构 |
| 第二章 基础理论和指导方法 |
| 2.1 进程演算 |
| 2.2 程序静态分析理论 |
| 2.3 形式语义学 |
| 2.4 程序统一理论 |
| 第三章 无线网络的质量演算CWQ |
| 3.1 CWQ演算的语法 |
| 3.2 CWQ演算的标签转移语义 |
| 3.2.1 进程层标签转移语义 |
| 3.2.2 网络层标签转移语义 |
| 3.3 CWQ演算的规约语义 |
| 3.4 和谐定理 |
| 3.5 案例研究 |
| 3.6 本章小结 |
| 第四章 CWQ演算的分析 |
| 4.1 CWQ演算的参数化模型 |
| 4.1.1 参数化模型的语法 |
| 4.1.2 参数化模型的语义 |
| 4.2 CWQ演算的可靠性分析 |
| 4.2.1 基于SAT的可靠性分析 |
| 4.2.2 案例模型 |
| 4.2.3 案例分析 |
| 4.3 CWQ演算的数据概率可信性分析 |
| 4.3.1 带有可信度级别标签的CWQ演算 |
| 4.3.2 基于数据的概率可信性分析 |
| 4.3.3 案例模型 |
| 4.3.4 案例分析 |
| 4.4 本章小结 |
| 第五章 带移动的质量演算mCWQ |
| 5.1 无线网络中的移动模型 |
| 5.2 mCWQ演算的语法 |
| 5.3 mCWQ演算的标签转移语义 |
| 5.3.1 进程层语义 |
| 5.3.2 网络层语义 |
| 5.3.3 语义性质 |
| 5.4 行为等价 |
| 5.5 案例研究 |
| 5.5.1 案例建模 |
| 5.5.2 案例分析 |
| 5.6 本章小结 |
| 第六章 mCWQ演算的指称语义 |
| 6.1 语义模型 |
| 6.1.1 可观察变量 |
| 6.1.2 健康条件 |
| 6.2 通信动作 |
| 6.3 延迟动作 |
| 6.4 带有质量谓词的组合接收动作 |
| 6.5 进程语义 |
| 6.6 并行组合 |
| 6.7 本章小结 |
| 第七章 总结与展望 |
| 7.1 本文工作总结 |
| 7.2 后续工作展望 |
| 参考文献 |
| 致谢 |
| 攻读博士学位期间发表论文和参与科研情况 |
（7）面向实时嵌入式系统的中断语义理论研究（论文提纲范文）
| 摘要 |
| Abstract |
| 第一章 绪论 |
| 1.1 实时嵌入式系统的中断机制 |
| 1.2 中断的研究现状与相关工作 |
| 1.3 本文的指导方法 |
| 1.3.1 程序统一理论 |
| 1.3.2 语义理论的相关工作 |
| 1.4 本文的主要工作 |
| 第二章 中断建模语言IML |
| 2.1 IML描述的中断机制 |
| 2.2 IML的语法 |
| 2.3 IML的操作语义 |
| 2.3.1 操作语义的语义空间 |
| 2.3.2 操作语义的迁移规则 |
| 2.3.3 基于操作语义的程序等价性 |
| 2.4 本章小结 |
| 第三章 IML的指称语义 |
| 3.1 IML的指称语义 |
| 3.1.1 指称语义的语义空间 |
| 3.1.2 程序算子的指称语义 |
| 3.2 IML的代数规则及证明 |
| 3.3 IML的语义一致性 |
| 3.4 本章小结 |
| 第四章 带卫兵的中断建模语言gIML |
| 4.1 gIML的语法 |
| 4.2 gIML的语义 |
| 4.2.1 gIML的操作语义 |
| 4.2.2 gIML的指称语义 |
| 4.3 gIML的代数规则及证明 |
| 4.4 本章小结 |
| 第五章 带概率的中断建模语言pIML |
| 5.1 pIML的语法 |
| 5.2 pIML的概率语义 |
| 5.2.1 pIML的概率操作语义 |
| 5.2.2 pIML的概率指称语义 |
| 5.3 pIML的代数规则及证明 |
| 5.4 本章小结 |
| 第六章 中断建模语言的应用 |
| 6.1 仿真 |
| 6.1.1 语法解析 |
| 6.1.2 语义实现 |
| 6.2 程序运行时间与概率计算 |
| 6.3 概率统计在中断上的应用 |
| 6.4 示例 |
| 6.5 本章小结 |
| 第七章 总结与展望 |
| 参考文献 |
| 致谢 |
| 攻读博士学位期间发表论文和科研情况 |
（8）混成建模语言HyML及其语义理论研究（论文提纲范文）
| 附表 |
| 摘要 |
| Abstract |
| 第一章 绪论 |
| 1.1 信息物理融合系统 |
| 1.2 信息物理融合系统的研究现状 |
| 1.3 程序统一理论 |
| 1.3.1 基于字母表的指称语义 |
| 1.3.2 联接理论 |
| 1.3.3 语义表现形式 |
| 1.3.4 程序代数及其应用 |
| 1.4 本文的主要工作及创新点 |
| 1.5 论文结构 |
| 第二章 混成建模语言HyML |
| 2.1 交互方式 |
| 2.2 变量 |
| 2.3 卫兵结构 |
| 2.4 语法 |
| 2.5 案例研究 |
| 2.5.1 单摆 |
| 2.5.2 猫鼠问题 |
| 2.5.3 水箱控制 |
| 2.6 本章小结 |
| 第三章 混成建模语言的指称语义 |
| 3.1 高级时段演算 |
| 3.2 字母表 |
| 3.3 指称语义 |
| 3.3.1 基本元素 |
| 3.3.2 组合算子 |
| 3.4 本章小结 |
| 第四章 混成建模语言的代数语义 |
| 4.1 卫兵结构 |
| 4.2 混成语言的代数语义 |
| 4.2.1 赋值语句 |
| 4.2.2 事件释放语句 |
| 4.2.3 选择语句 |
| 4.2.4 等待语句 |
| 4.2.5 连续语句 |
| 4.2.6 串行组合 |
| 4.2.7 并行组合 |
| 4.3 本章小结 |
| 第五章 混成建模语言规范型 |
| 5.1 瞬时程序的代数规则 |
| 5.2 延时程序的代数规则 |
| 5.3 推导的代数规则 |
| 5.4 规范型 |
| 5.4.1 瞬时程序的条件规范型 |
| 5.4.2 混成程序的规范型 |
| 5.5 案例研究 |
| 5.6 本章小结 |
| 第六章 混成建模语言框架下的程序分解 |
| 6.1 问题的提出 |
| 6.2 案例分析 |
| 6.3 混成程序划分框架 |
| 6.3.1 程序划分规则 |
| 6.3.2 程序分解框架 |
| 6.4 本章小结 |
| 第七章 总结与展望 |
| 7.1 工作总结 |
| 7.2 后期工作的展望 |
| 参考文献 |
| 致谢 |
| 攻读博士学位期间发表论文和参与科研情况 |
（9）面向无线网络的形式化方法研究（论文提纲范文）
| 摘要 |
| Abstract |
| 第一章 绪论 |
| 1.1 背景和动机 |
| 1.2 无线网络形式化研究现状 |
| 1.3 本文的主要工作 |
| 第二章 基础理论和方法 |
| 2.1 形式语义 |
| 2.2 程序统一理论 |
| 2.3 Rely/Guarantee方法 |
| 2.4 形式化描述语言Z |
| 2.5 重写逻辑和Maude工具 |
| 2.6 本章小结 |
| 第三章 无线系统演算的代数语义 |
| 3.1 无线系统演算 |
| 3.2 卫兵选择 |
| 3.3 代数规则 |
| 3.4 首规范型 |
| 3.5 从代数语义计算操作语义的导出规则 |
| 3.6 基于Maude工具的语义与导出规则自动实现 |
| 3.6.1 语法实现 |
| 3.6.2 代数语义和首规范型实现 |
| 3.6.3 导出规则和操作语义的实现 |
| 3.7 本章小结 |
| 第四章 无线系统演算的指称语义 |
| 4.1 语义模型 |
| 4.2 发送节点 |
| 4.3 接收节点 |
| 4.4 卫兵选择 |
| 4.5 并行组合 |
| 4.6 代数性质 |
| 4.7 本章小结 |
| 第五章 无线网络AODV路由协议建模与分析 |
| 5.1 AODV路由协议 |
| 5.2 建模分析 |
| 5.3 路由请求发起操作 |
| 5.4 路由请求过程 |
| 5.5 性质分析 |
| 5.6 网络拓扑结构 |
| 5.7 本章小结 |
| 第六章 无线网络AODV路由协议验证 |
| 6.1 共享变量并行程序的Rely/Guarantee推理规则 |
| 6.2 基于共享变量并行程序的AODV模型 |
| 6.2.1 模型基本变量 |
| 6.2.2 路由请求过程 |
| 6.2.3 路由请求 |
| 6.2.4 路由回复 |
| 6.3 AODV路由协议性质验证 |
| 6.4 本章小结 |
| 第七章 总结与展望 |
| 7.1 本文工作总结 |
| 7.2 后续工作展望 |
| 参考文献 |
| 致谢 |
| 攻读博士学位期间发表论文和科研情况 |
（10）实时系统规范语言STeC的Maude语义模型和静态分析设计及其工具实现（论文提纲范文）
| 论文摘要 |
| 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静态分析工具软件设计书 |
| 参考文献 |
| 后记 |
| 攻读硕士学位期间发表论文和科研情况 |
四、陈仪香教授与计算语义模型研究（论文参考文献）
- [1]空天运输遥操作系统净评估与可信度认定研究[D]. 温晋杰. 石家庄铁道大学, 2020(04)
- [2]协作式工业控制系统建模、分解及验证技术研究[D]. 熊家文. 华东师范大学, 2020(11)
- [3]软件定义网络的形式化建模与验证[D]. 向霜晴. 华东师范大学, 2020(08)
- [4]基于重写逻辑的嵌入式操作系统建模与验证技术研究[D]. 朱晓冉. 华东师范大学, 2019(09)
- [5]基于STeC的空天地一体化地球观测的验证与仿真[D]. 杨志华. 华东师范大学, 2016(10)
- [6]基于质量演算的无线网络形式语义与分析[D]. 吴茜. 华东师范大学, 2016(08)
- [7]面向实时嵌入式系统的中断语义理论研究[D]. 黄滟鸿. 华东师范大学, 2014(01)
- [8]混成建模语言HyML及其语义理论研究[D]. 朱龙飞. 华东师范大学, 2014(10)
- [9]面向无线网络的形式化方法研究[D]. 吴晓峰. 华东师范大学, 2014(10)
- [10]实时系统规范语言STeC的Maude语义模型和静态分析设计及其工具实现[D]. 栾天骄. 华东师范大学, 2013(S2)