进程创建的语义及等价性

针对一个基于共享变量的带有进程创建的命令式语言,用变迁系统描述了它的结构操作语义,并用扩展的状态变迁迹模型定义了它的指称语义,在该模型下,状态变迁被区分为两种不同形式,分别表示发生在原进程和被创建进程中的状态变迁,这样便可以定义适当的语义复合运算,在对命令的指称进行复合时根据变迁类型的不同对变迁迹进行串行或交错连接,恰当地反映了进程的并发运行受创建命令在程序中的相对位置的限制,最后证明了这两个语义     

基于事件结构的SystemVerilog指称语义

本文利用形式化的方法对SystemVerilog的指称语义进行研究,采用EBES(extended bundle event strueture)作为抽象模型,以便更好的描述SystemvPrilog真并发的特点.我们的主要工作是:首先,通过对SystemVefilog语言的认真学习,从中抽取出一个尽可能多的包含其语法的真并发子集;其次,利用进程代数LOTOS描述其基于EBES模型的指称语义,以提供一个准确的、无二义性的SysteroVerilog文档,避免硬件设计中的逻辑性错误.     

GSOS算子下共变-异变模拟的公理刻画

进程的行为理论是进程演算研究的核心内容之一,其侧重于讨论进程间的行为等价和模拟关系。共变-异变模拟(Covariant-Contravariant Simulation,CC-模拟)的概念是对经典(互)模拟概念的推广,它通过区分动作类型,刻画了规范与实现对系统主动、被动和通讯动作在精化关系中的不同要求。行为关系的(前)同余性和公理刻画是进程演算代数特征的集中体现,它们对规范及实现的分析和推理至关重要。一般而言,行为关系(前)同余性的证明和公理系统的构造需要基于不同进程演算系统的结构化操作语义(Structural Operational Semantics,SOS)分别展开。为了避免这类研究工作中的重复劳动,学术界针对一般化SOS规则形式的元理论开展了研究,GSOS是其中被广泛研究的规则形式之一。文中在考量了动作类型的基础上,基于CC-模拟对GSOS规则形式做出扩充,提出了CC-GSOS规则类型,证明了CC-模拟相对于CC-GSOS算子具有前同余性,并给出了在这些算子下CC-模拟的可靠完备公理系统的一般性构造方法。     

Linux进程语义安全性检测的稳定模型

现有进程检测方法,检测的目标是系统调用的序列的排列关联,忽略了语义中潜在的异常。稳定模型是逻辑程序的语义模型,可以用以发现并修改逻辑程序的异常问题。该文以系统调用为基本检测点,采用逻辑程序描述进程的基本语义逻辑,用稳定模型表达进程的检测语义。系统定义进程的一系列安全语义规则,在进程执行中,计算安全语义规则与进程逻辑之间的稳定模型,得到安全语义的可计算性结论。论文最后,给出了一个Linux系统中的进程语义安全性检测的基本框架。     

基于进程代数的UML序列图的形式语义

UML序列图用于建模实例间动态交互过程．但UML规范并没有给出其形式化的动态语义，这不利于对模型进行形式化验证和证明。本文把序列图中的事件动作及其执行序列映射为进程代数中的进程表达式，利用进程代数语义框架来构建UML序列图的形式语义。首先，建立了序列图到进程代数的语义映射规则；然后用Plotkin风格的结构化操作语义给出并证明务件组合算子演绎规则；最后，归纳定义了算子次序约束条件并证明了其可终止性。     

基于本体知识推理的QoS区分服务策略精化方法

策略精化过程的主要难点在于网络的不同层次之间缺少统一的知识表示,且在不同层次的知识之间,缺少必要的映射和推理机制。为此,研究一种通过本体知识推理实现策略自动精化的方法。将本体工程引入策略网络系统,利用本体对网络知识进行定义,利用语义Web规则描述语言对底层策略行为进行语义描述,建立不同层次间的自动化推理机制。以QoS区分服务应用场景为例,实现了策略的自动精化过程。     

