An Automated Approach for the Interpretation of Counter-Examples

Model checking is an automatic technique used for the verification of finite systems. A model checker explores the full state space of a given model and checks it against a set of requirements. If a state exists in which a requirement is not satisfied most tools will generate a counter-example. Counter-examples are useful for debugging a model and determining if an error exists in the modelled system. However, they can be difficult for end users to understand and this may limit the take-up of model checking in industry.This paper describes a domain-specific approach to automatically interpreting counter-examples and presenting the results in an intuitive form to the end user. Our research extends previous work on model checking railway signalling control tables with signalling engineers from Queensland Rail.     

一种基于属性的自动信任协商方法

提出一种基于属性的信任协商方法。协商的双方首先交换包含多个加密属性的信任证书,然后双方根据自己的访问控制策略多次交换密钥逐步向对方显示出自己的属性。在这种协商方法中,双方可以控制自己的信任书中属性值的出示,且该协商方法使用椭圆曲线密钥交换算法产生会话密钥,计算量比较小。     

一种自动化软件设计改进方法

面向对象的软件设计改进是增强系统的可扩展性、使之适应可能的需求变化的一种有效手段.提出一种基于CBR(case based reasoning)和微体系结构反模式的设计改进方法.该方法形式化地定义了在微体系结构层中不灵活的设计结构和相应的重构方案的描述方法,研究了它们在事例库中的组织和索引机制.根据基于事例的推理技术的4R过程,提出了类图、顺序图、质量要素和语义约束的相似性度量方法,描述了在给定设计中识别反模式及其实例,并在此基础上,用高质量的设计方案进行替代的几种算法.以该方法为依据,进一步介绍了设计改进支撑系统--CBDIT(CBR based design improving tool)的体系结构的设计.     

SWITCH Technology: An Automated Approach to Developing Software for Reactive Systems

A technology for developing software for reactive systems is proposed that supports the stages of the subject domain investigation, analysis, design, implementation, debugging, certification, and documenting. The technology is based on the automaton approach.     

面向RISC-V内存一致性测试的自动化分析方法

开源架构RISC-V定义了其内存一致性模型RVWMO,作为多核RISC-V系统软硬件设计开发的重要规范。在多核芯片的验证阶段,需要对芯片的内存一致性进行严格全面的测试。测试通常针对某一访存顺序模式,选取典型的并行程序片段进行大规模测试（又称Litmus测试）,通过程序运行的最终状态推测芯片内存一致性模型。通常,更为宽松的内存一致性会导致更多的程序状态。分析Litmus测试结果对于验证芯片的RVWMO兼容性、探索多核系统的内存一致性优化的可能性具有重要意义。以RVWMO规范下允许的程序状态为基准,芯片实测得到更多的程序状态表明其存在兼容性问题,得到更少的程序状态表明其仍具有优化空间。面对规模庞大、行为复杂的Litmus测试,如何对其测试结果进行自动化分析是亟待解决的问题。本文对Litmus测试的原理和输出结果进行了深入分析,提出一种面向RISC-V内存一致性测试的自动化分析方法,采用形式化方法对Litmus测试进行基于RVWMO规范的模拟运行,并通过与芯片的实测结果进行对比分析给出测试结论。本方法基于Hifive Unmatched开发板开展测试。实验表明,本文提出的方法可快速、有效地对RISC-V内存一致性测试进行自动化分析。     

文本自动分类中特征权重算法的改进研究

文章研究并改进了文本自动分类中的特征权重算法。传统的特征权重算法着重于考虑频率和反文档频率等因素,而未考虑特征的类间、类内分布与低频高权信息。该文重点研究了特征的类间、类内分布,以及低频高权特征对分类的影响,并在此基础上提出了低频高权特征集的构造方法及特征权重的新算法,同时将该算法推广到多层次分类体系。实验证明该算法能有效提高分类的精确度,而且在多级分类中也能取得很好的效果。     

一种基于双向选择的多Agent系统自动集成方案

多Agent系统集成方案的选择能极大程度地影响多Agent系统的性能。目前大多数的多Agent系统集成方案只关注于系统级的行为与性能。本文在关注多Agent系统性能的同时,也关注各个Agent的收益。本文提出一种基于双向选择的多Agent系统集成方案,在此方案中,Agent根据自身的意愿选择合适的角色进行申请,同时角色根据对各个Agent的信任值选择合适的Agent来承担其任务。实验表明,随着若干次系统学习,多Agent系统协作任务完成时间能较快地下降,Agent在单位时间内的收益逐步提高。     

Tracing DDoS Floods: An Automated Approach

We propose a Controller-Agent model that would greatly minimize distributed denial-of-service (DDoS) attacks on the Internet. We introduce a new packet marking technique and agent design that enables us to identify the approximate source of attack (nearest router) with a single packet even in the case of attacks with spoofed source addresses. Our model is invoked only during attack times, and is able to process the victims traffic separately without disturbing other traffic, it is also able to establish different attack signatures for different attacking sources and can prevent the attack traffic at the nearest router to the attacking system. It is simple in its implementation, it has fast response for any changes in attack traffic pattern, and can be incrementally deployed. Hence we believe that the model proposed in this paper seems to be a promising approach to prevent distributed denial-of-service attacks.     

