移动进程的空间逻辑

提出了一个用于描述异步π-演算中移动进程的时态和空间性质的模态逻辑. 该逻辑具有基于谓词变量的递归构造. 建立了这一逻辑的语义理论, 并证明了语义的单调性, 从而保证了不动点的存在. 还设计了一个算法来自动地检测移动进程是否具有用该逻辑公式所描述的性质, 并证明了该算法的正确性.     

科学发现的逻辑验证

R演算是一个关于逻辑连接词符号和量词符号的演算系统．它是一个根据事实反驳对科学理论进行修正的符号演算系统．文中以狭义相对论和生物进化论为例，使用R演算，对这两个科学理论的发现过程，在数理逻辑层面进行了验证．验证的结果表明：对Einstein时代的物理学而言，狭义相对论是唯一而且正确的选择．对Darwin时代的生物学而言，在接受自然选择原理等前提下，R演算可以推导出3种不同的，但逻辑上合理的进化论方案．Darwin提出的进化论是其中一种．有趣的是三者中的另一种，现在看来它具有一定的包容性．     

开放域静态电磁场问题数值解的渐近边界条件技术研究

基于电势的多极展开理论, 对开放域静态电磁场问题数值解的渐近边界条件(ABC)技术的近似实质给出了解释, 揭示了传统高阶ABC的缺陷, 提出了建立新型高阶ABC的概念和相应的表达式. 数值例题表明了新型高阶ABC的优点.     

一类含积分约束的生产制造系统优化调度

“即时消费”类生产制造系统的优化调度具有重要学术和应用价值. 满足此类系统对产量的实时需求, 考虑调度计划的可实现性具有挑战性. 如何得到精确满足累积产量实时需求的最优调度目前尚无系统方法, 迫切需要研究. 本文建立了含积分约束的生产制造系统优化调度新模型. 通过对生产量变化率约束的深入分析, 证明了该类优化问题等价于光滑非线性规划问题. 生产设备在各时段的产量上下界可表述为时段初、末时刻瞬时生产率的二元函数, 且为精确可达的上下界. 本文结合梯度映射的单调性, 证明了上下界函数的凸性(凹性), 在生产成本为凸函数时, 进一步证明了此类优化调度问题等价于凸规划问题. 本文以上述分析为基础, 针对含积分约束的生产制造系统优化调度问题, 提出了两阶段数值求解方法, 在许多情况下可以迅速获得调度问题的全局最优解. 新模型和相应求解方法克服了生产量变化率约束带来的困难, 获得了精确满足累积产量实时需求的最优调度. 本文同时以电力生产优化调度问题为例, 进行数值求解, 并对结果进行了讨论, 验证了新模型和相应方法的有效性.     

离散幅度信号分析方法及其应用

研究离散幅度信号的分析方法。提出任意连续信号的二比特量化重构定理，建立了以信号量化精度作为尺度的多分辨率分析的概念，还分析了离散时间信号用二比特序列重构时的奇异点和求余效应。在实际信号处理应用中，用二比特量化重构定量，提供了一种有效的压缩编码方法，还利用量化精度多分辨率分析方法，实现了高速实时检测。理论和实验证明，提出的离散幅度信号分析方法是一种简单、有效的并行信号分析方法，尤为适于硬件实现。     

需求驱动的Web服务建模及其验证:一个基于本体的方法

从Web服务所交互的环境角度出发，提出了基于环境本体的Web服务能力描述框架，从Web服务操作的环境以及操作导致的环境变化两个方面刻画Web服务的能力，并由此建立了需求驱动的Web服务组合模型．同时提出用π演算的进程表达式表示Web服务的行为语义，并建立了从Web服务概念化的能力表示到形式化的进程表示的自动转换机制，在此基础上给出Web服务组合的可行性验证算法及需求可满足性的验证方法．经过验证的Web服务组合模型可以作为备选执行方案之一反馈给需求提出者．     

矩独立的基本变量重要性测度及其概率密度演化解法

为有效分析基本变量对可靠性分析中失效概率的影响程度,提出了一种矩独立的基本变量对系统失效概率的重要性测度指标η,分析了其相应性质,并给出了性质的证明.在此基础上,比较了基本变量对系统失效概率与基本变量对响应量分布密度的重要性测度,并建立了求解2种矩独立基本变量重要性测度的概率密度演化方法,有效地解决了求解2种矩独立基本变量重要性测度在计算上的困难.采用所建立的重要性测度概率密度演化方法,求解了数值算例和具体工程中基本变量对功能响应函数分布密度和失效概率的重要性测度指标,结果证明所提重要性测度可以从输入变量随机取值的分布密度角度衡量基本变量对失效概率影响的程度,同时,计算结果也表明采用所建立的求解重要性测度的密度演化方法是高效可行的.     