弱共变-逆变模拟的公理刻画

进程代数是并发理论研究的主流方向,是分析和描述并发与分布式系统的重要工具之一。模拟是进程代数中刻画精化关系的核心概念。共变-逆变模拟派生于通常的模拟关系,它区分动作的类型,直观上,表达了状态的行为数目越多但并不一定越好的事实。然而,该模拟关系忽略了可观测动作与内动作的区别。因此,给出一种弱共变-逆变模拟关系及其相应的公理刻画,并且建立了该公理系统的可靠性与基完备性,进而证明了该公理系统亦是ω-完备的。     

一种基于构件演算的主动构件精化方法

现代构件系统通常包含多个并发执行的主动构件,这使得验证构件系统的正确性变得十分困难.通过对构件演算进行扩展,提出了一种主动构件的精化方法.在构件接口层引入契约.契约使用卫式设计描述公共方法和主动活动的功能规约.通过一对发散、失败集合定义契约的动态行为,并利用发散、失败集合之间的包含关系定义契约间的精化关系.证明了应用仿真技术确认契约精化关系的定理.定义构件的语义为其需求接口契约到其服务接口契约的函数,以此为基础,可以通过契约的精化来证明构件的精化.给出了构件的组装规则.在构件系统自底向上的构造过程中,应用构件的精化方法和组装规则可以保证最终系统的正确性.     

UML类图的形式规约与精化研究

UML由于其广泛的应用和直观的图形化符号,成为了模型驱动工程的重要组成部分。但UML本身缺乏精确的形式语义定义,缺少对其模型精化关系的形式化规范定义,对UML模型进行形式验证变得尤为困难。UML类图作为描述系统结构的静态模型,不具备完整的形式语义。从UML类图的机械语义中抽取出形式规约,将UML类图中的结构和形式规约转换成定理证明器Coq中的机械语义定义。此外,还提出了类图的结构精化操作,将模型间的精化关系在Coq中进行形式化定义,并且对精化操作的原子操作进行机械验证,保证其精化前后系统的结构和语义保持一致。将UML和形式化方法相结合,为可验证的软件设计精化框架提供了理论依据。     

并行系统与并发程序设计语言的形式语义

语义学的研究目前活跃在二个领域中,一个是代数语义学,另一个是并发程序设计语言的各种形式语义的定义,本文主要介绍并发程序设计语言形式语义的基础,尤其是幂域理论、指称语义、操作语义、以及并发类型理论问题的讨论。     

并发行为推理的一种进程代数方法

在人工智能领域，动态系统的行为推理是一个非常热门的研究课题，其中最重要的问题是如何描述系统以及如何进行推理。在这一方面，人们已经提出很多形式化的方法。典型的描述动态系统的方法是引进一个取值随系统进化而改变的“事实”(fact)的集合，以及定义行为对“事实”的影响函数，以方便描述由执行特定的动作引起的状态转移；典型的推理问题是逻辑蕴涵，即寻找一种特定的适合描述动态系统的逻辑，在此逻辑下，系统状态的属性可以由有关系统的一些假设出发推导出来。     

基于LTS的Statecharts操作语义研究

Statecharts是一种用于复杂反应式系统行为的可视化规格语言。该文提出了一种基于标签变迁系统(LTS)的Statecharts操作语义描述方法，介绍了Statecharts及其项语法和一步语义，并基于进程代数描述Statecharts的并发行为，使用结构化的操作语义SOS规则描述Statecharts的组合语义，从而得到相应的LTS。     

并发系统中谓词行为图的行为时序逻辑表达

行为时序逻辑(TLA)组合时序逻辑与行为逻辑, 可以对并发系统进行描述与验证, 它引入动作和行为的概念, 使得系统和属性可用它的规约公式表示, 但存在用TLA描述复杂系统时TLA公式复杂且难以理解的不足。类似于状态转移图, 对于并发转移可以用谓词行为图进行图形化表示, 谓词行为图与行为时序逻辑规约具有相同的表达能力。介绍行为时序逻辑的语法、语义及简单推理规则, 用一个简单的实例说明使用谓词行为图去描述并发转移系统的有效性, 并用系统规约的TLA公式对谓词行为图表达能力进行证明, 表明两者具有等价性, 为描述和分析并发转换系统提供了一种可行的方法。     

