图搜索问题算法推导及形式化证明

用非形式化方法解决图搜索问题规模受限,对于一些复杂问题难以保证其正确性.传统的形式化方法推导图搜索问题难以理解且不易于形式化证明,现有形式化方法对这类问题的解决方案较少,在保证可靠性和正确性方面有欠缺.该文通过对图搜索问题的深入研究,开发出一种针对解决图搜索算法的新方法.首先刻画问题的规约,利用循环不变式的递归定义技术给出了开发图搜索问题循环不变式的新策略,在此基础上得到Apla抽象算法程序,并对该算法程序进行了形式化证明,再将已验证的Apla算法程序自动生成C++可执行程序,实现了从抽象的形式规约推演出具体的面向计算机的程序代码的程序精化完整过程.以拓扑排序和广度优先遍历为例对所提方法进行实验,实验结果验证了所提方法的有效性,不仅可以推导和证明已知算法,而且对未知算法的推导也有指导性作用.     

PAR平台中并发分布式事务处理机制及其应用研究

随着大数据、云计算和云服务等新技术的兴起,并发分布式计算作为这些新技术的基础,扮演着越来越重要的角色.在分布式计算中,数据的一致性难以得到保证,而事务处理技术能够有效解决该问题.为了提升PAR平台在高可靠应用程序的使用范围,在其建模语言Apla中融入了并发分布式事务处理机制,使得Apla语言不仅支持分布式数据库事务,还支持分布式非数据库事务.该文对Apla语言并发分布式事务处理机制进行了深入地研究,并将其应用在学生管理系统、在线购物系统等实际应用场景中.     

基于时间自动机的UML模型转换与验证研究

针对无法对UML模型进行形式化验证的问题,提出在元模型层将UML模型转换为时间自动机模型并进行验证的方法.形式化UML状态机的结构,抽象出UML和时间自动机的元模型,利用模型转换语言ATL对UML元模型和时间自动机元模型构造映射规则,实现UML模型到时间自动机模型的转换,在模型验证工具Uppaal中对转换结果进行形式化验证.最后进行实例研究,结果表明了此方法的有效性和先进性.     

基于Apla语言的虚拟现实建模机制研究

针对传统的脚本建模存在语言机制复杂繁琐、开发效率不高、可靠性难保证、建模阶段和交互阶段相互独立等问题,基于分划与递推(PAR)及其Apla抽象程序设计语言,设计与原Apla语言融合的虚拟现实建模语言机制.开发的Apla→MAXScript自动生成系统可以将抽象Apla程序转换成MAXScript脚本,并借助3DSMax...     

基于Web Service和多媒体数据库技术的PAR方法在线自学系统的设计与实现

设计并实现了一个PAR方法的在线自学系统.利用Web服务(Web Service)和多媒体数据库技术,将使用PAR方法开发算法程序设计的基本概念、算法设计语言Radl、抽象程序设计语言Apla以及设计和推导算法程序的方法学形象生动地呈现给学习者.最后介绍了利用算法程序设计支撑平台生成可执行算法程序的过程,以及该算法程序运行产生的结果.     

VSOS-HAM:基于Isabelle/HOL的OS内核硬件抽象模型和形式化验证方法研究

形式化方法是保证操作系统设计和实现的正确性的可靠方法.操作系统的形式化设计和验证过程仍然是一个极其复杂的过程.由于汇编语言过于底层,对其进行形式化验证的难度较大,如何有效地对汇编语言代码进行建模,便于对其语义和功效的正确性进行验证成为操作系统形式化领域的研究热点.在汇编级提出对操作系统的设计和实现的正确性进行形式化验证的方法.通过建立操作系统内核硬件抽象模型,形式化地描述指令的操作语义,在此内核硬件抽象模型的基础上界定影响系统状态变化的数据对象,建立系统状态空间,结合指令的操作语义的定义来描述系统的状态转换函数.在Isabelle/HOL定理证明器环境中描述该内核硬件抽象模型,以实现的可信操作系统VSOS为例,在汇编级对系统设计和实现的正确性进行验证.结果表明,该方法是可行的和高效的.     

