检索结果-内蒙古大学图书馆

Model checking CTL based on complete abstraction interpretation

Jisuanji Xuebao/Chinese Journal of computers 2009年第5期32卷 992-1001页

作者： Qian, Jun-Yan Xu, Bao-Wen School of Computer and Control Guilin University of Electronic Technology Guilin 541004 China State Key Laboratory for Novel Software Technology Nanjing University Nanjing 210093 China Department of Computer Science and Technology Nanjing University Nanjing 210093 China

Abstraction plays a fundamental role in combating state-space explosion in model checking. In a complete abstract interpretation-based view, the authors reduce the state space of a Kripke structure in order to obtain a minimal abstract state translation system that strongly preserves a given temporal specification language CTL. According to a relation between completeness of abstract interpretations and strong preservation of abstract model checking, the problem of minimally refining abstract model in order to make it strongly preserving CTL can be formulated as a minimal abstract domain refinement in abstraction interpretation in order to get completeness, and this refined complete abstract domain always exists. Given initial abstract domain, we can obtain a minimal abstract domain which is complete for the standard operators of CTL by the iterative computation of the fixpoint. Moreover, the corresponding partition is the coarsest partition which is strong preserving for CTL. The authors show that the abstract domain is complete for the standard operators of CTL iff it is complete for complement and standard predecessor transformer operators.

关键词： Model checking

来源：评论

学校读者我要写书评

暂无评论

A Security Calculus of Concurrent Objects for Verifying Ad Hoc Network Protocols

A Security Calculus of Concurrent Objects for Verifying Ad H...

引用

International Conference on Network and System Security, NSS

作者： Qin Li Qingkai Zeng School of Computer Science Anhui University of Science and Technology China State Key Laboratory of Novel Software Technology Department of Computer Science and Technology Nanjing University China

We present a calculus of concurrent objects for specification and security analysis of ad hoc security protocols. The communicating nodes and the network are modeled by objects, while the interactions between them are modeled by asynchronous method invocations. The internal state of an object is represented by a constant method which can be overridden. The approach is complemented by a control flow analysis which can be used to automatically check properties such as security routing. The attacker model is integrated into the analysis as set values containing the knowledge of the attacker.

关键词： Calculus Ad hoc networks Routing protocols computer security Object oriented modeling computer science Telephony Automatic control Authentication Internet

来源：评论

学校读者我要写书评

暂无评论

Improvements on Teaching Methods and Contents for the "computer Organization and Architecture" Curriculum

Improvements on Teaching Methods and Contents for the "Compu...

引用

International Conference on Scalable Computing and Communications;International Conference on Embedded Computing, SCALCOM-EMBEDDEDCOM

作者： Chunfeng Yuan Yihua Huang Zhesheng Zhang Guihai Chen Wanchun Dou Department of Computer Science and Technology State Key Laboratory for Novel Software Technology Nanjing University Nanjing Jiangsu China

"computer Organization and Architecture" is one of the most important fundamental courses for those majoring in computer science and engineering. The contents of the curriculum are crucial for entire computer discipline and computer systems. As a result, the curriculum plays an important role in training computer science students. This paper begins with the discussion on principles and goals of the curriculum. Then, it describes teaching philosophy and methods, improvements of contents, along with their effects, for lectures and experiments of the curriculum. Finally we review some experiences from the development and teaching of the curriculum. This paper intends to share experiences in teaching the curriculum with other institutes in China and provide them with a potentially useful instructional model.

关键词： Education computer architecture Hardware Embedded computing computer science Operating systems computer interfaces Embedded software Program processors Instruction sets

来源：评论

学校读者我要写书评

暂无评论

Design pattern directed clustering for understanding open source code

Design pattern directed clustering for understanding open so...

引用

IEEE Workshop on Program Comprehension

作者： Zhixiong Han Linzhang Wang Liqian Yu Xin Chen Jianhua Zhao Xuandong Li State Key Laboratory of Novel Software Technology Department of Computer Science and Technology Nanjing University Nanjing Jiangsu China

