命题投影时序逻辑并发建模与自动验证

针对目前尚无模型检测方法对区间并发模型进行区间性质的自动验证的情况,采用命题投影时序逻辑中具有特定结构的一类公式来建立系统的区间并发模型,该逻辑的任意公式可以描述模型需要满足的区间性质,通过归约为已有的逻辑公式可满足性判定算法,证明了命题投影时序逻辑统一框架模型检测是可判定的,从而得到了其自动验证方法,并给出了一个验证实例.     

面向投影时序逻辑的Web服务模型检测

为了满足Web服务的可靠性.利用投影时序逻辑的模型检测方法来验证Web服务.利用投影时序逻辑的一个可执行子集对OWL-S进行建模.用命题投影时序逻辑来描述期望的性质.模型M和性质P统一以投影时序逻辑来表示,通过判定M蕴含P的有效性,即判定M和非P的合取的不可满足性,亦利用M和非P的正则形可构造合取式的正则图,判定合取的不可满足性,从而达到模型检测的目的.通过运行实例表明,所提模型检测器可验证Web服务系统性质,保证Web服务的可靠性.     

PPTL模型检测器实现的一个关键技术

针对命题线性时序逻辑表达能力有限的问题,设计并开发了基于SPIN(Simple Promela interpreter)验证系统的命题投影时序逻辑(PPTL)模型检测器.将协议元语言(ProMeLa)描述的系统转换为系统自动机,将PPTL公式表达的性质转换为性质自动机,通过判定系统与性质自动机的积自动机接受的语言是否为空来判断系统是否满足性质.PPTL模型检测器修改了SPIN的匹配机制,从而改进了验证算法,使得PPTL模型检测器支持有穷和无穷模型的验证.实验结果表明,该模型检测器可以减少无效验证产生的无效迹数目,有效地实现PPTL模型检测.     

基于PPTL的着色Petri网的模型检测方法

为了提高着色Petri网的描述及验证能力,提出了一种基于投影命题时序逻辑的着色Petri网的模型检测方法。通过构建投影命题时序逻辑公式的否定形式等价的Buchi自动机,将它与着色Petri网的可达图相积,通过检测检测乘积图的可接受语言是否为空,从而判断用时序逻辑公式描述的系统性质是否满足。利用投影命题时序逻辑公式具有更强的表达力,可以有效地提高着色Petri网系统的描述及验证能力。     

基于时态逻辑的多时间序列挖掘模型

为了从多时间序列之间发现的定性的时态相关模式可而更全面的理解和把握系统的演化特性,提出了一种基于时态逻辑的多时间序列挖掘模型.它首先将多时间序列转化为多事件序列,然后将预处理后的多事件序列利用区间时态逻辑(ITL)关系子集来定义多事件序列中事件间的时态相关模式.其次进行多状态序列融合和局部时态观测序列的生成,之后采用频繁模式挖掘算法发现多时间序列的频繁时序模式.该模型有助于解决时间序列挖掘所面临的若干挑战和难题,有助于扩展现有时间序列挖掘系统的功能,从而指导时间序列等复杂类型数据的知识发现过程.实验结果表明了该模型及算法的有效性和优越性.     

基于属性RBAC及委托性质的使用控制模型

针对UCON未涉及特权委托的基本特征和权限管理的缺陷,提出了基于属性RBAC的带委托性质的使用控制模型(EUCON).将角色、委托和扩展属性等要素引入到EUCON,构建了基于属性-角色的访问控制方法,提高了模型的可变性和动态性,并使用区间时序逻辑对该委托模型的完备性进行逻辑验证,最后提供了网上行政审批的实例,为模型的应用奠定了一个很好的实例基础.     

基于UML状态图的工作流时序约束一致性研究

通过对UML状态图进行时间扩展，建立工作流的时间模型，再把该模型转化为时间自动机，接着用时序逻辑公式定义时序约束，最后分别在建立阶段、实例化阶段和运行阶段使用模型检测技术对时序约束的一致性进行验证．     

业务流程的形式化设计与验证

针对如何保证业务流程设计模型与业务需求的一致性问题,在研究有限自动机模型的基础上,提出了一种业务流程的自动机模型构建和验证方法.采用扩展的带约束条件的确定有限自动机对业务流程设计模型进行形式化描述,使用线性时序逻辑表示业务需求,分别给出业务流程设计模型到自动机模型和自动机模型到Promela描述的转换算法,并通过模型检测技术,使用Spin工具验证设计模型是否满足需求性质.若不满足性质,则能够获得反例执行的路径.实例分析表明,该方法可用于业务流程设计的正确性验证.      

一种基于TLA的解决N皇后问题的方法

行为时序逻辑语言(TLA+)是一种在模型检测范围内能够表达模型程序和逻辑规约的语言。N皇后问题是一个久远的问题,回溯法是解决该问题一种经典的方法。本文提出如何用行为时序逻辑语言TLA+去描述N皇后问题,然后使用Toolbox工具去检测n=5时该问题的全部解。     

关于BMI模型的算法及其研究

对基于区间值估计的 BMI模型作了充分的研究 ,给出了该模型的算法的一些直观特征 ,并指出了该模型的算法的一些不完善的地方以及该模型中的一些不合理的限制条件 ,在此基础上 ,给出了一个修正的算法 ,该算法解决了原算法中存在的不确定性的平行传播问题     

