PAR平台中若干软件构件形式化验证技术研究

PAR平台是本团队研制成功的支撑软件形式化和自动化开发的软件平台。该平台充分体现了功能抽象和数据抽象的优越性,使得软件开发变得便捷和可靠,达到这一性能的关键要素是一批可重用软件构件。为保证整个软件平台的正确性和可靠性,确保其中软件构件的正确性和可靠性就显得十分重要。选取PAR平台中若干典型软件构件,用形式化方法对构件的语义进行形式化描述,并借助Coq定理证明系统,对构件的正确性进行形式化验证,大幅度提高了软件构件形式化验证的效率。

PAR平台从规约出发的算法推导与自动生成

简要介绍PAR方法及其支撑平台,使用PAR方法及其平台从规约出发形式化推导并生成了两个典型的算法程序。PAR方法及其平台使用一阶谓词逻辑表示功能规约,分划与递推来进行算法形式推导,各种转换系统来自动生成算法程序。这显著地提高了算法程序的正确性和开发效率,也有助于深刻地理解算法设计思想。

Transaction在PAR平台中的实现方法及应用研究

随着电子商务和金融软件应用日益广泛,提高这类软件系统的可靠性和安全性就显得特别重要。虽然能够提高这类软件可靠性的事务处理技术早在数据库管理系统中普遍使用,近几年在Java软件开发环境中也新增了事务处理接口JTA,但是在基于模型驱动架构设计的建模语言中嵌入事务处理机制的成功案例尚不多见。论文在已有体现模型驱动软件架构思想的PAR方法和PAR平台中,融入抽象事务处理机制,并使用融入了事务处理机制的PAR平台及其建模语言开发了具有事务处理功能的金融软件模型,通过PAR平台的模型自动转换工具生成了Java和SQL程序。实验证明融入了事务处理机制的PAR方法和PAR平台具有建模简单、实用,软件开发效率高,便于形式化推导和证明等特点。

面向PAR平台的测试用例生成技术研究

测试用例的设计是软件测试中一个具有关键作用的工作,如何用较少的测试用例达到比较高的覆盖度,是需要解决的主要技术问题。本文结合现代软件测试技术中的数据驱动测试和结构驱动测试设计技术,根据PAR平台转换工具的实际测试情况,设计了一种基于路径的测试用例自动生成算法,并在PAR平台的转换工具中应用实施,科学合理的测试用例设计为PAR平台转换工具测试的进行提供基础,测试达到了预期目的。

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

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

PAR平台数据库查询优化方案

数据库系统的查询优化技术是提高数据库系统效率的重要技术。当今Java和C++等主流程序设计语言依靠SQL语句,造成数据库系统中查询复杂、繁琐、效率低下、可靠性得不到保证等。针对上述问题,在PAR(Partition And Recur)平台数据库关系代数实现机制基础上,提出和实现基于关系代数的查询优化规则设计方法。这种设计不仅提高了数据库查询效率,也为高可靠数据库的形式化开发提供了依据。

新型Action泛型机制在PAR平台中的实现和应用研究

在软件开发过程中,开发语言中的泛型机制能够显著提高软件开发的效率和软件可靠性,但现有高级语言中一般只有类型和子程序(如过程、函数和方法等)作参数,限制了泛型机制的应用.该文对新型泛型机制进行深入探索,着重研究以action作为参数的泛型机制.在Apla→Java程序自动生成系统中实现了将Web服务作为Apla语言中的action参数的泛型机制,完善了Apla语言中的泛型安全的约束机制,成功地将新型泛型机制应用于PAR平台中.

PAR在数学算法中的应用

针对算法走进高中课堂的现状,提出使用PAR作为高中学习算法开发的主要平台,通过PAR形式化推导实现多项式和素数两个经典数学问题,表明PAR具有良好的数学和程序设计语言透明性,得到算法简短易于理解的同时也可以同时保证算法的正确性,理论分析和试验表明,PAR是学习算法开发的一个有效平台。

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

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

基于PAR的软件服务外包开发过程应用研究

