一种扩展式动态环境演算范型的Petri网描述

为了以可视化的方式验证扩展式动态环境演算范型对移动协同中移动性和协作性的描述能力及描述语义的正确性,提出了一种扩展式动态环境演算范型的Petri网描述(PND).首先,给出基本演算实体的Petri网表示,用Petri网的顺序行为理论和并发行为理论中的变迁来表达任意动作,用库所来表达任意动作前后的各种环境状态及其变量.其次,给出演算实体的各操作语义关系的Petri网表示,并引入弧权重来刻画动作与其前后相关的环境、状态的相互作用关系.最后,引入了Petri网的合成理论,用简单Petri网合成法来构造动态复杂环境的模型.采用染色Petri网工具进行仿真,结果表明PND具有正确的描述语义,从而进一步为扩展式动态环境演算范型的有效性提供了有力的论证.     

κ-演算建模λ噬菌体的生活周期

κ-演算是一种描述生物蛋白质分子间相互作用的形式化语言.介绍了κ-演算的语法、语义以及λ噬菌体侵蚀大肠杆菌细胞的生物过程,提出了用κ-演算建模生物过程的一种方法,给出翻译规则,并在规则的指导下建模具体的生物过程.根据模型的特点,分析和研究κ-演算的表达能力和表达特点.     

检验实时系统的有序时段性质

模型检验是一种被广泛应用于对设计或系统正确性进行自动验证的技术。实时系统的性质包括瞬间性质和时段性质，显然后的检验要比前复杂得多。介绍了一类新的时段性质——有序时段性质，并检验了时间正则表达式的有序时段性质，最后分析了算法的复杂度，和相关工作进行了比较，并探讨了今后的工作方向。     

基于时序可中断π演算的BPEL和BPEL4People建模

为了形式化地定义BPEL和BPEL4People的语义,提出了一个π演算的变种——πit演算。相对于传统的π演算,πit演算可以描述中断事件和时间事件,从而拥有更好的建模表达能力。介绍了πit演算的语法和语义,定义了一类强互模拟关系来判定πit演算进程间的行为等价,然后使用πit演算对BPEL和BPEL4People的活动进行了建模。该形式化模型有助于在BPEL和BPEL4People程序的设计阶段对其可靠性和一致性进行验证。     

Modeling BPEL and BPEL4People with a Timed Interruptable n-Calculus

为了形式化地定义BPEL和BPEL4People的语义,提出了一个π演算的变种——πit演算。相对于传统的π演算,πit演算可以描述中断事件和时间事件,从而拥有更好的建模表达能力。介绍了7ci。演算的语法和语义,定义了一类强互模拟关系来判定πit算进程间的行为等价,然后使用πit。演算对BPEL和BPEL4People的活动进行了建模。该形式化模型有助于在BPEL和BPEL4People程序的设计阶段对其可靠性和一致性进行验证。     

分布式实时系统的一种转化设计方法

介绍了实时分布式系统的一种转化设计方法。系统的形式化需求规范用时段演算DC（Duration Calculus)描述，系统的设计用规范语言SL（Specification Language)表示。一组标准的转换规则可将系统从形式化需求规范转化为设计规范。系统设计的正确性可由转换过程本身得以保证。多用户多媒体通信系统的设计实例展示了转换设计方法的具体过程。     

用π-演算描述网络考试系统

在分析了基于W eb的网络考试系统需求的基础上,针对其具有多进程并发通讯的特点,采用π-演算对系统进行结构和功能的描述;在简单介绍π-演算的语法和操作语义的基础上,用进程表达式对整个系统进行形式化的描述;最后,通过实际编程实现,表明用π-演算描述这一类系统是非常适合的.     

具有真正并发语义的面向约束的实时进程代数

对于标准进程代数,通过加入因果和时间约束,对前缀操作项进行扩展,使得处理后的演算,保持定义简单,表达力增强,能够描述实时系统,并且具有真正并发语义。     

Web服务事务的动态补偿模型

对π-演算进行扩展,提出了作为Web服务事务动态补偿模型的Exπ-演算.该演算的补偿可随着Web服务的交互动态地建立起来,同时给出了结构同余关系和操作语义.为了保证事务的唯一性,定义了一个简单的类型系统.最后,将该简化的Exπ模型与静态补偿模型和并行动态补偿模型进行比较,结果表明:本演算比其他演算更灵活,表达能力更强.     

面向移动协同的扩展式动态环境演算范型研究

针对已有移动协同研究中尚缺乏既能描述移动性、又能描述协作性的演算系统,提出了一种扩展式动态环境演算范型(EMA).在对动态环境演算中的基本概念"环境"进行深入解析的基础上给出其在协同计算情境下的新语义,之后抽取刻画协同行为的基础动作A,并将A作为刻画协作性的基本单位.进而将动作行为理论引入到动态环境演算中,即在动态环境演算的基础上将A作为参与环境演算的基本实体,从而借助已有动态环境演算对移动性的描述能力来刻画移动协同计算的移动性,同时借助A刻画了移动协同中的协作性.最后给出了基于EMA的移动协同行为实例描述.较之经典动态环境演算,EMA弥补了不能刻画移动协同中的协作性缺陷,为移动协同理论框架的完善提供了依据,为移动协同应用的构建提供了一种新的理论基础.     