基于高阶面元法与模态法的静气动弹性分析方法

建立了一种基于高阶面元法与模态法的静气动弹性分析方法，并基于此方法对弹性机翼进行了静气动弹性分析．基于机翼几何实体模型建立了三维气动力模型，利用高阶面元法计算气动力，通过模态法实现气动与结构的耦合，以AGARD445．6机翼和一个小展弦比机翼为研究对象，分析了机翼结构弹性变形对气动力的影响．本文重点研究了机翼的气动力系数、翼根载荷、结构变形、不同展向位置的压力分布等参数的变化趋势，并将部分结果与风洞试验、基于风洞试验气动力所得弹性结果进行了对比．结果表明：高阶面元法计算所得气动力具有较高的精确性；基于高阶面元法与模态法的静气动弹性分析方法具有可行性、可靠性和高效性，可以提供较为全面的静气动弹性数据为飞机初步设计参考．     

R-演算:一个修正程序规约的演算系统

在一个软件规约(program specification)的形成过程中, 规约总是不断被修改, 要么增加新的功能, 要么由于出现事实反驳, 而改正规约中的错误. 规约的新功能是与其逻辑无关的新规则, 而它的事实反驳则是其反例. 新规则和事实反驳都是由研究者或用户提出来的. 极大缩减是在规约出现事实反驳的情况下, 对规约的理想修正. 这里在一阶逻辑的框架下给出规约的新规则、事实反驳和极大缩减的模型论定义. 构建了R-演算. 该演算由一组变换规则组成, 用以删除规约中与事实反驳矛盾的规则, 并最终得到规约的极大缩减. 同时证明了R-演算的可达性和完全性.     

网格服务链模型的验证分析技术及应用

确保网格应用中大规模资源共享和复杂任务处理的正确性与可靠性是一项重要的工作．文中从形式化方法的角度出发，提出了基于状态Pi演算的网格服务链模型作为对网格中服务协作与组合进行建模和分析的理论工具．其中，状态Pi演算针对Web服务资源框架（WSRF）的思想，协调了系统状态与行为间的关系，扩展了Pi演算对系统状态的全生命周期管理能力．在此基础上，进一步结合了模型验证技术对网格服务链进行设计和运行时的逻辑性质分析．通过材料形变与断裂过程动态分析的网格应用案例，展示了采用上述方法对网格应用进行需求验证和可靠性分析的有效性．     

一种基于P/T网的低级并发程序验证模型

随着片上多处理器/多核技术的不断发展,采用机器级语言的并发程序(低级并发程序)有了更加广阔的应用前景.然而,低级并发程序的验证问题也成为程序语言领域一种新的挑战.并发程序安全性验证领域现有的工作多数是针对高级语言、规范或者演算,而针对机器级语言的甚少。这种情况的主要原因之一是缺少低级抽象模型.文中描述一种可验证的低级并发编程模型P-PMCC.P-PMCC程序是一个扩展的P/T网系统,其网结构用来刻画低级并发线程(原子的顺序汇编级代码)之间的并发关系.P-PMCC程序的验证采取模型检查和定理证明相结合的方法,分开考虑并发行为与顺序线程的规范和验证:前者借助于Petri网领域已有的方法,后者则借助现有的顺序程序的正确性证明方法。P-PMCC程序也可以看作并发程序的一种可验证的低级中间表示.     

梯级水电站群长期发电优化调度多核并行随机动态规划方法

随机动态规划求解水电站群长期发电优化调度易产生"维数灾"问题,导致计算耗时急剧增加,求解效率降低.如何缓解维数灾和提高计算效率,一直是水库优化调度致力于研究的难点问题.在随机动态规划的并行性分析基础上,提出了基于Fork/Join并行框架的多核并行随机动态规划方法.该方法将单个时段内所有变量组合状态下的计算任务作为父任务,通过分治法递归分解为多个子任务,并平均分配到不同的内核同时计算实现细粒度并行求解.以澜沧江下游梯级水电站群为研究实例,建立了3个变量离散数不同的调度方案,并在多核环境下验证该方法的计算效率.结果表明,在2和4核环境下,该方法的计算耗时与串行方法相比,分别节省了约50%和70%,大幅度缩减计算耗时,可充分利用多核资源;同时,计算任务的规模越大,并行计算的耗时缩减幅度越大.因此,此方法为大规模水电系统优化调度提供了一种可行途径,其并行原理可为其他应用所借鉴.     

高阶效应对超短光孤子脉冲传输特性的影响及其抑制方法

