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

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

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

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

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

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

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

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

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

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

PAR在数学算法中的应用

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

形式化方法在高中算法教学中的应用研究

国家教育部制定的高中新课程标准将算法初步作为高中数学课程的必修内容,算法与程序设计也首次纳入到选修课之列。全国大部分普通高中均按新课标开展教学实验,不少省份还把算法内容纳入高考。同时现有算法初步和算法与程序设计教材在介绍算法与算法设计方法时,无法说清楚算法设计的过程;在教学实践中,这一问题更加突出。这给高中生学习、理解及掌握算法和算法设计方法带来很大的困难。本文从新课程实验教材中及数学高考题中选取两个问题,用支持算法程序形式化开发的PAR（Partition And Recur）方法与PAR平台,从待求解问题的精确功能描述出发,经过一系列等价数学变换,最后得到正确的算法和程序。实践说明PAR方法与PAR平台可以在高中算法教学及学生能力评测中发挥建设性作用。     

中软 微软联手育人

本报讯记者蒋湘辉报道 11月20日,中软总公司与微软公司在北京签署合作备忘录,双方将建立战略合作伙伴关系,在人才培养、软件开发、市场营销、企业协议、培训认证反软件外包服务等方面进行全方位合作。根据双方签署的备忘录,中软和微软将联合开发基于微软.NET平台和Office System的各种电子政务和行业应用解决方案;中软将获得微软企业许可授权,以支持其产品开发和应用:微软将支持中软开拓国际软件外包市场,其中包括向中软提供各种软件外包业务,首批软件外包项目于今日签订;双方还将联合在一年内为中软培养200名软件开发人员和120名软件架构师等。     

基于构件的指控软件复用

当前军用指控软件开发效率仍然较低,软件设计和代码开发重复性开发仍然普遍,由此导致软件系统的可靠性得不到保证,开发周期也较长。软件复用是指控软件开发中避免重复开发的重要解决方案,通过软件复用明显可以提高软件开发的效率和可靠性,改善军用软件的维护性和保障性。结合军工科研院所软件开发中流行的构件技术,介绍了软件复用的基本概念和关键技术,就基于构件的指控软件复用技术在指挥与控制软件系统做出应用研究,这些对指控软件复用的工程普及做出了实践贡献。     

基于构件的指控软件复用

当前军用指控软件开发效率仍然较低,软件设计和代码开发重复性开发仍然普遍,由此导致软件系统的可靠性得不到保证,开发周期也较长.软件复用是指控软件开发中避免重复开发的重要解决方案,通过软件复用明显可以提高软件开发的效率和可靠性,改善军用软件的维护性和保障性.结合军工科研院所软件开发中流行的构件技术,介绍了软件复用的基本概念和关键技术,就基于构件的指控软件复用技术在指挥与控制软件系统做出应用研究,这些对指控软件复用的工程普及做出了实践贡献.     

最小生成树算法的PAR方法形式化推导

采用PAR方法通过功能归约变换，形式化推导出可读性好、效率高的递推的最小生成树算法，简化了算法程序设计和正确性证明的过程，有效提高了算法程序设计自动化、规范化的程度及其正确性。该文给出的相关算法在PAR平台通过自动转换系统转换成可执行语言程序并运行通过。     

Mapping PAR using MODIS atmosphere products

Instantaneous PAR (Photosynthetically Active Radiation), computed from atmospheric parameters from individual images from the MODIS sensors aboard the Terra and Aqua satellite platforms, is combined to derive daily integrated PAR and mapped to a local coordinate system. Compared to field observations, the daily integrated PAR values were shown to have average errors in the order of 5-8%, with individual estimation errors as high as 21%, but monthly averages showed much better correspondence with observations yielding averaged absolute errors of around 5%. The error appears to be mostly related to uncertainties in the MODIS aerosol retrieval accuracy. This accuracy and the medium spatial resolution of the PAR map compare very favourably to other sources of PAR data and make this a useful product in the improved assessment of vegetation dynamics.     

PAR方法和循环不变式的范畴语义

范畴论对理解程序规约及程序设计和正确性证明十分有用。PAR方法则是建立在严格的数学基础之上的一种统一的算法程序设计方法。循环不变式在循环算法程序的设计中至关重要。使用格理论和范畴论作为工具对PAR方法建立一个理论框架,并对其用范畴论的概念加以解释,从而使得PAR有更强的理论基础。在此基础上引入不动点原理深入刻划循环不变式的含义,循环不变式可以表示为谓词泛函的最小不动点,并从范畴论的角度解释该过程。     

Simplified atmospheric radiative transfer modelling for estimating incident PAR using MODIS atmosphere products

Photosynthetically active radiation (PAR) is an important parameter in the estimation of vegetation growth. A method is presented with which instantaneous PAR can be calculated with high accuracy from Moderate Resolution Imaging Spectroradiometer (MODIS) atmosphere data products. The method, PARcalc, is based on a simplification of the general radiative transfer equations, whereby the atmosphere is modelled in a few layers depending on the opacity of the atmosphere due to clouds and aerosol load. The four major processes of atmospheric attenuation of solar radiation, Rayleigh scattering, absorption by ozone and water vapour, and aerosol scattering, are treated individually, using calibrated data from MODIS imagery. Comparing the calculations to field measurements made in Costa Rica in 2002, absolute errors in the order of 2-3% are obtained, which should be sufficiently accurate for application of the PARcalc method in models of vegetation growth as a source of incident PAR.