首页 | 本学科首页   官方微博 | 高级检索  
文章检索
  按 检索   检索词:      
出版年份:   被引次数:   他引次数: 提示:输入*表示无穷大
  收费全文   1篇
  国内免费   1篇
  完全免费   11篇
  自动化技术   13篇
  2020年   4篇
  2018年   1篇
  2017年   1篇
  2016年   2篇
  2014年   3篇
  2013年   1篇
  2012年   1篇
排序方式: 共有13条查询结果,搜索用时 31 毫秒
1.
针对计算机图形学中应用广泛的多边形布尔计算,提出了一种新的、适用于一般多边形的并集、交集和差集算法。算法主要分为计算交点、将交点插入多边形顶点序列、遍历三个步骤。通过采用循环单链表的数据结构、避开复杂的出入点计算、及预先的一些碰撞检测以避开复杂的求交运算与链表遍历等技巧,提高了算法的执行速度、减少了存储单元。算法能够很好地处理一些奇异情形(边界情形),比如重叠边、交点为边的顶点等情形,具有很好的鲁棒性。与经典的Weiler算法、Vatti算法和Greiner-Hormann算法相比,该算法具有较低的时间复杂度O(( m+n+k) log d))和空间复杂度。实验结果显示该算法在处理2222×2222个顶点、42个交点时比经典的Weiler算法速度提高了296倍。算法的主要思想对确定两个多面体的交、并、差问题亦有参考价值。  相似文献
2.
软件正确性是一个逐渐改进的过程.通过不断地修改,软件越来越接近于正确.同时软件的执行依赖于环境.为了刻画软件的动态正确性并考虑环境的因素,以参数化互模拟为基础,利用极限的观点,建立软件动态正确性的形式化描述.首先建立参数化互模拟的无限演化理论,给出参数化极限互模拟的定义,并给出几个特殊的参数化极限互模拟实例.其次,建立参数化互模拟极限,给出参数化互模拟极限的规约刻画.最后,证明参数化互模拟极限的唯一性、与参数化互模拟的相容性等代数性质.  相似文献
3.
统计模型检测是一种高效的验证技术,常用于复杂的随机系统验证,如分布式算法等。而在超长路径上对性质进行验证时,其验证效率会急剧降低。为解决这个问题,这里提出一种启发式的统计模型检测算法。在对路径进行验证时,我们会查找帮助剪枝的最短前缀。并在后续抽样时,利用前缀信息直接判定路径是否满足给定性质,避免进入费时的路径验证阶段。在与PRISM的比较中,它的路径验证次数相对更少且平均抽样路径长度更短。因此使统计模型检测技术可应用于超长路径上的性质验证。  相似文献
4.
强度矩阵分解作为调强放疗(IMRT)中的一个核心技术,是一个NP-hard问题。调强一般分为两种:静态模式和动态模式。本文中,我们针对静态调强放疗,对总治疗时间所主要依赖的四个参数:总机器跳数(TNMU)、子野个数(NS)、多叶准直器叶片移动速率和验证记录(V  相似文献
5.
郑晓琳  邓玉欣  付辰  雷国庆 《软件学报》2018,29(6):1517-1526
互模拟是并发系统的分析和验证的一个重要概念。本文主要扩展了一种由Du和Deng提出的准局部算法,使其更加适用于一般的标记迁移系统。我们用Java实现扩展后的准局部算法与Fernandez和Mounier提出的局部算法。我们以VLTS为实验数据基准,进行大量的实验,发现在大多数情况下,前者的性能比后者更好。同时,我们修改了算法使其能够验证模拟关系。最后,我们用Java实现对标记迁移系统进行转换,使算法同时可以验证弱互模拟关系。  相似文献
6.
葛徐骏  王玲  徐立华  郭建  朱惠彪 《软件学报》2016,27(7):1757-1771
在模型驱动软件开发过程中,基于模型的测试方法往往用于检验软件代码针对软件模型的一致性以确保软件质量.然而,随着当今软件系统规模的不断扩大,相应的软件开发过程也变得越来越灵活,代码有时会先于模型被修改,以更忠实地体现系统功能和实现机制.传统的基于模型的测试方法只能检测代码之于模型的一致性而不能反作用于模型层面,模型的修改者只能人为地评估修改的正确性,大大降低了效率并增加了系统的潜在隐患.为此,对传统基于模型的测试方法的一致性检验进行了扩展,实现了一致性检验框架ProMiner,通过抽取表达模型与代码的不一致的系统性质来自动定位模型中与实际运行系统不匹配的部分,并将其表示为可直接用于模型检测的线性时序逻辑(LTL)表达式,以支持软件模型和代码间双向的一致性检验.实验结果表明,ProMiner可有效查找软件模型和代码间的不一致并生成可直接检测模型的系统性质,从而实现了自动化的模型与代码间的双向一致性检测,不仅提高了一致性检测的有效性,而且大大减少了人力开销.  相似文献
7.
尹玲  陈小红  刘静 《软件学报》2014,25(2):400-418
信息物理融合系统(cyber-physical system,简称CPS)蕴藏着巨大的潜在应用价值.时间在CPS中起到非常重要的作用,应该在需求早期阶段明确.提出了一个基于逻辑时钟的CPS时间需求一致性分析框架.首先,构建了CPS软件的时间需求概念模型,提供时间需求和功能需求的基本概念,并给出了概念模型的形式化语义;然后,在模型制导下,从CPS的交互环境特性和约束中提取出其软件时间需求规约.基于形式化语义,定义了时间需求规约的一致性特性.为了支持形式化验证,将时间需求规约转换成NuSMV模型,用CTL公式表述要检测的特性,并使用NuSMV工具实施了一致性检测.  相似文献
8.
随着网络技术的发展,越来越多用户生成的内容(user-generated content)出现在网络应用中,其中,用户评论富含用户的观点,它们在网络环境中充当越来越重要的角色.据美国Cone公司2011年的调查报告,64%的用户在购买行为之前会参考已有的用户评论.因此,为用户提供准确、简洁和真实的评论是一个迫切且重要的任务.主要围绕评论质量评估、评论总结和垃圾评论检测这3个方面综述了国际上评论质量检测与控制的研究内容、技术和方法的研究进展.在此基础上,展望该领域的发展给出了可能的研究方向.  相似文献
9.
针对高维数据近似最近邻查询,在过滤-验证框架下提出了一种基于学习的数据相关的c-近似最近邻查询算法.证明了数据经过随机投影之后,满足语义哈希技术所需的熵最大化准则.把经过随机投影的二进制数据作为数据的类标号,训练一组分类器用来预测查询的类标号.在此基础上,计算查询与数据集中数据对象的海明距离.最后,在过滤后的候选数据集上计算查询的最近邻与现有方法相比,该方法对空间需求更小,编码长度更短,效率更高.模拟数据集和真实数据集上的实验结果表明,该方法不仅能够提高查询效率,而且方便调控在查询质量和查询处理时间方面的平衡问题.  相似文献
10.
Paxos是一个在不可靠的分布式处理器网络中解决共识问题的算法族.共识问题是指分布式系统中一组参与者就一个结果达成一致的过程.随着Paxos在大型分布式系统中的广泛运用,比如区块链系统以及谷歌文件系统等,其安全性证明越来越重要.本文在定理证明工具Coq中形式化描述和定义了Lamport的Basic Paxos算法,并且证明了其满足共识性.  相似文献
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号