递归数据传送进程的证明系统

本文提出了递归数据传送进程互模拟的证明系统，并证明了其可靠性和相对于数据推理的完备性，其中关键的推理规则是唯一不动点归纳法，这个结果一方面将Ｍｉｌｎｅｒ关于正则基本ＣＣＳ的公理系统推广到数据传送进程，另一方面将Ｈｅｎｎｅｓｓｙ与Ｌｉｎ关于有穷数据传送进程的证明系统推广到无穷进程。     

自动生成参数化同步系统的符号化模型

验证具有任意进程个数的并发系统是一个重要的具有挑战性的课题。那些包含任意多个类似的有限状态进程的并发系统出现在一些领域中，如硬件设计、通信协议和高速缓存一致性协议。当验证进程数目较大的问题时，传统的有限状态验证技术遭受状态爆炸问题。为了解决这个问题，提出了一些不同的技术来推理无限家族，如互模拟关系、定理证明和网络语法、抽象解释和搜索技术。尽管在一般情况下，验证参数化并发系统是不可判定的，但对于一些包含相同的有限状态进程的子系统，已     

高阶π-演算的互模拟理论研究

标签转移系统语义在早期的进程演算中取得了巨大的成功。基于标签转移系统，Milner与Park引入了互模拟的概念来描述进程间的等价性，互模拟从此成为整个进程演算中的理论基石。在经典的CCS进程演算中，标签转移系统用于描述进程的操作语义，然后在此基础上，互模拟概念通过如下方式被定义出来：两个进程若互模拟，不仅要满足任何一方的行为都要能够被另外一方匹配，同时要     

一种框架时序逻辑程序设计语言

本文提出了区间时序逻辑的一个变种——投影时序逻辑，给出了它的语法规则和语义定义，并建立了该逻辑系统的模型理论。在该逻辑系统中，我们引入了一个新的投影操作符(prj)。这使得我们不仅能够在不同的时间层次上控制进程的并行操作，而且可以以该操作符为基础定义顺序操作符(chop)和并行操作符(‖)。因此，该逻辑系统比区间时序逻辑具有更强的表达能力。同时，本文也给出了与投影操作相关的一些性质。     

基于进程演算和知识推理的安全协议形式化分析

安全协议的形式化分析是当前安全协议研究的热点,如何扩充现在已经成熟的理论和方法去研究更多的安全性质,使同一系统中各种安全性质在统一的框架下进行分析和验证是一个亟待解决的问题.进程演算是一强有力的并发系统建模工具,而结合知识推理可以弥补进程演算固有的缺乏数据结构支持的特点,以此提出了一个安全协议形式化分析的一般模型.基于此模型,形式化地定义了一些安全性质,给出了一个实例研究,并指出了进一步完善此模型的研究方向.     

补偿通信顺序进程的扩展及失败发散语义

补偿通信顺序进程(cCSP)是通信顺序进程用于长事务建模的扩展,可用来描述服务计算中的编制程序,比如WS-BPEL程序。目前,cCSP只有操作语义和基于迹的指称语义,对死锁和发散行为的推理支持不够。本文扩展了cCSP,引入新的组合操作子,给出扩展cCSP的失败发散语义;并根据该语义,给出新引入组合操作子的重要代数规则,用于语义的理解和佐证。最后,给出一个案例描述用于展示扩展cCSP。     

互逆主义程序精化——程序精化从形式化到半自动化的发展

Carroll Morgan的规则精化方法是一种典型的程序精化方法,是一种形式方法.本文用互逆主义逻辑对其进行了改造将其中的精化法则改造成为逻辑定理,以二层假言推理和小前提逆二层单准正向证明系统为推理规则,使得程序精化从形式化发展为半自动化.