异构分布式环境中的并行离群点检测算法

离群点检测是数据挖掘领域研究的热点之一,主要目的是识别出数据集中异常但有价值的数据点. 随着数据规模不断扩大,使得处理海量数据的效率降低,随即引入分布式算法. 目前现有的分布式算法大都用于解决同构分布式的处理环境,但在实际应用中,由于参与分布式计算的处理机配置的差异,现有的分布式离群点检测算法不能很好地适用于异构分布式环境. 针对上述问题,本文提出一种面向异构分布式环境的离群点检测算法. 首先提出基于网格的动态数据划分方法（Gird-based Dynamic Data Partitioning,GDDP）,充分利用各处理机的计算资源,同时根据数据点的空间位置信息进行数据划分,可有效减少网络通信. 其次基于GDDP算法,提出了异构分布式环境中并行的离群点检测算法（GDDP-based Outlier Detection Algorithm,GODA）. 该算法包括2个阶段：在每个处理机本地,按照索引中数据点的顺序进行过滤,通过2次扫描得到离群点候选集;判断候选离群点需要进行网络通信的处理机,使用较低网络开销得出全局离群点. 最后,通过大量实验验证了本文提出的GDDP和GODA算法的有效性.     

并发系统性质验证的一种形式化方法

采用Ｍａｎｎａ和Ｐｎｕｅｌｉ提出的命题线性时态罗辑ＰＬＴＬ作为并发系统的形式化规约语言、用ＰＬＴＬ公式描述系统的性质,给出并发系统性质验证的一种模型检验算法。     

二叉树排序非递归算法推导及形式化证明

非线性数据结构递归问题非递归算法的循环不变式的开发一直是形式化开发的难点.研究二叉树类非递归算法的推导及形式化证明方法,对二叉树排序算法进行推导,得出非递归Apla(Abstract Programming Language)算法及其精确而简单的循环不变式,然后用Dijkstra-Gries标准程序证明法证明算法的正确性,最后使用PAR平台C++程序自动生成系统自动生成C++代码.实例的实验结果简化了算法程序的推导和证明过程,对递归问题非递归算法的循环不变式的探测具有一定的借鉴意义,而且对非线性数据结构算法程序的推导及形式化证明具有指导意义.     

一种分布式过程模型及实例的优化方法

ADEPT模型具有分布式对称控制结构, 可以对控制流、数据流建模. 但由于ADEPT模型未被形式化描述, 所以无法判断过程模型及其实例的正确性.对ADEPT模型进行了形式化定义, 并结合实例状态机给出了过程实例的形式化描述; 在此基础上提出了用于验证过程模型正确性及过程实例一致性的优化方法.     

并发CHILL源语言调试器的研究

CHILL 语言的重要功能之一就是支持并发。并发的引入使得 CHILL 语言的调试变得十分困难。本文讨论了并发程序调试的困难与问题,研究了一般并发程序调试器应具有的功能,说明了我们借助实时扩展 UNIX 操作系统(RTU)所设计的并发程序调试器结构,找到了扩充的传统调试法用于并发程序调试时一些重要功能的实现方法。实验性地实现了 CHILL 并发源语言调试器。为消除探测影响,本文提出了硬件辅助软件调试法的设想。     

并发一致性问题及解决办法

维持系统的一致性是使系统正常运行的前提。该文叙述了面向对象分布式计算系统在引入并发之后可能带来的不一致问题及解决办法，从一致性理论出发，全面探讨了维持并发一致性的各种方案，提出了一套维持一致性的管理策略，设计并实现了一个并发控制算法。     

Verification of Concurrent Assembly Programs with a Petri Net Based Safety Policy