基于Boltzmann模型方程的平板Couette流计算

将基于Boltzmann模型方程的气体运动论统一算法推广应用于Couette槽道流计算,发展可用于槽道流问题的气体运动论边界条件数学模型及数值处理方法,研究建立模拟不同Knudsen数二维低速槽道流动问题的气体运动论数值算法,通过将近连续流到高稀薄区Couette剪切流计算结果与基于微观分子统计模拟的类DSMC值、基于宏观流体力学滑移Navier-Stokes解和线化Boltzmann近似解比较分析,显示出该文发展的介观Boltzmann简化速度分布函数方程数值算法对不同尺度槽道流问题具有很强的模拟能力。     

Super resolution reconstruction of moving objects from low resolution surveillance video

Construction of high resolution images from low resolution sequences having rigid or semi-rigid objects with unified motions is often important in surveillance and other applications. In this paper a novel object-based super resolution reconstruction scheme was proposed, in which a six-parameter affine model-based object tracking and registration method was first used to segment and match objects among a sequence of low resolution frames. The motion model was then further extended to the traditional maximum a posterior (MAP) super resolution algorithm. The proposed object tracking and registration method was evaluated by both simulated and real acquired sequences. The results have demonstrated the high accuracy of the proposed object based method and the enhanced reconstruction performance of the extended approach.     

空间线性组合模拟模型及其实证

空间分布的模拟精度与采用的模型密切相关.针对具有空间自相关时空数据的空间分布模拟问题,将时空数据看成为时间序列数据与横截面数据的组合,分别建立横截面数据一阶空间自回归[SAR(1)]模拟模型和克立格(Kriging)方法模拟模型,时间序列数据的遗传神经网络(GABP)模拟模型,在这些模型研究的基础上建立空间线性组合模拟(SLCS)模型.应用这些模型对2002年福建部分县市人均GDP水平空间变异进行实证模拟研究,结果表明空间线性组合模型模拟效果较好.     

Robust Boolean Operation for Sculptured Models

To enhance the ability of current modeling system, an uniformed representation is designed to represent wire-frame, solid, surface models. We present an algorithm for Boolean operation between the models under this representation. Accuracy, efficiency and robustness are the main consideration. The geometric information is represented with trimmed parametric patches and trimmed parametric splines. The topological information is represented with an extended half-edge data structure. In the process of intersection calculation, hierarchy intersection method is applied for unified classification. Tracing the intersection curve to overcome degenerate cases that occur frequently in practice. The algorithm has been implemented as the modeling kernel of a feature based modeling system named GS-CAD98, which was developed on Windows/NT platform.     

孤立性肺结节诊断模型的特征选择算法

孤立性肺结节诊断模型中未得到充分解决的一个关键问题就是如何选择合适的特征子集。为了构建一个良好的诊断预测模型,提高肺结节良恶性诊断的效率以及准确率,提出了一种基于联合互信息的混合模型特征子集选择算法。该算法综合过滤式和包裹式特征选择模型各自的优势,首先使用过滤式方法得到与诊断有高相关度的候选特征子集,然后通过包裹式方法对候选特征子集进行特征间冗余分析,最后得到最优特征子集。实验表明,该算法与基于其他互信息的过滤式、混合模型特征选择方法相比,不仅在特征子集数目上,而且在良恶性诊断的敏感性、特异性和平均分类准确率上,均具有很好的性能效果。     

一种增广的Laguerre模型自适应预测控制算法

论文在简述基于Laguerre函数近似模型的自适应预测控制原理、算法的基础上,将现有的仅适用于开环稳定系统的预测控制算法进行扩展,提出一种增广的Laguerre函数模型自适应预测控制算法。该算法对于开环不稳定系统和非最小相位系统同样适用。仿真结果表明基于Laguerre函数模型的预测控制方法对控制变时延、变阶次对象具有较好的鲁棒性。     

Robust Boolean Operation for Sculptured Models

To enhance the ability of current modeling system, an uniformed representation is designed to represent wire-frame, solid, surface models. We present an algorithm for Boolean operation between the models under this representation. Accuracy, efficiency and robustness are the main consideration. The geometric information is represented with trimmed parametric patches and trimmed parametric splines. The topological information is represented with an extended half-edge data structure. In the process of intersection calculation, hierarchy intersection method is applied for unified classification. Tracing the intersection curve to overcome degenerate cases that occur frequently in practice. The algorithm has been implemented as the modeling kernel of a feature based modeling system named GS-CAD98, which was developed on Windows/NT platform.     

用户电费统一计算模型的设计与实现

针对在用电营业ＭＩＳ系统建立过程中电费计算无法统一处理的问题,分析了大用户电费计算复杂的原因,给出了一种电费分层计算模型和算法实现,成功地解决了建立用电营业ＭＩＳ系统的核心问题．实践证明,此算法可解决以前在电费计算过程中大用户的电费无法统一处理的问题．     

一种集成时空数据模型及语义扩展

采用面向对象的方法提出了一种具有集成特点的时空数据模型．模型分别扩展了空间数据对象和时态数据对象,时空对象是空间对象和时态对象的聚集,空间对象的变化由对象的行为进行描述并以不同的版本表现出来．此外,通过量词符号在时域上的扩充对对象的基本关系进行了语义扩展,在形式上将时态和空间谓词语义统一起来．这种模型能够更好地适应时空信息系统的应用需求．