基于语义Web服务的供应链自动采购技术

将语义Web服务技术应用到企业间业务的自动集成中,设计实现了自动采购原型系统.通过使用服务发现、匹配以及自动调用技术来实现企业间订单的交互、选择以及自动生成.基于汽车制造业供应链背景,给出了原型系统及关键组件的设计和实现细节.     

An Ontology-Based Approach to Personalized Situation-Aware Mobile Service Supply

Mobile devices such as personal digital assistants (PDAs) and mobile phones are in widespread use already today and converging to mobile smart phones. They enable users to access a wide range of services and information without guidance through their actual demands. Especially during mass events like the Olympic Games 2008 in Beijing—which was initially the context of our work—a large service space is expected to support all mobile visitors, being athletes, journalists, or spectators. Current approaches tackling such problems are location based, meaning that a user's location is central to service provision, and even context-aware, meaning that, beyond location, characteristics of a user's environment are taken into account. Such information obviously helps to deliver relevant information at the right time to the mobile users. Going one step further, a situation-aware system abstracts from the context dimensions by translating specific contexts into logical situations. Knowing the situation end users are in allows the system to better identify the information to be delivered to them and to choose the appropriate services with regard to their scope, which is referred to as service roaming. Even though many context frameworks have been introduced in the past few years, what is usually missing is the notion of characteristic features of contexts that are invariant during certain time intervals. This paper presents these concepts in the context of a platform development, namely FLAME2008, which is able to support its mobile users with personalized situation-aware services in push and pull mode.     

Automated Nucleic Acid Purification for Large Samples

Advancements in the fields of genomic screening, molecular pathology and clinical research have resulted in a major increase in the demand for high quality DNA and RNA. This escalating demand has resulted in a sample preparation bottleneck and an emphasis on the development of new technologies to automate the purification process. Gentra has developed the AUTOPURE LS™ nucleic acid purification instrument, a platform capable of high-throughput sample purification from large samples, such as 10 mL whole blood. This article presents data showing the equivalency of DNA purified using manual and automated processing.     

基于对象请求代理的程序自动开发方法与工具

随着分布式对象技术的日益流行,越来越多的应用程序开始采用基于对象请求代理(object request broker,简称ORB)进行开发.从开发人员角度看,目前这类应用程序在开发过程上仍存在一些不足之处,例如,需要掌握的基本概念较多,ORB产品之间的兼容性不足等.在深入分析了这些问题后,提出了一种改进开发过程的方法,通过代码自动生成,分离特定于ORB产品的代码等技术,尽可能提供对其中开发活动的自动支持.实验结果表明,实现上述方法的支撑工具原型系统可以有效地减少代码编写量,并降低编码出错的概率.     

设计特征模型到分析特征模型的自动转换方法

针对有限元分析建模的需求,提出一种将工程零件的设计特征模型自动转换为相应的分析特征模型的方法.首先将设计特征模型分解为所有正特征剩余体的集合,然后从各正特征剩余体中分解出一组扫成体和非扫成体,再采用基于二维轮廓的方法从各扫成体中确定出候选分析特征区域,最后通过合成候选分析特征区域得到真正的分析特征区域,并在此基础上生成分析特征和分析特征模型.实验结果表明该方法是有效的.     

An Automated Signature-Based Approach against Polymorphic Internet Worms

Capable of infecting hundreds of thousands of hosts, worms represent a major threat to the Internet. However, the defense against them is still an open problem. This paper attempts to answer an important question: How can we distinguish polymorphic worms from normal background traffic? We propose a new worm signature, called the position-aware distribution signature (PADS), which fills the gap between traditional signatures and anomaly-based intrusion detection systems. The new signature is a collection of position-aware byte frequency distributions. It is more flexible than the traditional signatures of fixed strings while it is more precise than the position-unaware statistical signatures. We propose two algorithms based on expectation-maximization (EM) and Gibbs sampling to efficiently compute PADS from a set of polymorphic worm samples. We also discuss how to separate a mixture of different polymorphic worms such that their respective PADS signatures can be calculated. We perform extensive experiments to demonstrate the effectiveness of PADS in separating new worm variants from normal background traffic.     

一种基于Messy GA的结构测试数据自动生成方法

结构性测试是标识测试用例的基本方法之一.由于程序语言的复杂性以及被测程序的多样性,自动生成结构测试数据的一种有效方法是根据程序运行结果指导生成过程,通过不断迭代,生成符合要求的测试数据集.提出一种基于Messy GA的结构测试数据自动生成方法,将测试覆盖率表示为测试输入集X的函数F(X),并利用Messy GA不需要染色体模式排列的先验知识即可进行优化求解的性质对F(X)进行迭代寻优,进一步提高了搜索的并行性,并最终提高测试覆盖率.对一组标准测试程序和若干实际应用程序的实验结果表明,较之现有基于遗传算法的生成方法,该方法能够以更高的效率生成更高质量的测试数据,并适用于较大规模的程序.     

Requirements and GitHub Issues: An Automated Approach for Quality Requirements Classification

Programming and Computer Software - In the development of quality software, critical decisions related to planning, estimating, and managing resources are bound to the correct and timely...