一种基于指针逻辑的代码安全属性分析方法

在分析和总结前人工作的基础上,提出了一种改进的代码安全属性验证方法.该方法在利用传统的源代码安全属性验证工具的基础上,加入了指针逻辑,针对现有代码属性分析技术只能对C语言子集进行分析验证的不足,利用指针逻辑对源代码的分析结果对源代码中的指针进行替换,从而避开了传统静态代码属性验证工具对指针处理功能太弱的瓶颈,可以实现对C语言中的部分指针及运算进行处理.

基于Isabelle定理证明器算法程序的形式化验证

形式化验证对保证软件的正确性和可靠性具有十分重要的意义.定理机械证明是形式化验证的一个重要研究领域,Isabelle系统是一个被广泛运用的定理证明辅助工具.本文在分析Dijkstra最弱前置谓词理论的基础上,根据PAR方法开发的算法程序循环不变式,提出了一种使用Isabelle定理证明器对算法程序进行机械验证的方法.该方法既克服了传统手工验证过程的繁琐性和易错性等缺点,又达到"提高验证效率和保证算法程序高可信"的目标,具有很好的实用价值.

森林流域单元水文模型的构建与应用

目前全球缺水、水污染、洪涝灾害以及水土流失仍然非常严重，尤其在我国北方地区。流域水文模型可用来进行不同需水管理的情景分析，为解决我国水问题提供科学依据。分布式水文模型是流域水文模型的发展方向，具有显著特点：1）应用前景广泛，不仅可以模拟流域水文过程，还可以协助模拟泥沙或污染物的运移过程，为水利工程设计、水土保持、环境保护等领域提供技术支持；2）能够预测流域土地利用或气候变化下的流域水文响应过程变化，为管理部门提供决策支持；3）模型所需要的参数全部具有物理意义，可通过实际测量确定，适合模拟实测系列较短或是无观测流域的水文过程；4）对于目前国际水文界的前沿问题—水文尺度转换提供了一种有效的解决途径。 然而分布式水文模型还不完善，如1)真实性问题。对一些水文过程和边界条件还不确定。2)尺度转换问题。目前很少考虑尺度对参数有效性的影响。3)检验问题。还无法判断对有些难以测量的水文状态变量的模拟正确与否。4)计算时间和数据存储的问题。有些分布式水文模型虽然具有很强的水文物理基础和完善的模型结构，但是计算时间过长和(或)数据存储过大，难以应用。上述问题的核心就是对分布式水文模型的核心—单元水文模型的研究不够，需要为进一步完善单元水文模型进行研究。 本文采用饱和入渗理论、Saint-Venant方程、Richards方程、Penman-Monteith方程等等构建了以有限差分法求解的适用于森林流域的单元水文模型，并通过实验室模拟试验和坡地径流场资料进行了验证，主要结论为： 通过不同坡度和不同雨强下的室内坡面产汇流实验模拟，表明：该模型模拟的坡面流和壤中流过程与实测过程基本一致，峰现时间、径流历时、峰值流量、出流总量模拟值与实测值的相对误差均较小，基本小于10%。模型的模拟精度较高，实用性较强，为深入研究壤中流机制和改进流域降雨-径流模型提供了理论依据。 通过坡地径流观测场实测资料的验证，表明：该模型模拟的坡面流过程精度较高，累计流量的精度更高于小时过程的精度，离差系数、效率系数、确定系数均较理想，具有应用价值，有助于改善分布式水文模型在森林流域的模拟效果。

重离子相对生物学效应的实验测定及生物有效剂量的验证

重离子高的相对生物学效应（relative biological effectiveness ，简称RBE）是将其应用于放疗治癌的生物学优势。生物有效剂量(GyE) = RBE

对称加密方案的密文验证安全性

文中研究由密文的完整性检查而导致的数据保密性问题,提出一个新的安全概念——加密方案在密文验证攻击下的不可区分性(IND-CVA:indistinguishability ofencryption scheme under ciphertext verification attacks)来刻画加密方案在这种情况下的保密安全性。IND-CVA允许敌手访问加密oracle和密文验证oracle。与IND-CPA和IND-CCA相比,IND-CVA比IND-CPA稍微强些,但要比IND-CCA弱得多。IND-CVA能使多数常用的加密方案(如:OTP,CBC,及CTR)得以满足。并且,这个IND-CVA可以恰当地刻画安全信道的保密安全性。将认证方案和加密方案结合起来是保证通信安全的一种常用方法。然而,在IND-CVA模型下,当利用认证方案来加强保密安全性的时候,却有可能反而破坏了原有的保密安全性。IND-CVA揭示了完整性对保密性的影响,准确刻画了安全信道的保密性要求,为协议设计提供了有益的参考。

基于一阶迁移系统的限界模型检测工具实现

为了简化在限界模型检测过程中模型的建立过程,给出了一种采用基于一阶迁移系统语言的模型建立方法,并在此一阶迁移系统语言中加入了通道的功能,增强了描述能力。然后在此基础上完成了一个以基于插值和k步归纳的限界验证算法为核心的模型检测工具(BMCF),最后利用该工具对常见的互斥协议,简单数据传输协议的性质进行了分析与验证。结果表明,利用该工具对系统进行建模具有方便直观的特点,并借助实现的验证算法能高效的检验性质的正确性,如果性质不成立工具还会给出反例提示。

一种基于安全状态转移的简并测试集生成方法

