基于关键迹和ASP的CSP模型检测

模型检测是通信顺序进程(communicating sequential processes,简称CSP)形式化验证的重要手段.当前, CSP模型检测方法基于操作语义,需将进程转化为迁移系统,进而提取语义模型,但转化过程较为复杂;待验证性质采用CSP语言进行描述,虽然有利于精炼检测(refinement checking),但描述能力较弱,通用性不强.鉴于此,提出了一种新的CSP指称语义模型——关键迹模型(critical-trace model)及基于该指称语义模型的CSP模型检测方法,并证明了其验证的可靠性,避免了上述问题.关键迹模型采用递归策略计算,待验证性质采用线性时态逻辑(linear temporal logic,简称LTL)描述.基于回答集程序设计(answer set programming,简称ASP)实现了关键迹模型的自动生成及LTL的自动验证,并开发了一个CSP模型检测原型系统——T_ASP.实验结果表明:与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,且可同时验证多条性质,在性质不满足时还可提供多条反例.     

基于有限自动机的密码协议入侵检测方法*

提出了一种在密码协议运行中,基于有限自动机原理检测其上攻击的方法,详细介绍了该方法的工作原理,并通过实例验证了此方法的可行性,最后给出了该检测方法原型系统的测试结果.     

基于Web的自适应上报系统技术的研究与实现

分析了自适应上报系统的要求,提出了利用微软提供的OWC(office Web components)组件中的Spreadsheet控件实现基于B/S架构的自适应上报系统的解决方案.该解决方案通过后台用户对上报报表和表中需前台用户填写的内容进行设置,自动建立与上报报表相对应的数据表来保存数据,并可在此基础上由后台用户设定统计报表的格式与内容,完成数据的统计和汇总工作.此解决方案避免了因用户需求变更而导致二次开发的可能性,并为不同类型的上报系统提供了通用平台.     

热轧成品质量检测专家系统

针对传统专家系统的知识获取存在“瓶颈”以及传统热轧成品质量检测过程过于复杂的问题,提出了基于复二次函数的RBF神经网络和四组神经网络相结合的热轧成品质量检测专家系统.根据钢铁企业生产的特点,通过对四组神经网络的子判断结果进行综合判定得出输出结果.试验结果验证了该系统应用于热轧成品质量检测工作的便捷性及可行性,简化了传统质量检测过程的冗余步骤,提高了热轧质量检测工作的自动化程度.     

普通高等院校课时量统计系统的研究

为了弥补当今软件开发公司不能针对每个学校开发特定功能的缺憾,也为提高高校教师的工作效率和现如今倡导的高效的网上办公能力,山东万杰医学院组织开发"课时量统计系统"解决此问题,该系统使用Access2007和ASP.NET语言开发而成,整合教师课时上报、课时管理、课时查询、课时打印等模块,对教师课时量上报工作提供极大便利。     

实验室能力验证管理信息系统的设计与实现

实验室能力验证是对实验室检测能力和管理状况进行客观考核的一种方法。通过对实验室能力验证过程的分析研究,运用PHP技术,以MySQL为后台数据库,设计并实现了基于B/S模式的实验室能力验证管理信息系统。验证活动的组织者通过该系统发布验证计划,分配测试项目,管理测试数据,评定测试结果,接收测试反馈。该系统优化了繁杂的验证过程,提高了验证管理的信息化水平和工作效率,增强了实验室的自检和自控能力,有利于实验室的可持续发展。     

某型无人机导航/飞控系统设计与仿真

某型无人机以DSP为核心部件,介绍了其导航/飞控系统硬件设计、结构,其中主要包括数据采集、数据通信,介绍了导航/飞控软件,给出流程框图,设计了用于验证该系统的仿真系统;仿真系统引入大气模拟系统和GPS模拟系统,介绍大气模拟系统结构原理和GPS工作原理,仿真各子系统之间采用CAN总线进行连接,并且挂载真实舵机,检测舵机偏转检测,形成负反馈;最后,给出系统仿真步骤和仿真内容,得出仿真结果,验证该系统可行、正确.     

基于SAT的软件验证