Program understanding plays an important role in the maintenance and reuse of open source code. Rapid evolving and bad documentation makes the understanding and reusing difficult. Design patterns are widely employed in the open source code. In this paper, we propose a design pattern directed clustering approach to help understand the structure of open source code. According to the approach, we have implemented a prototype tool. We also conducted an experiment on an open source system to evaluate it.

关键词： Detectors Engines Visualization Open source software Documentation Prototypes Laboratories software maintenance computer science software prototyping

来源：评论

学校读者我要写书评

暂无评论

Building Prioritized Pairwise Interaction Test Suites with Ant Colony Optimization

Building Prioritized Pairwise Interaction Test Suites with A...

引用

International Conference on Quality software

作者： Xiang Chen Qing Gu Xin Zhang Daoxu Chen State Key Laboratory for Novel Software Technology Department of Computer Science and Technology Nanjing University Nanjing Jiangsu China

ISBN: (纸本)9781424459124

Interaction testing offers a stable cost-benefit ratio in identifying faults. But in many testing scenarios, the entire test suite cannot be fully executed due to limited time or cost. In these situations, it is essential to take the importance of interactions into account and prioritize these tests. To tackle this issue, the biased covering array is proposed and the Weighted Density Algorithm (WDA) is developed. To find a better solution, in this paper we adopt ant colony optimization (ACO) to build this prioritized pairwise interaction test suite (PITS). In our research, we propose four concrete test generation algorithms based on Ant System, Ant System with Elitist, Ant Colony System and Max-Min Ant System respectively. We also implement these algorithms and apply them to two typical inputs and report experimental results. The results show the effectiveness of these algorithms.

关键词： Ant colony optimization software testing software quality Concrete System testing Partitioning algorithms Laboratories computer science Fault diagnosis Costs

来源：评论

学校读者我要写书评

暂无评论

A Decentralized Storage Scheme for Multi-Dimensional Range Queries over Sensor Networks

A Decentralized Storage Scheme for Multi-Dimensional Range Q...

引用

International Conference on Parallel and Distributed Systems (ICPADS)

作者： Lei Xie Lijun Chen Daoxu Chen Li Xie State Key Laboratory of Novel Software Technology Department of Computer Science Nanjing University Nanjing China

This paper presents the design of a decentralized storage scheme to support multi-dimensional range queries over sensor networks. We build a distributed k-d tree based index structure over sensor network, so as to efficiently map high dimensional event data to a two-dimensional space of sensors while preserving the proximity of events. We propose a dynamic programming based methodology to control the granularity of the index tree in an optimized approach, and an optimized routing scheme for range query processing to achieve best energy efficiency. The simulation results demonstrate the efficiency of the design.

关键词： Query processing Sensor phenomena and characterization Routing Distributed control Sensor systems Optimization methods Temperature sensors Laboratories Paper technology computer science

来源：评论

学校读者我要写书评

暂无评论

Sketch-based method for interactive hairstyling

引用

Ruan Jian Xue Bao/Journal of software 2009年第SUPPL. 1期20卷 202-212页

作者： Wang, Bin Sun, Zheng-Xing Zhang, Yan State Key Laboratory for Novel Software Technology Nanjing University Nanjing 210093 China Department of Computer Science and Technology Nanjing University Nanjing 210093 China

To support hairstyling effectively, it's crucial for hairstyling tools to find a tradeoff between realism and interaction. This paper presents an interactive hairstyling method which can handle both global and local details of the hairstyle. Vector field based hairstyling method is used to generate the global shape of the hairstyle. This paper defines three different kinds of hairstyle curves which indicate the boundary constraints of vector field so that the user can control the hairstyle generation interactively. Hair wisp model is also used to represent hairstyles and several wisp based editing operations are defined, such that users can control the local details of the hairstyle. Experimental results prove that the proposed method provides more interaction and computation efficiencies without lost of hair realism. © by Institute of software, the Chinese Academy of sciences. All rights reserved.

关键词： computer software

