期刊文献+
共找到17篇文章
< 1 >
每页显示 20 50 100
基于启发式on-the-fly的扩展TGBA模型检测算法 被引量:1
1
作者 王曦 徐中伟 《计算机学报》 EI CSCD 北大核心 2014年第12期2519-2529,共11页
以广义Büchi自动机为研究对象,对其作判空检测能为解决系统的状态空间爆炸问题提供有效途径.但广义Büchi自动机难以适用于安全苛求计算机系统中,只需满足某个可接受条件子集便可作出非空性判断,进而能判断出系统的安全性的情... 以广义Büchi自动机为研究对象,对其作判空检测能为解决系统的状态空间爆炸问题提供有效途径.但广义Büchi自动机难以适用于安全苛求计算机系统中,只需满足某个可接受条件子集便可作出非空性判断,进而能判断出系统的安全性的情形.文中提出了基于启发式on-the-fly的扩展TGBA模型检测算法,该算法采用ETGBA模型,通过启发式on-the-fly判空检测方法对ETGBA作判空检测时,加强了对不能构成其可接受运行的结点的处理,节省了内存空间,提高了检测效率,从而能较快地作出非空性判断.通过算法的正确性证明及复杂度分析、实验比较与实例研究验证了所提出算法的正确性与实际可行性.与已有算法相比,该算法的通用性更强,当应用于广义Büchi自动机的判空检测时,其时空性能均优于已有算法. 展开更多
关键词 模型检测 广义Btichi自动机 on-the-fly算法 安全性分析
下载PDF
基于on-the-fly的Petri网模型检查技术研究与实现 被引量:1
2
作者 沈云付 解晓方 《计算机应用与软件》 CSCD 2011年第5期82-85,共4页
Petri网是一种应用非常广泛的建模工具,它能深刻、简洁地描述控制系统,特别是能较好地描述并发系统的结构,并能对系统的动态性质进行分析。在探讨了Petri网的模型检查的基础上,采用双DFS算法,对基于Petri网的模型检查的算法进行了改进,... Petri网是一种应用非常广泛的建模工具,它能深刻、简洁地描述控制系统,特别是能较好地描述并发系统的结构,并能对系统的动态性质进行分析。在探讨了Petri网的模型检查的基础上,采用双DFS算法,对基于Petri网的模型检查的算法进行了改进,提出了针对Petri网的on-the-fly算法,同时给出了基于on-the-fly的Petri网模型检查的实现和测试,从而可以有效地对Petri网表示的系统模型进行模型检查。 展开更多
关键词 模型检查 PETRI网 on-the-fly技术 自动机 双DFS算法
下载PDF
CPN建模与on-the-fly方法相结合的测试用例生成 被引量:1
3
作者 张玉荣 李华 +3 位作者 邢熠 王显荣 阮宏玮 张素梅 《软件学报》 EI CSCD 北大核心 2017年第10期2564-2582,共19页
在对复杂的软件系统进行测试时,生成的系统状态空间可能会非常庞大.为了避免对整个状态空间进行遍历,提出将on-the-fly方法与CPN形式化建模方法结合起来,用于生成测试例.在这种方法中,无需对整个状态空间进行遍历,只是仅对测试人员感兴... 在对复杂的软件系统进行测试时,生成的系统状态空间可能会非常庞大.为了避免对整个状态空间进行遍历,提出将on-the-fly方法与CPN形式化建模方法结合起来,用于生成测试例.在这种方法中,无需对整个状态空间进行遍历,只是仅对测试人员感兴趣的部分状态空间进行针对性的测试.首先,给出CPN和扩展可达图的定义,介绍了on-the-fly测试方法中涉及的相关概念,包括系统规约、测试目的、同步乘积和测试例等.然后,实现了同步乘积算法,并设计相关测试例对其进行了测试.最后,选定一个被测系统示例CPN建模与on-the-fly结合的方法,并通过适配器实现与被测系统的交互,生成和执行测试例,由此验证了方法的可行性和有效性. 展开更多
关键词 on-the-fly测试 CPN层次模型 扩展可达图 同步乘积 测试例
下载PDF
威胁驱动的Web应用On-The-Fly导航模型验证方法 被引量:1
4
作者 胡立立 缪淮扣 +2 位作者 陈圣波 梅佳 高洪皓 《应用科学学报》 EI CAS CSCD 北大核心 2011年第1期83-91,共9页
以Web应用为代表的网络软件安全性受到业界的广泛关注,对具有复杂交互行为的Web应用安全性建模和验证是一个挑战.该文提出一种威胁驱动的Web应用On-the-Fly导航模型验证方法,采用威胁驱动方法从规格说明中设计和抽取用于性质检验的安全... 以Web应用为代表的网络软件安全性受到业界的广泛关注,对具有复杂交互行为的Web应用安全性建模和验证是一个挑战.该文提出一种威胁驱动的Web应用On-the-Fly导航模型验证方法,采用威胁驱动方法从规格说明中设计和抽取用于性质检验的安全性质,利用模型检测工具NuSMV对建立的模型进行验证.实验结果表明该方法可以减少搜索空间并在一定程度上避免状态空间爆炸. 展开更多
关键词 on-the-fly验证 WEB应用 安全性
下载PDF
Hybrid windowed networks for on-the-fly Doppler broadening in RMC code 被引量:2
5
作者 Tian-Yi Huang Ze-Guang Li +2 位作者 Kan Wang Xiao-Yu Guo Jin-Gang Liang 《Nuclear Science and Techniques》 SCIE EI CAS CSCD 2021年第6期70-82,共13页
On-the-fly Doppler broadening of cross sections is important in Monte Carlo simulations,particularly in Monte Carlo neutronics-thermal hydraulics coupling simulations.Methods such as Target Motion Sampling(TMS)and win... On-the-fly Doppler broadening of cross sections is important in Monte Carlo simulations,particularly in Monte Carlo neutronics-thermal hydraulics coupling simulations.Methods such as Target Motion Sampling(TMS)and windowed multipole as well as a method based on regression models have been developed to solve this problem.However,these methods have limitations such as the need for a cross section in an ACE format at a given temperature or a limited application energy range.In this study,a new on-the-fly Doppler broadening method based on a Back Propagation(BP)neural network,called hybrid windowed networks(HWN),is proposed to resolve the resonance energy range.In the HWN method,the resolved resonance energy range is divided into windows to guarantee an even distribution of resonance peaks.BP networks with specially designed structures and training parameters are trained to evaluate the cross section at a base temperature and the broadening coefficient.The HWN method is implemented in the Reactor Monte Carlo(RMC)code,and the microscopic cross sections and macroscopic results are compared.The results show that the HWN method can reduce the memory requirement for cross-sectional data by approximately 65%;moreover,it can generate keff,power distribution,and energy spectrum results with acceptable accuracy and a limited increase in the calculation time.The feasibility and effectiveness of the proposed HWN method are thus demonstrated. 展开更多
关键词 Monte Carlo method Reactor Monte Carlo(RMC) on-the-fly Doppler broadening BP network
下载PDF
On-the-fly Doppler broadening method based on optimal doubleexponential formula
6
作者 Rui Chen Li-Juan Hao +2 位作者 Bin Wu Jing Song Li-Qin Hu 《Nuclear Science and Techniques》 SCIE CAS CSCD 2017年第11期251-257,共7页
As temperature changes constantly in nuclear reactor operation, on-the-fly Doppler broadening methods are commonly adopted for generating nuclear cross sections at various temperatures in neutron transport simulation.... As temperature changes constantly in nuclear reactor operation, on-the-fly Doppler broadening methods are commonly adopted for generating nuclear cross sections at various temperatures in neutron transport simulation. Among the existing methods, the widely used SIGMA1 approach is inefficient because it involves error function and Taylor series expansion. In this paper, we present a new on-the-fly Doppler broadening with optimal double-exponential formula based on SuperMC to improve efficiency with given accuracy. In this method, doubleexponential formula in 1/16 steps is used for broadening cross section at low energy, with both accuracy and efficiency. Meanwhile, the Gauss–Hermite quadrature of different orders is used for broadening cross section at resonance energy. The method can generate neutron cross section rapidly and precisely at the desired temperature.Typical nuclide cross sections and benchmarking tests are presented in detail. 展开更多
关键词 on-the-fly DOPPLER BROADENING CROSS SECTION Double-exponential FORMULA SuperMC
下载PDF
Swarming magnetic photonic-crystal microrobots withon-the-fly visual pH detection and self-regulated drug delivery
7
作者 Zheng Yu Luolin Li +8 位作者 Fangzhi Mou Shimin Yu Di Zhang Manyi Yang Qing Zhao Huiru Ma Wei Luo Tianlong Li Jianguo Guan 《InfoMat》 SCIE CSCD 2023年第10期64-79,共16页
Swarming magnetic micro/nanorobots hold great promise for biomedical applications,but at present suffer from inferior capabilities to perceive and respond to chemical signals in local microenvironments.Here we demonst... Swarming magnetic micro/nanorobots hold great promise for biomedical applications,but at present suffer from inferior capabilities to perceive and respond to chemical signals in local microenvironments.Here we demonstrate swarming magnetic photonic crystal microrobots(PC-bots)capable of sponta-neously performing on-the-fly visual pH detection and self regulated drug delivery by perceiving local pH changes.The magnetic PC-bots consist of pH-responsive hydrogel microspheres with encapsulated one-dimensional periodic assemblies of Fe3O4 nanoparticles.By programming extemnal rotating magnetic fields,they can self-organize into large swarms with much-enhanced collective velocity to actively find targets while shining bright“blinking”structural colors.When approaching the target with abnormal pH conditions(e.g.an ulcerated superficial tumor lesion),the PC-bots can visualize local pH changes on the fly via pH-responsive structural colors,and realize self-regulated release of the loaded drugs by recognizing local pH.This work facilita tes the develop-ment of intelligent micro/nanorobots for active“motile-targeting”tumor diag-nosis and treatment. 展开更多
关键词 collective behaviors drug delivery micro/nanorobots on-the-fly sensing responsivephotonic crystals
原文传递
Swarming Responsive Photonic Nanorobots for Motile-Targeting Microenvironmental Mapping and Mapping-Guided Photothermal Treatment 被引量:3
8
作者 Luolin Li Zheng Yu +7 位作者 Jianfeng Liu Manyi Yang Gongpu Shi Ziqi Feng Wei Luo Huiru Ma Jianguo Guan Fangzhi Mou 《Nano-Micro Letters》 SCIE EI CAS CSCD 2023年第9期205-223,共19页
Micro/nanorobots can propel and navigate in many hard-to-reach biological environments,and thus may bring revolutionary changes to biomedical research and applications.However,current MNRs lack the capability to colle... Micro/nanorobots can propel and navigate in many hard-to-reach biological environments,and thus may bring revolutionary changes to biomedical research and applications.However,current MNRs lack the capability to collectively perceive and report physicochemical changes in unknown microenvironments.Here we propose to develop swarming responsive photonic nanorobots that can map local physicochemical conditions on the fly and further guide localized photothermal treatment.The RPNRs consist of a photonic nanochain of periodically-assembled magnetic Fe_(3)O_(4)nanoparticles encapsulated in a responsive hydrogel shell,and show multiple integrated functions,including energetic magnetically-driven swarming motions,bright stimuli-responsive structural colors,and photothermal conversion.Thus,they can actively navigate in complex environments utilizing their controllable swarming motions,then visualize unknown targets(e.g.,tumor lesion)by collectively mapping out local abnormal physicochemical conditions(e.g.,pH,temperature,or glucose concentra-tion)via their responsive structural colors,and further guide external light irradiation to initiate localized photothermal treatment.This work facilitates the development of intelligent motile nanosensors and versatile multifunctional nanotheranostics for cancer and inflam-matory diseases. 展开更多
关键词 Micro/nanorobots Collective behaviors Responsive photonic crystals on-the-fly sensing Photothermal therapy
下载PDF
基于启发式NDFS的模型检测新算法 被引量:1
9
作者 王曦 徐中伟 《小型微型计算机系统》 CSCD 北大核心 2012年第8期1740-1746,共7页
以带有多个可接受条件的广义Büchi自动机为研究对象,提出基于启发式NDFS的模型检测新算法.该算法结合on-the-fly算法与启发式NDFS算法,能较快地判断出广义Büchi自动机非空性,通过理论证明和实验验证了算法的正确性和可行性.... 以带有多个可接受条件的广义Büchi自动机为研究对象,提出基于启发式NDFS的模型检测新算法.该算法结合on-the-fly算法与启发式NDFS算法,能较快地判断出广义Büchi自动机非空性,通过理论证明和实验验证了算法的正确性和可行性.与已有算法相比,在广义Büchi自动机非空的情况下,该算法减少了系统状态空间的搜索,提高了检测效率,且能形成相应反例,为缓解形式化验证中的状态空间爆炸问题提供了有效的解决途径,为安全苛求系统的安全性保障提供了有力支撑,丰富了基于模型的软件形式化开发方法. 展开更多
关键词 模型检测 启发式NDFS 安全性验证 on-the-fly算法 BÜCHI自动机
下载PDF
基于启发式SCCs的广义Büchi自动机判空检测算法 被引量:1
10
作者 王曦 徐中伟 《电子学报》 EI CAS CSCD 北大核心 2012年第1期95-102,共8页
基于自动机理论模型检测的一个关键算法是判断有穷状态系统是否满足属性的判空检测.对标准Büchi自动机作判空检测,容易引起状态爆炸.本文以TGBA为研究对象,提出基于启发式SCCs的广义Büchi自动机判空检测算法.该算法在on-the-... 基于自动机理论模型检测的一个关键算法是判断有穷状态系统是否满足属性的判空检测.对标准Büchi自动机作判空检测,容易引起状态爆炸.本文以TGBA为研究对象,提出基于启发式SCCs的广义Büchi自动机判空检测算法.该算法在on-the-fly算法的基础上结合启发式深度优先搜索和SCCs检测算法,能较快地判断TGBA的非空性.通过正确性证明、复杂性分析和实验验证了该算法的正确可行性.在TGBA非空的情况下,该算法的时空性能比已有算法更优. 展开更多
关键词 模型检测 BÜCHI自动机 on-the-fly算法 判空检测
下载PDF
移动Ad Hoc网络路由修复算法研究 被引量:1
11
作者 高巍巍 李晓峰 丁树春 《计算机与数字工程》 2014年第4期573-577,共5页
针对移动Ad Hoc网络路由算法本地修复方面,研究移动Ad Hoc网络由于节点相对运动或无线环境变化所引起的链路失效的修复问题。分析传统的本地修复方式采用全网泛洪所产生的大量控制开销对业务传输时延及分组成功交付率等方面产生的影响... 针对移动Ad Hoc网络路由算法本地修复方面,研究移动Ad Hoc网络由于节点相对运动或无线环境变化所引起的链路失效的修复问题。分析传统的本地修复方式采用全网泛洪所产生的大量控制开销对业务传输时延及分组成功交付率等方面产生的影响。采用基于on-the-fly策略的移动Ad Hoc网络路由修复算法研究,构造了将修复请求区域限制在两跳范围内的修复模型,并建立相应的修复函数,从而实现在满足修复概率的前提下降低网络泛洪与控制开销的目标。 展开更多
关键词 移动AD HOC网络 路由修复 on-the-fly策略 泛洪控制
下载PDF
Web服务组合的互模拟验证 被引量:2
12
作者 袁勇福 高春鸣 刘荣胜 《计算机应用》 CSCD 北大核心 2006年第10期2466-2469,共4页
为检验Web服务组合的实现与用户需求的一致性,在开互模拟形式化理论和检验工具的基础上,提出了一个自动化检验方法。首先,用π-演算分别对用户需求和商业流程可执行语言(BPEL4WS)程序实现建模,然后对它们进行弱开互模拟检验,当它们不互... 为检验Web服务组合的实现与用户需求的一致性,在开互模拟形式化理论和检验工具的基础上,提出了一个自动化检验方法。首先,用π-演算分别对用户需求和商业流程可执行语言(BPEL4WS)程序实现建模,然后对它们进行弱开互模拟检验,当它们不互模拟时,检验工具能自动标识关键的不互模拟的BPEL4WS程序片段。最后通过实例说明这一方法的可行性。 展开更多
关键词 Π-演算 商业流程可执行语言 开互模拟 on-the-fly算法 模型验证
下载PDF
基于偏序规约技术的网络程序JPF验证
13
作者 杨翰文 龙士工 谢光颖 《计算机工程与设计》 CSCD 北大核心 2014年第6期2004-2008,共5页
为了减少网络程序模型检测过程中产生的系统状态数目,提出了一种架构感知偏序规约方案。针对目前模型检测器JPF内置的偏序规约机制不能够识别出线程启动时产生的冗余状态问题,设计了一种可应用于JPF的网络程序模型检测的解决方案。该方... 为了减少网络程序模型检测过程中产生的系统状态数目,提出了一种架构感知偏序规约方案。针对目前模型检测器JPF内置的偏序规约机制不能够识别出线程启动时产生的冗余状态问题,设计了一种可应用于JPF的网络程序模型检测的解决方案。该方案通过消除线程启动时产生的冗余路径,有效减少了检测过程中产生的状态空间。实验结果表明,该方案能够有效消除对冗余状态的检测,减少了JPF对网络程序进行模型检测时产生的状态数。 展开更多
关键词 模型检测 状态爆炸 偏序规约 on-the-fly技术 程序验证
下载PDF
基于ARM的ZDMA传输设计与实现
14
作者 韩洋 周煦林 《计算机技术与发展》 2012年第3期195-198,共4页
DMA技术是一种由DMA控制器控制的存储器与外部设备或存储器之间大数据量传输的技术,具有传输速度高、CPU额外开销小的优点。ARM微处理器是32位RISC处理器,具有低功耗、高性价比等特点。文中介绍了一种使用ARM在外设与系统Memory之间实现... DMA技术是一种由DMA控制器控制的存储器与外部设备或存储器之间大数据量传输的技术,具有传输速度高、CPU额外开销小的优点。ARM微处理器是32位RISC处理器,具有低功耗、高性价比等特点。文中介绍了一种使用ARM在外设与系统Memory之间实现DMA On-the-fly模式传输的设计方法,硬件部分基于S3C44B0X的ARM7 TDMI微处理器,通过一个ZDMA控制器实现ARM7与系统外设间的通信,将CPU从繁杂的I/O事务中解放出来,解决了原有系统中因采用中断和轮询方式进行传输而导致的系统瓶颈,使得整个系统的速度与传输效率大大提升。 展开更多
关键词 ARM ZDMA 完全服务模式 on-the-fly模式 UART
下载PDF
高效乘除法器的设计研究
15
作者 胡振波 曾强辉 +1 位作者 毛志刚 张学鹏 《信息技术》 2010年第3期48-51,共4页
在某些复杂通信与多媒体算法中经常出现乘除法(A*B/C)运算,利用二进制补码乘法与除法的相似性,提出了一种高效的实现方式。该乘除法器使用冗余的商选择机制与两级CSA结构,在复用除法硬件资源的基础上即可完成乘法操作。32比特乘法可在1... 在某些复杂通信与多媒体算法中经常出现乘除法(A*B/C)运算,利用二进制补码乘法与除法的相似性,提出了一种高效的实现方式。该乘除法器使用冗余的商选择机制与两级CSA结构,在复用除法硬件资源的基础上即可完成乘法操作。32比特乘法可在11个时钟周期完成,除法在16个周期完成,故32比特的乘除法运算(A*B/C)可在27个周期完成,与传统的实现方式相比,总时钟数大为缩短,且具有设计复杂度低,面积小等优点。 展开更多
关键词 乘法器 除法器 基2的booth编码 CSA on-the-fly转换
下载PDF
基于LTL语义的可达性控制器合成工具
16
作者 景丽莎 项周坤 《计算机系统应用》 2016年第11期22-28,共7页
控制器合成是针对给定的获胜目标,在开放的实时系统环境中,自动地寻找获胜策略的过程.这个策略可以表述为一系列的符号化状态和动作的映射关系.在本文中,我们主要针对以线性时序逻辑(LTL)描述的可达性作为获胜目标,进行合成策略的发现.... 控制器合成是针对给定的获胜目标,在开放的实时系统环境中,自动地寻找获胜策略的过程.这个策略可以表述为一系列的符号化状态和动作的映射关系.在本文中,我们主要针对以线性时序逻辑(LTL)描述的可达性作为获胜目标,进行合成策略的发现.文中介绍了一种采用on-the-fly思路的合成算法,以规避状态数目太多带来的内存溢出问题.文中算法是对文献[1]的一种扩展,该算法主要用于解决基于分支时序逻辑(CTL)的控制器合成.另外,我们实现了相关的控制器合成工具CTAV/TGA(Timed Gamed Automata),在实现的过程中,使用on-the-fly的方式,避免了穷尽状态空间,同时,通过使用zone和抽象,大大缩减了状态数目,使时空效率控制在可接受的范围内. 展开更多
关键词 时间博弈自动机 控制器合成 线性时序逻辑(LTL) on-the-fly 符号化方法
下载PDF
Efficient approach of translating LTL formulae into Biichi automata
17
作者 Laixiang SHAN Xiaomin DU Zheng QIN 《Frontiers of Computer Science》 SCIE EI CSCD 2015年第4期511-523,共13页
In explicit-state model checking, system proper- ties are typically expressed in linear temporal logic (LTL), and translated into a BUchi automaton (BA) to be checked. In order to improve performance of the conver... In explicit-state model checking, system proper- ties are typically expressed in linear temporal logic (LTL), and translated into a BUchi automaton (BA) to be checked. In order to improve performance of the conversion algo- rithm, some model checkers involve the intermediate au- tomata, such as a generalized Btichi automaton (GBA). The de-generalization is a translation from a GBA to a BA. In this paper, we present a conversion algorithm to translate an LTL formula to a BA directly. A labeling, acceptance degree, is presented to record acceptance conditions sat- isfied in each state and transition. Acceptance degree is a set of U-subformulae or F-subformulae of the given LTL formula. According to the acceptance degree, on-the-fly de- generalization algorithm, which is different from the standard de-generalization algorithm, is conceived and implemented. On-the-fly de-generalization algorithm is carried out during the expansion of the given LTL formula. It is performed in the case of the given LTL formula contains U-subformulae and F-subformulae, that is, the on-the-fly de-generalization algorithm is performed as required. In order to get a more deterministic BA, the shannon expansion is used recursively during expanding LTL formulae. Ordered binary decision diagrams are used to represent the BA and simplify LTL formulae. We compare the conversion algorithm presented in this paper to previous works, and show that it is more efficient for five families LTL formulae in common use and four setsof random formulae generated by LBTT (an LTL-to-BUchi translator testbench). 展开更多
关键词 model checking Btichi automata acceptancedegree on-the-fly de-generalization
原文传递
上一页 1 下一页 到第
使用帮助 返回顶部