线性时态逻辑SE-LTL是具有高表达力和基于状态、事件推理能力的并发系统规约语言.目前,SE-LTL的模型检测算法依然是显式的,状态空间爆炸是检测的主要困难.对SE-LTL引入一种有界模型检测技术,该技术将SE-LTL模型检测归约为命题公式的可满足性问题,避免了基于二叉图方法中状态空间的快速增长,加速了验证过程.对SE-LTL-X进一步在该技术中集成stuttering等价技术.实验结果表明该集成有效地降低了验证时间.     

基于ACE并发编程模式的告警关联系统设计与实现

对告警进行关联处理,减少冗余告警,增强告警的故障检测能力,是网络管理系统需要解决的关键问题.本文充分考虑电信运营网络管理可能出现的各种关联情况,定义了告警关联规则,运用ACE(Adapter Communication Environment,自适配通信环境)的ACE_task组件设计并实现了告警关联系统.实验表明,该系统能有效剔除冗余告警,及时上报故障,方便客户定位故障.     

传感器在汽车双燃料电控系统中的应用

介绍了一种步进电机驱动的位移检测系统的设计思想,阐述了它的工作原理、机械结构,提出了用于位移检测的差动电感式位移传感器具体的设计方案。经实验分析验证:该位移传感器在工作范围±2mm内线性度可达到0. 5%。该系统成本低,工作性能可靠。     

Billiard Combat Modeling and Simulation Based on Optimal Cue Placement Control and Strategic Planning

The selection of a best sequential shots for a given start cue position is a major challenging task in a billiard game. A new algorithm is proposed as a strategy to apply maximum tolerance angle search sequentially. The strategy considers combinations among all pockets and target object balls during both the pre and post collision shots selection processes. A simulation program is developed to test the strategy in a competition scenario by players with different proficiencies. The level of proficiency of players in the competition is controlled by a threshold value as a criterion to evaluate capability to conduct consecutive shots and when to give out right of play. The winning score of each game (win rate) is used as a performance comparison index among different gaming situations and to verify the effectiveness of the algorithm. The initial results of several simulation games using our strategy show that higher proficiency player can out beat lower proficiency player easily. This is consistent with the gaming situation in the real world, showing the consistency of our simulation program. The simulation also verifies that the play order does decide the final competition outcomes, when the players?? proficiencies are close to each other. This work is the first to investigate the effects of consecutive shots and order of play on the billiard gaming results. A low cost training system is proposed to verify the efficiency of the repositioning algorithm in real world settings. The system adapts an augmented reality technology to instruct users for reliable aiming assistance. It makes use of a vision system for cue ball, object ball locations and cue stick velocity tracking. In all, the simulation program can provide an initial proof of the effectiveness of the reposition algorithm in the competition situation. Experiments results of maximum tolerance angle all pocket search strategy using our training facility as tested by users with different skill levels all out performed the results without guidance for the set of users with the same proficiency.     

Application of neural networks and genetic algorithms to the screening for high quality chips

During electrical testing, each die on a wafer must be tested to determine whether it functions as originally designed. For a clustered defect on a wafer, for example scratches, stains, or localized failure patterns, defective dies in the flawed area may not all be detected during the electrical testing stage. To prevent the defective dies from proceeding to the final assembly, the testing factory must assign some workers to identify patterns in the layout of defective dies for labeling other potential defects. Although a previously developed defect detection program enables full automation of the testing process in a testing factory, numerous defective dies in recognized clusters are not picked out, or in some clusters are even not captured in certain circumstances. This work thus proposes two automatic wafer-scale defect cluster identifiers, which utilize neural networks and genetic algorithms for detecting the defect clusters, and compares them with that presented in our earlier work. The experimental results confirm that both of the proposed algorithms are more effective in identifying defect clusters than the defect detection program presently used by the testing factory.     

基于系统调用的异常入侵检测

监视程序行为是近年基于主机的异常入侵检测的研究热点,构建程序行为模型是进行异常检测的关键。该文根据构建程序行为模型时,从系统调用抽取的信息和异常检测中使用的系统调用序列的粒度以及异常检测器记录的信息,分析和比较了基于程序行为的异常检测技术,并对该项研究作了展望。     

基于VB6.0的函数信号发生器自动检定/校准系统的开发