来源：评论

学校读者我要写书评

暂无评论

Principles for Energy-Efficient Topology Control in Wireless Sensor Networks

Principles for Energy-Efficient Topology Control in Wireless...

引用

International Conference on Wireless Communications, Networking and Mobile Computing (WiCom)

作者： Xue Zhang Xuyang Ding Sanglu Lu Guihai Chen School of Computer Science and Engineering University of Electronic Science and Technology Chengdu China State Key Laboratory of Novel Software Technology Department of Computer Science and Technology Nanjing University Nanjing China

Topology control is one of the most important energy-saving techniques used in wireless sensor networks. It has evolved into two dominant research directions: power control and sleep scheduling. Although many topology control algorithms and protocols are claimed to be highly energy-efficient, this is not necessarily the case in real systems due to various isolated considerations. In this paper, based on a simple and comprehensive analysis of energy consumption, we propose three necessary principles for energy-efficient topology control for wireless sensor networks. Topology control should (1) consider power control and sleep scheduling jointly, (2) be aware of traffic load, and (3) be done in conjunction with routing. We wish this paper could contribute to the development of the research on topology control for wireless sensor networks.

关键词： Energy efficiency Network topology Wireless sensor networks Power control Sleep Control systems Protocols Energy consumption Telecommunication traffic Routing

来源：评论

学校读者我要写书评

暂无评论

When does co-training work in real data?

When does co-training work in real data?

引用

13th Pacific-Asia Conference on Knowledge Discovery and Data Mining, PAKDD 2009

作者： Ling, Charles X. Du, Jun D. Zhou, Zhi-Hua Department of Computer Science The University of Western Ontario London ON N6A 5B7 Canada National Key Laboratory for Novel Software Technology Nanjing University Nanjing 210093 China

ISBN: (纸本)3642013066

Co-training, a paradigm of semi-supervised learning, may alleviate effectively the data scarcity problem (i.e., the lack of labeled examples) in supervised learning. The standard two-view co-training requires the dataset be described by two views of attributes, and previous theoretical studies proved that if the two views satisfy the sufficiency and independence assumptions, co-training is guaranteed to work ***, little work has been done on how these assumptions can be empirically verified given datasets. In this paper, we first propose novel approaches to verify empirically the two assumptions of co-training based on datasets. We then propose simple heuristic to split a single view of attributes into two views, and discover regularity on the sufficiency and independence thresholds for the standard two-view co-training to work well. Our empirical results not only coincide well with the previous theoretical findings, but also provide a practical guideline to decide when co-training should work well based on datasets. © Springer-Verlag Berlin Heidelberg 2009.

关键词： Supervised learning

来源：评论

学校读者我要写书评

暂无评论

SNN - A Neural Network Based Combination of software Reliability Growth Models

SNN - A Neural Network Based Combination of Software Reliabi...

引用

International Conference on Information science and Engineering (ICISE)

作者： Ang Li Qing Gu Guang-Cheng Feng Dao-Xu Chen State Key Laboratory for Novel Software Technology Department of Computer Science and Technology Nanjing University Nanjing China School of Computer Science and Engineering University of Aizu Japan

ISBN: (纸本)9781424449095

Applying SRGMs (software Reliability Growth Models) to real projects is a major concern in software reliability. Sometimes, it is hard to decide the best model for a specific project. Researchers have made a first step on solving this problem by combination, but the effect was limited in accuracy and adaptability. Aiming to improve the usability of the SRGMs, we propose a neural network based combination method to build accurate and adaptive SNN (Selective Neural Network) model. It avoids relying on a single model, thus reduces the risk to produce inaccurate predictions and improves the average performance in accuracy. Neural network and multi-criteria model selection strategy enable the SNN model to be adapted to various projects, producing accurate predictions. Experiment results show that the SNN model makes a notable improvement in accuracy compared with its component models and other combinational models do.

关键词： Neural networks software reliability Predictive models Reliability engineering computer science Usability Mathematical model Information science Laboratories software performance

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：