Seal演算与Boxed Ambient演算的关系分析

研究不同演算系统之间的逻辑结构和描述能力具有重要的理论意义.本文在系统分析Seal演算与BoxedAmbient演算的语法结构和语义规约系统的基础上给出了一些等价关系:通信等价、通信原语等价和代码移动等价.最后给出了Seal演算通信进程到Boxed Ambient演算通信进程的一种结构化转换方法.     

网上拍卖系统的π演算建模

在分析了基于WEB的网上拍卖系统的需求基础上,针对具有多进程并发通讯特点的该类电子商务系统,采用π演算对系统进行结构和功能建模．本文在简单介绍π演算的语法和语义基础上,用进程表达式对整个系统软件结构框架进行了形式化描述,并分析了π演算的建模能力．结果表明π演算在描述动态进程间的通讯所表现出的优势以及便于编程实现的技术特点,尤其适合这类电子商务系统的分析与设计。     

并行面向对象语言的Action演算语义

给出具体的Action演算EP的定义,并且应用该演算进一步给出一个并行面向对象语言的语义.通过这个例子,说明了Action演算簇在实际应用方面的描述能力.     

基于本体的多无人机系统语义互操作方法

引入基于领域本体的语义模型形式化建模方法,提出了多无人机交互描述的语义描述模型方法和交互配置的语义增强方法.设计了无人机本体UAV O和服务描述本体UAV OS,在OWL S（Ontology Web Language for Services）基础上扩展服务动态特性等的描述,可以为服务质量、服务状态和服务关系提供语义描述;扩展了对多无人机任务和动态配置、组合所需控制结构等的描述.为了实现多无人机应用配置的自动化和动态性,基于本体的语义增强方法可以用于配置管理,在匹配中引入高层次的语义增强匹配,对多无人机交互配置处理进行语义增强.在无人机综合仿真环境中进行了验证,结果表明,提出的基于本体的语义互操作方法能有效地支持多无人机应用交互和集成.     

入侵特征的时间语义逻辑及实现

在对ITL的定义和实时语义扩充进行描述的基础上，详细探讨了ISITL的特征，并给出了其模式图和MACIS事件的处理算法；最后对ISITL存在的优缺点进行了简要分析。     

马斯京根法——河道洪水演算的线性有限差解

常用的马斯京根法,是河道洪水演算的线性有限差解,它的入流条件应当是三角形的,选取时段长的条件应当是△t=K,在长河段的情况下,应当用分段连续演算。这一个计算系统,比较简便而且合理,宜于在实际中应用。如入流条件为矩形,也可以用有限差求解,其结果与纳须模型S-曲线解所得的十分相近.马斯京根法的积分解必然导致负效应,不宜应用,应用其特解纳须模型完全就可以了。但它提供了矩法,有意义。     

基于Pi演算的Android多线程程序的数据竞争检测

针对事件驱动机制下Android多线程程序的数据竞争问题,构造一个基于Pi演算的并发行为检测模型。利用扩展后的Pi演算对Android生命周期和多线程框架进行建模,得到形式化的行为模型;通过将安全约束抽象为形式化的IF-THEN规则,并利用Pi演算的性质进行进程演算和迁移,构建了检测模型;将动态检测与静态检测以相同的处理方式结合在检测模型中,并给出了并发行为检测算法和数据竞争检测的方法。理论分析和实验表明,本文所提出的方法具有线性的时间和空间复杂度,相比其他方法,在提高检测精确性的同时并没有牺牲检测的效率。     

构件化嵌入式软件设计的能耗性质分析与验证

从嵌入式软件设计模型层对构件化实时嵌入式软件系统中能耗相关性质进行研究,包括:扩展了实时接口自动机在能耗语义方面的描述能力,通过引入状态能量消耗率,建立了能耗接口自动机形式化模型以及自动机网络,用以建模嵌入式软件设计阶段系统构件及其构件组合的能耗行为特征;对能耗接口自动机网络的状态空间进行了形式化分析,构造了相应的可兼容整型空间的可达图,并在此基础上给出了最小能耗计算和最大能耗验证的算法.     

Cloud-SHOIQ: 描述逻辑SHOIQ的云扩展

经典描述逻辑是本体的重要表示方式,但不能表达不确定知识.分析了扩展描述逻辑表达不确定知识的研究现状及存在的问题,通过结合云模型(Cloud model)、描述逻辑SHOIQ及模糊逻辑提出了一种基于云的模糊描述逻辑C-SHOIQ表达不确定知识,给出了C-SHOIQ的语法、语义,并以实例分析了C-SHOIQ具有处理知识的随机性和模糊性的能力.给出了C-SHOIQ的推理方法,及映射C-SHOIQ知识库为经典SHOIQ知识库的改进规则.分析说明了C-SHOIQ是对模糊SHOIQ表达能力的扩展.