详细介绍了基于VB6.0的函数信号发生器自动检定/校准测试系统的组成及工作原理、测控软件的开发设计、测控程序主要功能的实施。重点介绍了测控软件的编程语言设计、测控软件构成、测控软件主要功能模块、测控模块程序流程图。其开发过程不仅适用于函数信号发生器自动检定/校准系统的开发,还可适用于其他专业的自动测试系统的开发。     

Detection of weak unstable predicates in distributed programs

This paper discusses detection of global predicates in a distributed program. Earlier algorithms for detection of global predicates proposed by Chandy and Lamport (1985) work only for stable predicates. A predicate is stable if it does not turn false once it becomes true. Our algorithms detect even unstable predicates, without excessive overhead. In the past, such predicates have been regarded as too difficult to detect. The predicates are specified by using a logic described formally in this paper. We discuss detection of weak conjunctive predicates that are formed by conjunction of predicates local to processes in the system. Our detection methods will detect whether such a predicate is true for any interleaving of events in the system, regardless of whether the predicate is stable. Also, any predicate that can be reduced to a set of weak conjunctive predicates is detectable. This class of predicates captures many global predicates that are of interest to a programmer. The message complexity of our algorithm is bounded by the number of messages used by the program. The main applications of our results are in debugging and testing of distributed programs. Our algorithms have been incorporated in a distributed debugger that runs on a network of Sun workstations in UNIX     

The longitudinal impact of enterprise system users’ pre-adoption expectations and organizational support on post-adoption proficient usage

Although enterprise systems (ES) are ubiquitous, many firms report less than stellar payoffs from these costly investments, with underutilization often attributed to failures in the implementation process. Unfortunately, research has not provided sufficient insights into these failures, in part because it has focused on actual usage, as opposed to proficient usage, as the benchmark for successful implementation. Moreover, research has not generally examined how the adoption process unfolds over time, thus overlooking potential underlying mechanisms that may help explain how adopters achieve proficiency. To begin addressing these shortcomings, we study how adopters’ pre-adoption expectations, enacted over time, can influence their post-adoption proficiency, by shaping how and why they spend time using the system during the adoption period. We analyzed time-lagged survey data from 153 financial analysts, required to adopt new ES-based software, at a multinational bank. We found that adopters who hold pre-adoption expectations reflecting greater internal and external motives to adopt the system as well as systematically integrate it into their work routines are more apt to use the system in ways that enhance their cumulative knowledge of it, and subsequently develop higher levels of proficiency post-adoption. Moreover, greater organizational support enhanced the impact of adopters’ expectations on proficiency, except when their actual use is low in which case organizational support had an adverse effect.     

油田产能建设项目后评价辅助系统设计与实现

以油田企业产能建设项目的决策、管理水平和投资效益为目标,在详细分析油田产能建设项目后评价工作内容、工作程序的基础上,提出建立以计算机技术支持的油田产能建设项目后评价系统。阐述了系统的结构设计及实现方法,包括数据库设计、软件模型建立和图形统计报表输出等。研究和开发了以满足项目管理及工程技术人员决策需求的智能系统。此系统的运用使油田企业更为客观地对产能建设项目进行排队和分类,使产能建设项目投资决策更加科学化。     

基于FPGA测试电路的SRAM自测试研究

SRAM是微机系统中的记忆设备,用来存放程序和数据。因此对SRAM的自测试可以有效地避免存储器工作不正常给系统带来的损害。采用硬件描述语言对FPGA电路进行编程,构造SRAM测试电路。以对各种存储器常见故障模型能够有效检测的March C-算法为主要测试算法,对存储器单元进行故障测试,并将有错误的地址单元映射到备用的存储单元,以确保微机系统稳定运行。     

基于FX的MPS上料检测站控制系统程序设计

MPS系统是模拟实际工业生产中复杂控制过程的教学实训装置.该装置采用德国先进技术,集电气技术、PLC编程、传感器、气动等技术为一体,解决了学生不能在实际生产线上操作训练的问题.多数教学装置厂家给出的各站参考程序均通过辅助继电器编程,程序步数多,程序结构繁杂,不利于学生理解掌握.基于此给出了上料检测站的顺序结构程序设计方...     

基于FFT算法的高炉鼓风运行状态检测

对于钢铁制造企业来说,高炉风机的状态检测十分重要.设计了一个基于FFT和特征值检测的实时应用程序,用于生产过程数据的分析.模拟试验表明,该程序能够有效及早地发现系统故障.