采用时域和频域复合控制方法,建立了光脉冲的传输方程,研究了高阶效应条件下飞秒和短皮秒光孤子系统中抑制孤子自频移(SSFS)和定时抖动影响的可行性和有效性采用变分法分析了高速啁啾高斯准孤子在高阶色散、自陡峭效应和自频移条件下的传输演化特性针对高阶效应对孤子传输特性的影响和产生定时抖动机理,采用时频复合控制方法,消除了自陡峭和受激Raman散射效应的影响,稳定了孤子中心频率,有效抑制了由高阶效应产生的系统定时抖动.设计了160Gb/s长距离高速孤子传输系统并对传输特性进行了数值模拟,所得结果与理论分析完全一致,结果对高速长距离通信系统的设计有指导意义.     

Boole过程论

定义Ｂｏｏｌｅ过程为与时间参数ｔ有关的Ｂｏｏｌｅ变量族，Ｂｏｏｌｅ过程的一个实值样本是波形，波形函数可以用数学工具形式地加以处理，定义了波形多项式的差分，距离和极限，给出了极限存在的充分必要条件，在此基础上，严格地重新定义了通路敏化概念，以期说明了Ｂｏｏｌｅ过程论的应用前景。     

开互模拟的一条泛公理

π-演算公理化中较难处理的是有关局部化算子的等式, 传统的方法是使用带条件的推导规则或使用“区别”. 提出一条关于π-演算局部化算子的泛公理, 并证明它可在开互模拟的公理化中取代“区别”的作用. 本方法的好处是在公理化过程中我们只要处理一个互模拟, 而无须处理一族互模拟.     

一种形式化的实时协议互操作性测试方法

协议互操作性测试是一种保证网络通信协议实现质量的重要技术．下一代互联网协议需要提供对实时应用的有效支持，然而已有互操作性测试相关研究中并没有考虑协议中的时间约束，现有互操作性测试技术很难应用于实时协议互操作性测试中．文中提出了一种形式化的实时协议互操作性测试方法．首先提出了一个用于描述实时协议互操作性测试被测系统的形式化模型CMpTIOA（通信多端口时间输入输出自动机），基于该模型定义了时间互操作性关系；然后提出一种以时间互操作性关系为指导的测试生成方法，根据被测系统模型生成参数化测试行为树，在该方法中还集成了可执行性预判决机制，在一定程度上缓解了状态空间爆炸问题；最后将提出的理论和方法应用于IPv6邻居发现协议的互操作性测试中，验证了该方法的可行性．     

电力系统能量与备用联合优化与精确调度

随着能源与环境危机日益严重,如何建立精确调度模型成为电力市场逐步完善过程中的一个迫切需要研究的课题．目前广泛采用的建模方式是将时间离散化,建立离散时间调度模型,本文首先举例说明离散时间调度模型中所定义的备用容量上、下限存在不可达的情况,即离散时间调度模型中的备用容量上、下限约束条件不严格,从而造成实际调度时存在旋转备用容量无法满足实际需求的情况．通过对机组出力方式与爬坡率关系的详细分析,证明了任意调度时段内机组精确可达的备用容量上、下限与该时段首末时刻机组输出功率相关,并给出了精确可达备用上、下限的计算方法．基于上面的分析结果,建立了能量与备用联合优化与精确调度模型,该模型将能量与备用联合精确调度这样一个连续时间最优控制问题建模成一个非线性规划问题,从而极大地降低了问题的复杂性,避免连续时间最优控制问题所存在的求解困难．应用序列二次规划法对模型进行了数值求解,并对结果进行了讨论,进而验证了模型的有效性．     

线性系统特征值的计算及其分布

提出了两种计算性系统特性值的方法，其一是由低阶到高阶用根轨迹法逐次递推同全部特征值，其二是利用Ｓｃｈｗａｒｔｚ阵的性质采用搜索方法确定系统特征多项式的所有因互。还给出确定在左右半复平面内各有多少个特征值的方法。     

塔里木河干流水资源的形成及其利用问题

新疆塔里木河干流是典型的干旱区内陆河, 自身不产流, 水资源全部依靠其源流补给, 为纯耗散性河道. 采用时间序列分析方法对塔里木河干流上游三源流(阿克苏河、叶尔羌河、和田河)的年径流量动态变化进行了分析, 建立了源流区的耗水模型, 对源流区来水及耗水的增加趋势给出了定量结果. 分析了干流各测站年径流量的变化趋势, 从而粗略推算了现状条件下各站发生间歇性断流的时段. 建立了干流区耗水模型, 分析了干流上、中游各段耗水特点, 得出了各段耗水随干流来水减少而减少、因人类活动而增加的定量关系.     

机构运动几何学的统一曲率理论

基于微分几何学方法导出了结构运动的瞬心线和瞬轴面及其不变量的表达式，并阐明了不变量的运动学意义，讨论了平面运动，球面运动和空间运动连杆上点的轨迹及空间运动连杆上直线的轨迹的不变量性质，建立了由平面到空间在形式上和内容上统一的机构运动几何学曲率理论。