Concurrent programs written in a machine level language are being used in many areas but verifi- cation of such programs brings new challenges to the programming language community. Most of the stud- ies in the literature on verifying the safety properties of concurrent programs are for high-level languages, specifications, or calculi. Therefore, more studies are needed on concurrency verification for machine level language programs. This paper describes a framework of a Petri net based safety policy for the verification of concurrent assembly programs, to exploit the capability of Petri nets in concurrency modeling. The con- currency safety properties can be considered separately using the net structure and by mixing Hoare logic and computational tree logic. Therefore, more useful higher-level safety properties can be specified and verified.     

并发进程的一种跟踪与重演算法

并发程序的执行具有“不确定性”,即在同样的输入条件下并发程序的执行结果不一定相同。这使得传统的对于顺序程序的循环调试方法对于并发程序的调试不再有效。通过对并行程序的执行情况进行跟踪和重演,可以保证并发程序在相同的输入时候两次执行完全一样。本文分析了基于消息传递的并发程序执行模型,并给出了相应的跟踪和重演算法及其实现。     

分布式并行CAIP系统协同求解模型的研究

采用ＳＴＲＩＰＳ规划系统语法格式和图论知识,论述了基于知识的通用检测规划的领域模型、抽象分层规划以及相应的任务分解算法,从而建立了基于分布式并行处理智能检测规划集成开发平台ＩＤＰＩＰ的分布式并行协同求解模型．     

An Algorithm to Construct Concurrent Reachability Graph of Petri Nets

IntroductionPetrinetisausefultooltomodelaconcurrentsystemandanalyzeitsproperties.[1]ThetheoryofPetrinetshasdevelopedsoundlysinceitwasputforwardin1962andwaswidelyappliedtomanyfieldssuchasflexiblemanufacturingsystem,workflow,webservice,etc.[234]ReachabilitygraphisapowerfultooltoanalyzethedynamicpropertiesofPetrinets,bywhichthefiringofconcurrenttransitionsinPetrinetsisrepresentedinaserialmanner.Thatis,Petrinetitselfisaconcurrentmodel,whileitsreachabilitygraphisserial.Infact,concurrencyrelations…     

并发面向对象语言运行支撑系统

探讨如何为并发面向对象语言提供松散耦合分布式环境下的运行支撑环境．介绍我们为并发面向对象语言ＡＣ＋＋设计实现的分布式运行支撑系统ＤＲＴＳ．着重讨论了ＤＲＴＳ的设计思想和一些重要的实现技术．     

基于统一建模语言和多色集合的并行设计过程研究

在分析现有并行设计过程建模研究的基础上，提出了一种基于统一建模语言（UML）和多色集合理论的并行设计过程建模与分析方法，分析了并行设计活动的连接形式、UML活动图的基本建模元素和基本模型结构．采用多色集合理论，将UML活动图节点间的连接关系和基本模型结构形式化，结合基于特征的零件和工艺并行设计过程，建立了UML活动图模型，从模型简化、路径求取和时间消耗等方面定量地分析了并行设计过程，实现了该模型到多色集合围道矩阵的映射．研究表明，该方法具有面向对象且易于被非专业人员理解和使用的特点，可以为产品设计过程建立形式化模型．通过对设计活动进行布尔运算和定量分析，发现了影响产品设计进程的关键环节，从而为并行设计的组织和实施提供了理论指导．     

产品并行设计多Agent系统中任务分解和协调模型的研究

适当的任务分解是网络式分布环境下进行产品并行设计的关键。本文分析了产品并行设计中任务分解的原则 ,提出了一种进行任务分解的与或树方法 ,探讨了在多Agent系统中并行设计各任务间的组织方法和协调策略 ,并对KQML语言作了扩充 ,这些工作为减少多Agent间的通讯量 ,加强多Agent间的相互协作 ,提高产品并行设计效率奠定了基础     

BSP用于分布式系统的协议规范

ＢＳＰ是一种带有广播原语的分布式语言，能很好地支持分布式系统的消息传递。本文强调了ＢＳＰ在分布式系统协议规范方面的应用，并完成了对ＯＳＩ参考模型的网络协议以及数据库并控制的ｔｉｍｅｓｔａｍｐ协议的规范说明。