期刊文献+
共找到23篇文章
< 1 2 >
每页显示 20 50 100
时间触发的机载无线通信网络确定性调度理论
1
作者 文秦 李士宁 +4 位作者 许江炜 纪源 肖林杰 李一鸣 程涛 《软件学报》 北大核心 2025年第11期5334-5355,共22页
为了满足航空器经济性的制造需求,降低航空器内部的有效载荷,使用无线代替有线已经成为机载网络转型升级的重要方向,然而传统无线技术难以满足机载网络中时间敏感业务的实时性传输需求.因此,通过明确机载无线通信网络(airborne wireless... 为了满足航空器经济性的制造需求,降低航空器内部的有效载荷,使用无线代替有线已经成为机载网络转型升级的重要方向,然而传统无线技术难以满足机载网络中时间敏感业务的实时性传输需求.因此,通过明确机载无线通信网络(airborne wireless communication network, AWCN)的应用特点,设计了AWCN结合机载骨干交换网络的混合拓扑架构;综合考虑了节点无冲突、信道无干扰、路径依赖与端到端时延需求,构建了时间触发的AWCN确定性调度应该满足的一阶逻辑形式;理论分析了不同信道数量下完成调度所需要的最少时隙数量与制约端到端时延的主要因素,并证明了稳态时数据流在网关处的信息年龄期望值;设计了基于整数规划的调度方法,并针对大规模网络中决策变量多、约束之间耦合性高而导致的求解效率低的缺陷,提出了一种增量式求解策略.最后,通过实验验证了确定性调度模型与理论分析的有效性,并讨论了不同调度影响因子对数据流总时延与调度规模的影响. 展开更多
关键词 机载无线通信网络 时间触发 确定性调度 约束求解器
在线阅读 下载PDF
高原铁路列车运行图与维修天窗协调优化研究 被引量:1
2
作者 邓智文 刘斌 +2 位作者 田志强 董傲冉 李和壁 《深圳大学学报(理工版)》 北大核心 2025年第2期216-225,共10页
针对高原铁路列车运行图与维修天窗之间的冲突问题,对高原铁路列车运行图与维修天窗进行协调优化.综合考虑列车服务水平约束、列车运行约束、列车运行图均衡性约束及维修天窗时间约束,建立列车总旅行时间最小和维修天窗开设总时长最大... 针对高原铁路列车运行图与维修天窗之间的冲突问题,对高原铁路列车运行图与维修天窗进行协调优化.综合考虑列车服务水平约束、列车运行约束、列车运行图均衡性约束及维修天窗时间约束,建立列车总旅行时间最小和维修天窗开设总时长最大的多目标混合整数规划模型.设计基于分层序列的多目标求解算法,运用Python编程调用杉数求解器(Cardinal optimizer,COPT)求解模型,并以高原铁路某区段为案例,验证模型有效性.结果表明,在考虑列车服务水平和列车运行图均衡性等约束前提下,本模型能够兼顾列车总旅行时间最短和维修天窗开设时长最长.基于最优解绘制的列车运行图表明,列车运行图和维修天窗的协调优化结果更符合高原铁路实际旅客运输生产作业需要.研究结果为铁路运营管理部门进一步优化列车运行图编制与维修天窗开设提供科学依据. 展开更多
关键词 高原铁路 列车运行图 维修天窗 列车运行约束 均衡性 混合整数规划 分层序列法 COPT求解器
在线阅读 下载PDF
Constraints Based Decision Support for Site-Specific Preliminary Design of Wind Turbines 被引量:1
3
作者 Abdelaziz Arbaoui Mohamed Asbik 《Energy and Power Engineering》 2010年第3期161-170,共10页
This study presents a decision-support tool for preliminary design of a horizontal wind turbine system. The function of this tool is to assist the various actors in making decisions about choices inherent to their act... This study presents a decision-support tool for preliminary design of a horizontal wind turbine system. The function of this tool is to assist the various actors in making decisions about choices inherent to their activities in the field of wind energy. Wind turbine cost and site characteristics are taken into account in the used models which are mainly based on the engineering knowledge. The present tool uses a constraint-modelling technique in combination with a CSP solver (numerical CSPs which are based on an arithmetic interval). In this way, it generates solutions and automatically performs the concept selection and costing of a given wind turbine. The data generated by the tool and required for decision making are: the quality index of solution (wind turbine), the amount of energy produced, the total cost of the wind turbine and the design variables which define the architecture of the wind turbine system. When applied to redesign a standard wind turbine in adequacy with a given site, the present tool proved both its ability to implement constraint modelling and its usefulness in conducting an appraisal. 展开更多
关键词 Wind TURBINE DECISION Support Preliminary Design Cost Modelling constraint SATISFACTION Problem (CSP) Digital CSP solver
暂未订购
语义推理驱动的协同装配技术 被引量:6
4
作者 万昌江 古飚 鲁玉军 《计算机集成制造系统》 EI CSCD 北大核心 2010年第9期1852-1858,共7页
为提高协同装配智能型和自动化程度,提出了语义推理驱动的智能装配技术。通过定义装配端口,建立装配元件之间连接关系的高级抽象表达;通过三维语义标注,构建产品三维形体与语义内容的关联,由此构建面向装配的产品本体模型。通过建立语... 为提高协同装配智能型和自动化程度,提出了语义推理驱动的智能装配技术。通过定义装配端口,建立装配元件之间连接关系的高级抽象表达;通过三维语义标注,构建产品三维形体与语义内容的关联,由此构建面向装配的产品本体模型。通过建立语义推理规则库及端口坐标系,实现装配连接关系的自动推理,并自动创建元件之间的配合操作关系。开发了基于自由度分析的三维约束求解引擎,基于推理结果自动求解变换矩阵,最终实现元件的自动装配。开发了智能协同装配原型系统并进行了试验,结果验证了该方法的有效性。 展开更多
关键词 装配 语义标注 推理规则 几何约束求解 三维形体 本体 产品设计
在线阅读 下载PDF
基于约束满足的卫星地面站资源优化分配问题研究 被引量:23
5
作者 贺仁杰 谭跃进 《计算机工程与应用》 CSCD 北大核心 2004年第18期229-232,共4页
卫星地面站资源优化分配问题是在给定的时间内,对卫星需要执行的任务分配地面站及执行时间,以便卫星能最大限度地完成任务。该文对该问题建立了CSP模型,并采用ILOGSolver对该模型进行求解。文中最后给出了一个应用实例,并比较了几种不... 卫星地面站资源优化分配问题是在给定的时间内,对卫星需要执行的任务分配地面站及执行时间,以便卫星能最大限度地完成任务。该文对该问题建立了CSP模型,并采用ILOGSolver对该模型进行求解。文中最后给出了一个应用实例,并比较了几种不同搜索算法和搜索策略的执行效率。 展开更多
关键词 约束满足问题 地面站资源分配 ILOG solver
在线阅读 下载PDF
基于反馈的可信网络软件验证与测试集成框架研究 被引量:1
6
作者 蒋凡 邢学智 章磊 《中国科学技术大学学报》 CAS CSCD 北大核心 2010年第2期197-202,共6页
形式化方法被认为是高可信软件工程必不可少的工具,但是软件测试依然是提高软件质量最有效的方法.为此基于TTCN-3的测试集成环境,提出一种基于反馈的框架,可扩展地集成形式化规约和形式化证明方法,并把形式化方法和测试工程有效地结合起... 形式化方法被认为是高可信软件工程必不可少的工具,但是软件测试依然是提高软件质量最有效的方法.为此基于TTCN-3的测试集成环境,提出一种基于反馈的框架,可扩展地集成形式化规约和形式化证明方法,并把形式化方法和测试工程有效地结合起来,提高了测试的充分性和必要性. 展开更多
关键词 高可信软件 模型驱动测试 符号执行 约束求解 UML TTCN-3
在线阅读 下载PDF
Excel规划求解水—岩作用模型 被引量:10
7
作者 何丽 周从直 +1 位作者 谢有奎 高银峰 《地下空间与工程学报》 CSCD 2008年第2期265-268,共4页
根据能量最低原则和化学热力学的基本原理,采用线性规划的方法,对水与岩石之间的相互作用进行模拟,建立了由目标函数和约束条件方程组构成的数学模型,利用Excel规划求解的功能对其进行求解。通过正确设置Excel规划求解参数的对话框,快... 根据能量最低原则和化学热力学的基本原理,采用线性规划的方法,对水与岩石之间的相互作用进行模拟,建立了由目标函数和约束条件方程组构成的数学模型,利用Excel规划求解的功能对其进行求解。通过正确设置Excel规划求解参数的对话框,快速而准确的求解出目标函数的最优解,揭示了水—岩相互作用的机理并得出了矿物溶蚀量。 展开更多
关键词 EXCEL 水-岩作用 规划求解 目标函数 约束条件
在线阅读 下载PDF
可满足性问题的约束求解器应用浅析 被引量:1
8
作者 付江龙 杨阳 +1 位作者 陈素军 赵天骄 《河北建筑工程学院学报》 CAS 2017年第2期132-134,共3页
约束求解问题涉及广泛,解决约束求解问题的一个重要方法就是SMT理论.本文介绍了两种利用SMT理论设计的约束求解器,分析了其求解原理和主要应用,并对以上两种约束求解器的优缺点进行探讨.约束求解器的研究为解决相对应的约束求解问题提... 约束求解问题涉及广泛,解决约束求解问题的一个重要方法就是SMT理论.本文介绍了两种利用SMT理论设计的约束求解器,分析了其求解原理和主要应用,并对以上两种约束求解器的优缺点进行探讨.约束求解器的研究为解决相对应的约束求解问题提供了思路和方法. 展开更多
关键词 约束求解 YICES HySat
在线阅读 下载PDF
一种可扩展型CLP系统的统一建模方法 被引量:2
9
作者 易军凯 翟性泉 王雪晶 《计算机工程与应用》 CSCD 北大核心 2004年第30期116-119,共4页
约束推理是人工智能中主要组成部分之一,可以解决实际优化调度和规划过程中的约束求解问题。这里在解释了约束逻辑程序设计的原理和过程基础上,打破封闭式约束逻辑程序设计系统,从软件工程上采用统一建模语言,提出一种新的开放的可扩展... 约束推理是人工智能中主要组成部分之一,可以解决实际优化调度和规划过程中的约束求解问题。这里在解释了约束逻辑程序设计的原理和过程基础上,打破封闭式约束逻辑程序设计系统,从软件工程上采用统一建模语言,提出一种新的开放的可扩展型约束逻辑程序设计结构系统。为实现可扩展的约束推理搜索系统,引进UML建模语言中用例图、类图和协作图。在建模基础上详细说明了可扩展约束逻辑程序设计中数学模型,搜索引擎和搜索驱动三者间的关系以及它们内部的工作内容。最后在描述系统结构后,提出了可扩展的内容。根据扩展因素,外界为满足更多的需要可扩展本系统的约束过滤器。 展开更多
关键词 约束逻辑程序设计 数学建模 搜索引擎 搜索求解器
在线阅读 下载PDF
具有约束条件的组合测试用例集的构建方法 被引量:1
10
作者 丁怀宝 高建华 《计算机工程与设计》 CSCD 北大核心 2010年第14期3189-3192,3206,共5页
针对如何为存在约束条件的软件系统生成尽可能小的组合测试用例集问题,提出了基于组合测试算法的约束组合测试法。该方法是对待测系统中的约束条件进行处理,将约束条件先转化为合取范式再转化为布尔表达式的形式。利用布尔可满足性求解... 针对如何为存在约束条件的软件系统生成尽可能小的组合测试用例集问题,提出了基于组合测试算法的约束组合测试法。该方法是对待测系统中的约束条件进行处理,将约束条件先转化为合取范式再转化为布尔表达式的形式。利用布尔可满足性求解器进行求解,找出满足约束条件的约束组合测试用例。最后运用AETG-SAT算法得到较优的组合测试用例集,并通过实验表明了AETG-SAT算法的优越性。 展开更多
关键词 组合测试 约束条件 合取范式 布尔表达式 可满足性求解器
在线阅读 下载PDF
基于Web Services的开放式分布计算求解器的设计与实现
11
作者 何伟 孔梦荣 车战斌 《郑州轻工业学院学报(自然科学版)》 CAS 2006年第4期69-71,共3页
设计了基于Web服务的开放式分布计算求解器系统.该分布式计算求解器能够充分利用网络的软硬件资源,将网络上的多个求解器通过互相协调共同解决一个等式约束问题.采用该方案的计算求解器是安全、高效的,具有健壮性.
关键词 分布计算求解器 等式约束 分布计算 MATHML 文档对象模型 WEB服务
在线阅读 下载PDF
线性规划在缓冲区溢出检测中的应用研究
12
作者 葛小凯 白振兴 +1 位作者 魏剑简 张娜 《微计算机信息》 2009年第27期85-86,84,共3页
文中建立了一个缓冲区溢出检测模型,用整型区间约束系统来表示字符串和关键性函数,将C字符串操作抽象成线性规划问题来解决。设计了线性求解器对所产生的约束集合进行求解,进而确定缓冲区的界,然后用溢出条件判定漏洞是否发生。最后在wu... 文中建立了一个缓冲区溢出检测模型,用整型区间约束系统来表示字符串和关键性函数,将C字符串操作抽象成线性规划问题来解决。设计了线性求解器对所产生的约束集合进行求解,进而确定缓冲区的界,然后用溢出条件判定漏洞是否发生。最后在wu-ftp-2.6.2上验证了该方法在检测缓冲区溢出上的可行性和有效性,并通过横向比较证明了其线性执行时间的效率。 展开更多
关键词 约束 线性规划求解器 缓冲区溢出 静态分析
在线阅读 下载PDF
基于SMT求解器的微处理器指令验证数据约束生成技术 被引量:6
13
作者 谭坚 罗巧玲 +3 位作者 王丽一 胡夏晖 范昊 徐占 《计算机研究与发展》 EI CSCD 北大核心 2020年第12期2694-2702,共9页
处理器研制过程中需要对指令算术数据路径进行覆盖验证.针对现有模拟验证方法存在的不足,提出了一种基于可满足模理论(satisfiability modulo theory,SMT)的指令约束求解方法:利用可满足模理论求解器将指令级功能验证任务转化成数据约... 处理器研制过程中需要对指令算术数据路径进行覆盖验证.针对现有模拟验证方法存在的不足,提出了一种基于可满足模理论(satisfiability modulo theory,SMT)的指令约束求解方法:利用可满足模理论求解器将指令级功能验证任务转化成数据约束求解满足问题.在结果操作数约束、操作数间约束、指令内部约束以及浮点操作数约束4个方面分别给出示例,并分别给出了利用SMT求解器进行约束建模的关键过程以及可以用于指令级功能验证的元组数据.为提高求解模型效率,提出了2种解决方法:首先利用时间阈值实现问题求解超时即终止的策略;其次是结合进程管理与线程管理技术,实现了指令功能约束并行求解框架,将串行求解任务分派给可并行执行的多个线程,提高了求解速度.该技术已成功应用于系统级验证中,有效提升了测试覆盖与质量,取得了很好的效益. 展开更多
关键词 指令功能 数据路径 约束求解 SMT求解器 验证数据 并行加速
在线阅读 下载PDF
基于约束的几何造型系统 被引量:1
14
作者 薛丽霞 唐忠民 邓家禔 《工程设计学报》 CSCD 2001年第1期21-24,共4页
提出了一种基于约束的造型系统模型 ,通过约束网、约束求解器与实体特征表示、实体的边界表示 ,获得一致的实时更新的实体 。
关键词 几何设计 自由度 约束求解器 几何造型系统 约束网 工程设计
在线阅读 下载PDF
一种基于自由度分析的过约束处理方法
15
作者 朱立 《价值工程》 2010年第20期142-143,共2页
特征造型是建立形体的产品信息模型,实现CAD/CAM一体化,支持设计和制造全过程的新兴造型技术。参数化设计可以使CAD系统具有交互式绘图功能以及自动绘图功能。参数化设计的关键是几何约束关系的提取和表达,几何约束的求解及参数化几何... 特征造型是建立形体的产品信息模型,实现CAD/CAM一体化,支持设计和制造全过程的新兴造型技术。参数化设计可以使CAD系统具有交互式绘图功能以及自动绘图功能。参数化设计的关键是几何约束关系的提取和表达,几何约束的求解及参数化几何模型构造。约束求解是将特征间的相互依赖关系映射为几何或工程约束描述,通过求解约束实现设计对象的细节。本文提出了一种基于自由度分析的过约束处理方法。 展开更多
关键词 参数化设计 特征设计 几何约束 约束求解
在线阅读 下载PDF
使用共享变量分析和约束求解检测安卓应用数据竞争 被引量:1
16
作者 孙全 许蕾 +1 位作者 夏昕濛 张卫丰 《软件学报》 EI CSCD 北大核心 2019年第11期3281-3296,共16页
安卓系统在移动端操作系统始终占据主导地位,在增强用户体验和提高程序性能的同时,其特有的事件驱动模型和多线程模型也造成了并发缺陷.并发程序中,线程调度的不确定性和难以再现性是并发缺陷检测困难的原因.现有技术主要在动态生成执... 安卓系统在移动端操作系统始终占据主导地位,在增强用户体验和提高程序性能的同时,其特有的事件驱动模型和多线程模型也造成了并发缺陷.并发程序中,线程调度的不确定性和难以再现性是并发缺陷检测困难的原因.现有技术主要在动态生成执行路径的基础上进行发生序(happens-before)分析,进而检测安卓应用的并发缺陷,但仍然存在低覆盖率、误报、漏报等问题.结合共享变量分析和约束求解方法实现了安卓应用数据竞争的检测,并实现了检测工具RaceDetector.该工具首先根据安卓系统的特性和数据竞争的定义,通过静态分析抽取相关信息,并进一步使用安卓共享变量分析来提高准确性和性能,继而进行可疑数据竞争分析,得出可疑的数据竞争集合;接着根据每一个可疑的数据竞争候选者,通过约束求解的方法在所有事件调度和线程调度解空间下识别发生序关系,并最终检测出真正的数据竞争.实验部分是从Google Play等来源收集了15个流行的应用APK文件作为数据集,RaceDetector平均报告了340个数据竞争,误报率为13%(44/340).与现有工具EventRacer(默认产生300随机事件触发应用执行,平均检测2个有害数据竞争)相比,RaceDetector能够解析全部源码,覆盖了所有线程调度和事件调度,平均检测出15个有害数据竞争. 展开更多
关键词 安卓应用 数据竞争 事件驱动模型 多线程模型 约束求解
在线阅读 下载PDF
基于动态符号执行的勒索软件检测方法 被引量:3
17
作者 陈政 方勇 +1 位作者 刘亮 左政 《计算机工程》 CAS CSCD 北大核心 2018年第6期104-110,共7页
针对目前因勒索软件造成网络安全事故的问题,在对大量勒索软件样本进行分析的基础上,提出一种基于动态符号执行的勒索软件检测与分析方法。基于插桩工具Pin和约束求解器STP构建ADRAS系统模型,利用动态符号执行和可满足性模理论技术监控... 针对目前因勒索软件造成网络安全事故的问题,在对大量勒索软件样本进行分析的基础上,提出一种基于动态符号执行的勒索软件检测与分析方法。基于插桩工具Pin和约束求解器STP构建ADRAS系统模型,利用动态符号执行和可满足性模理论技术监控勒索软件的加密函数,同时捕捉勒索软件加密行为以及相关的加密信息,从而对多个家族的勒索软件进行检测。实验结果表明,ADRAS系统模型可检测15种已知勒索软件家族的样本,包括著名的CryptoLocker以及最近爆发的WannaCry。 展开更多
关键词 勒索软件 动态符号执行 约束求解器 混合加密算法 恶意代码
在线阅读 下载PDF
COMPSPEN:对形状性质与数据约束进行融合推理的分离逻辑求解器 被引量:1
18
作者 苏婉昀 高冲 +1 位作者 古新才 吴志林 《软件学报》 EI CSCD 北大核心 2023年第5期2181-2195,共15页
分离逻辑是经典霍尔逻辑的针对操作指针和动态数据结构的扩展,已经广泛用于对基础软件(比如操作系统内核等)的分析与验证.分离逻辑约束自动求解是提升对操作指针和动态数据结构的程序的验证的自动化程度的重要手段.针对动态数据结构的... 分离逻辑是经典霍尔逻辑的针对操作指针和动态数据结构的扩展,已经广泛用于对基础软件(比如操作系统内核等)的分析与验证.分离逻辑约束自动求解是提升对操作指针和动态数据结构的程序的验证的自动化程度的重要手段.针对动态数据结构的验证一般同时涉及形状性质(比如单链表、双链表、树等)和数据性质(比如有序性、数据不变性等).主要介绍能对动态数据结构的形状性质与数据约束进行融合推理的分离逻辑求解器COMPSPEN.首先介绍COMPSPEN的理论基础,包括能够同时描述线性动态数据结构的形状性质和数据约束的分离逻辑子集SLIDdata、SLIDdata的可满足性和蕴涵问题的判定算法.然后,介绍COMPSPEN工具的基本框架.最后,使用COMPSPEN工具进行了实例研究.收集整理了600个测试用例,在这600个测试用例上将COMPSPEN与已有的主流分离逻辑求解器Asterix、S2S、Songbird、SPEN进行了比较.实验结果表明COMPSPEN是唯一能够求解含有集合数据约束的分离逻辑求解器,而且总体来讲,能对线性数据结构上的同时含有形状性质和线性算术数据约束的分离逻辑公式的可满足性问题进行高效的求解,另外,也能对蕴涵问题进行求解. 展开更多
关键词 分离逻辑 形状性质 线性算术数据约束 集合数据约束 可满足性问题 蕴涵问题 约束求解器
在线阅读 下载PDF
基于控制流分析的导向性灰盒模糊测试方法 被引量:1
19
作者 黎君玉 罗琴 刘智 《电子测量技术》 北大核心 2022年第15期21-27,共7页
模糊测试(Fuzzing)是软件漏洞挖掘的主要技术,它能随机生成测试用例并动态执行程序,可以覆盖较深的分支。但模糊测试技术中变异存在一定的盲目性,并且随机变异样本执行相同路径的频率很高,导致变异样本冗余,从而降低测试效率。本文提出... 模糊测试(Fuzzing)是软件漏洞挖掘的主要技术,它能随机生成测试用例并动态执行程序,可以覆盖较深的分支。但模糊测试技术中变异存在一定的盲目性,并且随机变异样本执行相同路径的频率很高,导致变异样本冗余,从而降低测试效率。本文提出并实现了一种基于控制流分析的导向性灰盒模糊测试方法CTM。CTM首先对目标二进制程序进行静态分析获取程序控制流图,再根据程序控制流分析程序路径执行稀有度,接着识别执行路径上敏感函数来计算程序执行路径比重,并且求解生成测试用例;其次在模糊测试过程中,对非格式关键信息位置进行变异;最后根据支路覆盖反馈信息,利用启发式规则对执行路径约束信息进行求解,来生成新测试用例样本。CTM通过引导性的测试用例和定位变异方法,提高模糊测试生成满足复杂分支条件测试用例的概率,从而提高代码覆盖率和减少变异样本冗余。为了验证本方法有效性,本文选择readelf、gif2png等真实应用程序进行测试,并与业界主流Fuzzing软件Driller和AFL进行对比测试,测试结果表明,CTM发现crash和探索新路径的能力都有所提高。 展开更多
关键词 符号执行 模糊测试 控制流图 约束求解 测试用例
原文传递
结合混合符号执行的导向式灰盒模糊测试技术 被引量:5
20
作者 戴渭 陆余良 朱凯龙 《计算机工程》 CAS CSCD 北大核心 2020年第8期190-196,共7页
导向式灰盒模糊测试是一种能够快速生成测试用例,达到给定程序目标区域并且发现漏洞的模糊测试技术。针对当前导向式模糊测试难以通过魔术字节等检查语句,且对目标区域路径覆盖率较低的问题,提出结合混合符号执行的导向式灰盒模糊测试... 导向式灰盒模糊测试是一种能够快速生成测试用例,达到给定程序目标区域并且发现漏洞的模糊测试技术。针对当前导向式模糊测试难以通过魔术字节等检查语句,且对目标区域路径覆盖率较低的问题,提出结合混合符号执行的导向式灰盒模糊测试方法。通过跟踪种子的执行路径,使用约束求解器对种子的遗传变异加以辅助,生成能够通过检查语句的测试用例,从而对目标区域进行有效测试。实验结果表明,该测试方法能够提高导向式模糊测试对目标区域的覆盖率。 展开更多
关键词 导向式灰盒模糊测试 动态能量调控 混合符号执行 遗传变异 约束求解器
在线阅读 下载PDF
上一页 1 2 下一页 到第
使用帮助 返回顶部