软件外包中开发效率低、可靠性差的问题一直存在。PAR(Partition and Recur)方法及高可靠软件开发平台PAR平台,在提高软件开发效率和可靠性方面能够发挥很好的作用。本文将PAR方法和PAR平台应用于外包软件开发过程,使用PAR平台成功研发中软国际实训教材中软件外包案例,在软件开发效率和可靠性方面取得显著效果。

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

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

三个经典数学问题的形式化开发

计算机科学最高奖图灵奖获得者Knuth指出,算法是计算机科学的核心。算法的设计和理解对开发高效、正确的软件至关重要。本文选取平方数问题、几何级数求和问题和多项式求值这3个经典数学问题,使用支持算法程序形式化的PAR方法和PAR平台,从待求解问题的精确功能描述出发,使用PAR方法和PAR平台的推理和变换规则,经过一系列等价变换,最后得到正确的算法程序。这一系列形式化推演的过程揭示了这3个经典数学问题的奥妙,事实说明PAR方法和PAR平台在算法程序设计过程中可以发挥更大的作用。

基于动态规划的双序列比对算法构件设计与实现

双序列比对算法是生物信息学中的一个关键算法,广泛应用于序列相似性分析以及基因组序列数据库搜索.现有研究主要针对特定应用问题优化和使用相对应比对算法,缺乏高抽象层算法框架的细致研究,在一定程度上导致了序列比对算法的冗余性以及人为选择算法可能造成的误差等问题,也使得人们难以有效地了解算法结构.通过深入分析基于动态规划的双序列比对算法(dynamic programming-based pairwise sequence alignment algorithm, DPPSAA)领域,在建立该算法领域的特征模型以及对应算法构件交互模型基础上,利用PAR 平台形式化实现双序列比对算法构件库,并装配生成具体算法,保证了形式化装配算法的可靠性,为序列相似性分析算法应用提供了一条有价值的参考途径.最后,利用PAR平台 C++程序生成系统将组装的比对算法转换为 C++程序,运行结果表明DPPSAA算法构件库具有一定的实用性.

虚拟现实软件系统开发方法研究

虚拟现实技术是一门综合性技术,涉及计算机图形学、多媒体技术、人机交互和人工智能等多个领域,在教育、医疗、娱乐、军事等众多领域有非常广泛的应用。所有这些技术和应用最终都要靠计算机软件来实现,这就使得虚拟现实系统的软件变得十分庞大和复杂,涉及许多多媒体数据。传统软件开发方法和程序设计技术侧重于处理文本数据,显然不能满足开发虚拟现实软件的需要。试图以所在团队研发成功的PAR方法和PAR平台为基础,根据虚拟现实软件系统的特征,探寻虚拟现实软件系统开发的新方法,进一步扩充和完善PAR平台中已有多媒体处理技术、形式化建模技术和C#等高级语言程序自动生成系统。

多序列比对算法族的形式化设计与生成

多序列比对问题是生物信息学研究的重要部分,是解决物种进化关系、基因组序列分析等问题的基础。多序列比对算法具有很高的专用性,不同的算法适用于不同的研究环境。目前常用的多序列比对软件是在生物信息学理论指导下利用多个子算法装配形成的,而现有的研究主要针对特定算法的特定步骤进行优化,缺乏领域层次高抽象性的算法框架研究,致使多序列比对算法较为繁杂且冗余过多。根据产生式编程以及软件复用的思想,分析了多序列比对算法族MSAA的特征,设计了相应的泛型算法构件并刻画了构件间的交互关系,进一步借助PAR平台形式化构建了MSAA构件库,提高了装配算法的可靠性和组装灵活性,便于研究人员的维护和优化。

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

针对传统的脚本建模存在语言机制复杂繁琐、开发效率不高、可靠性难保证、建模阶段和交互阶段相互独立等问题,基于分划与递推(PAR)及其Apla抽象程序设计语言,设计与原Apla语言融合的虚拟现实建模语言机制。开发的Apla→MAXScript自动生成系统可以将抽象Apla程序转换成MAXScript脚本,并借助3DSMax来实现三维建模。Apla建模机制采用直接重用MAXScript修改器API方式,既大幅度简化了重构的工作量,又延续了Apla语言抽象程度高特征,便于对Apla建模程序进行形式化推导和正确性验证。最后通过案例证明了Apla建模语言及其工具能够提高三维建模的精细度、可靠性及开发效率。