在总结前人工作的基础上,结合安全操作系统对测试的特殊需求,提出了简并测试集(degenerate test set,简称DTS)的概念,设计了一种使用模型检测的基于安全状态转移的高效测试集生成方法.该方法以状态转移为化简对象,在利用模型检测技术生成测试用例的同时,归并相同的状态转移并化简需求集中的冗余属性,从而最终达到化简测试集的目的.在此基础上,探讨了单个用例失败时用例集的有效性问题,并对DTS生成算法进行了改进.实验结果表明,该方法可以有效地对测试集中的冗余进行化简.

模型检测MESIF Cache一致性协议

在处理器从单核向多核演进的过程中,为了获得更好的性能和可扩展性,适用于多核处理器系统的Cache一致性协议变得越来越复杂。Cache一致性协议的验证一直是模型检测在工业界主要应用之一,被工业界和学术界关注。相对传统方法而言,微结构级的模型检测能够描述和验证更多的协议细节。利用NuSMV工具对Intel公司的MESIF Cache一致性协议进行模型检测在微结构层次上进行了建模,并对该协议进行模型检测,试验结果证明了此方法的有效性。

语义Web服务组合一致性验证及案例研究

语义Web和Web服务是当前热门的应用技术，而两者的结合——语义Web服务将在未来几年具有极大的应用前景。语义使得~Web~服务的自动发现和自动组装变得非常容易、高效，但是随之而来的问题是如何确保自动组装的~Web~服务组合在本体知识库的状态下是一致的，并且在执行过程中也始终保持一致。 本文介绍了一种基于路径的语义Web服务组合验证方案，通过对服务组合中的单个Web服务进行输入、输出、前置条件和执行效果（IOPE）进行语义标注，旨在找出组合执行过程中在任何结点处可能存在的不一致性。文章定义了显式不一致性和隐式不一致性，首先提出了语义Web服务前置条件和执行效果的正规化表示方法，然后介绍了顺序和并发执行的多个Web服务之执行效果自动化累积算法，接下来给出了基于路径的一致性验证算法。文章还给出了实现该验证方案的平台架构，给出了相关实验过程和结果。 文章还完整地介绍了中科院某研究所本体的构造和扩充过程，定义了研究生毕业申请服务组合，并介绍了服务的IOPE标注，最后运用验证方案对该组合进行验证，给出了验证结果。

algorithms for computing weak bisimulation equivalence

IEEE Comp Soc, IFIP, Tianjin Normal Univ

A theoretical framework of tracer methods for marine sediment dynamics

A new theoretical framework of tracer methods is proposed in the present contribution, on the basis of mass conservation. This model is applicable for both artificial and natural tracers. It can be used to calculate the spatial distribution patterns of sediment transport rate, thus providing independent information and verification for the results derived from empirical formulae. For the procedures of the calculation, first, the tracer concentration and topographic maps of two times are obtained. Then, the spatial and temporal changes in the concentration and seabed elevation are calculated, and the boundary conditions required are determined by field observations (such as flow and bedform migration measurements). Finally, based upon eqs. (1) and (13), the transport rate is calculated and expressed as a function of the position over the study area. Further, appropriate modifications to the model may allow the tracer to have different densities and grain size distributions from the bulk sediment.

Determination of fractional energy loss of waves in nearshore waters using an improved high-order Boussinesq-type model

Fractional energy losses of waves due to wave breaking when passing over a submerged bar are studied systematically using a modified numerical code that is based on the high-order Boussinesq-type equations. The model is first tested by the additional experimental data, and the model's capability of simulating the wave transformation over both gentle slope and steep slope is demonstrated. Then, the model's breaking index is replaced and tested. The new breaking index, which is optimized from the several breaking indices, is not sensitive to the spatial grid length and includes the bottom slopes. Numerical tests show that the modified model with the new breaking index is more stable and efficient for the shallow-water wave breaking. Finally, the modified model is used to study the fractional energy losses for the regular waves propagating and breaking over a submerged bar. Our results have revealed that how the nonlinearity and the dispersion of the incident waves as well as the dimensionless bar height (normalized by water depth) dominate the fractional energy losses. It is also found that the bar slope (limited to gentle slopes that less than 1:10) and the dimensionless bar length (normalized by incident wave length) have negligible effects on the fractional energy losses.

Numerical simulation on the process of saltwater intrusion and its impact on the suspended sediment concentration in the Changjiang (Yangtze) estuary

To study the relationship between sediment transportation and saltwater intrusion in the Changjiang (Yangtze) estuary, a three-dimensional numerical model for temperature, salinity, velocity field, and suspended sediment concentration was established based on the ECOMSED model. Using this model, sediment transportation in the flood season of 2005 was simulated for the Changjiang estuary. A comparison between simulated results and observation data for the tidal level, flow velocity and direction, salinity and suspended sediment concentration indicated that they were consistent in overall. Based on model verification, the simulation of saltwater intrusion and its effect on sediment in the Changjiang estuary was analyzed in detail. The saltwater intrusion in the estuary including the formation, evolution, and disappearance of saltwater wedge and the induced vertical circulation were reproduced, and the crucial impact of the wedge on cohesive and non-cohesive suspended sediment distribution and transportation were successfully simulated. The result shows that near the salinity front, the simulated concentrations of both cohesive and non-cohesive suspended sediment at the surface layer had a strong relationship with the simulated velocity, especially when considering a 1-hour lag. However, in the bottom layer, there was no obvious correlation between them, because the saltwater wedge and its inducing vertical circulation may have resuspended loose sediment on the bed, thus forming a high-concentration area near the bottom even if the velocity near the bottom was very low during the transition phase from flood to ebb.