论文部分内容阅读
澄清了非滥用性质的模糊理解,提出了一种新的非滥用性质的形式化描述,并用定理证明工具Isabelle/HOL验证了BW多方合同签署协议的非滥用性。
合同签署协议非滥用性的形式化描述
【摘 要】
：
澄清了非滥用性质的模糊理解,提出了一种新的非滥用性质的形式化描述,并用定理证明工具Isabelle/HOL验证了BW多方合同签署协议的非滥用性。
【机 构】
：
解放军理工大学指挥自动化学院 南京 210007
【出 处】
：
2007全国软件及其应用学术会议
【发表日期】
：
2007年8期
其他文献
为了解决传统车型识别技术难以应用于背景变换的视频流和单幅图像的问题,本文提出基于约束Delaunay三角剖分(CDT)变换的通用车型识别方法。该方法通过对图像角点进行CDT变换获取车辆假设区域,依据图像纹理特征判断真实车辆区域,最终进行特征匹配输出识别结果。
当前对于科学计算的监控管理仍然普遍采用基于脚本的方式,对用户的要求较高。本文从业务流程编排方式、系统结构、各功能模块实现三个方面介绍了一种基于B/S的图形化监控管理系统的构建方法。
在肺部医学图像检测与诊断中,分割肺实质是肺结节检测的第一步。由于需要检测的肺结节的大小仅为2～10毫米,因此更应该精确分割出肺实质的边缘,并尽可能避免遗漏很小的粘连在肺壁上的肺结节,这是目前研究的难点。本文提出了一种自动分割肺实质分割方法,方法的要点是:1.为了更好利用区域增长算法截取主支气管和肺实质交接处边界,提出了应用各向异性滤波去除噪声。2.应用优化阈值算法得到肺部二值化图像。3、根据搜索最
随着Web相关技术的发展软件呈现出新的形态,如在网络上自由发布,遵循公共协议的网络服务,以及自主构造的网构软件。软件开发过程也随之发生变化,要求软件构件具有按需动态组装的能力。作为开发先导的需求工程过程,也必须建立起新的分析框架以适应面向服务的软件的要求。本文采用本体作为组织需求概念的核心,选取了教育领域进行分析,描述了教育领域的基本需求。在此基础之上,文章提出了新的需求分析框架即面向服务软件的需
为了使软件系统能够在运行时改变系统的行为,满足环境和用户的动态需求,本文给出一个面向构件的动态体系结构框架。该框架符合基于构件的开发模式,具有实施简单、运行高效的特点。该框架不仅实现了在运行时安全地对构件实施增加、删除和替换的基本操作,还支持构件语义接口的动态更新以实现构件自身的升级。在此基础上,框架提供自演化接口,实现了系统的自演化。同时引入演化约束机制,保障演化后的系统满足基本的约束。该框架系
软件可视化在软件逆向工程中发挥着重要的作用,它具有直观、易理解性好等优点。在面向对象软件开发中,结构清晰的类图能够帮助开发人员便捷地理解Java程序。本文从逆向工程的角度分析了Java程序可视化中面临的问题,基于传统的层次布图算法,从支持类关系精确提取、软件设计模式以及软件版本演化等方面对Java可视化方法进行了扩展;并实现了可视化系统Venus,它具有符合UML类图语义、层次展现度好以及支持图元
现有的基于关键字或语义分类信息的Web服务发现基本上都是针对单个Web服务行为的。本文提出了一种基于模式匹配的组合Web服务的发现方法,通过对Web服务的交互模式匹配性和组合模式匹配性的检查,可以得到满足用户要求的组合行为的服务,从而降低了用户参与组合服务的难度,实现Web服务大粒度的重用和高效的开发。
软件体系结构元信息的组织和管理是利用反射机制实现软件体系结构重用的一个重要问题。为了满足基于反射的体系结构设计重用的需求,本文提出了一个体系结构元信息模型,它能有效地反映出体系结构的元信息以及其组织形式。此外,利用XML Schema来描述该元信息模型,得到了一个可以由计算机软件自动处理的元信息模型框架,使得体系结构设计人员通过软件工具操作它,从而实现通过操作元信息来设计出新的体系结构,达到在设计
将目标驱动的需求分析方法引入军事电子信息系统需求获取过程,使军事人员可直接参与需求建模,无疑为准确把握军事电子信息系统的需求提供了行之有效的方法指导。但不同的军事人员可能会提出相互冲突的目标,从而不同程度地影响了系统整体需求的可行性。本文用KAOS方法提供的描述语言形式化定义了军事电子信息系统的目标概念,并介绍了KAOS方法的冲突处理机制在其中的应用,为发现和解决目标冲突提供了理论方法指导,为需求
膨胀图是有很好连通性的稀疏图。一个膨胀图族是具有相同膨胀系数的一类正则膨胀图。本文从组合学角度对膨胀图及膨胀图族的概念、性质进行讨论。用概率方法证明了3-正則膨胀图族的存在性,井证明了2-正则膨胀图族的不存在性,提出了一类3-正則非膨胀图──塔形图的概念。按时间复杂度可将膨胀图分为弱可构造的和强可构造的。膨胀图的扩张图仍然是膨胀图,通过应用实例说明利用膨胀图能够降低随机算法对随机位的依赖程度。