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

state/Action-based Fairness Verification for Non-determinism

电子学报(英文版) 2011年第4期20卷 603-606页

作者： XU Guangquan PANG Shanchen GAO Honghao XIAO Yingyuan LI Xiaohong FENG Zhiyong School of Computer Science and Technology Tianjin University Tianjin China Department of Computer Science and Technology Tsinghua University Beijing China College of Information Science and Engineering Shandong University of Science and Technology Qingdao China School of Computer Engineering and Science Shanghai University Shanghai China Tianjin Key Laboratory of Intelligence Computing and Novel Software Technology Tianjin University of Technology Tianjin China

Most of the existing work about fairness verification was carried out by checking the fairness based on state, action, or process respectively. It is hard to resolve the fairness issue for complex software systems, especially in life-critical systems and safety-critical systems. In this paper, we verify the fairness based on both state and action, which is realized mainly by introducing an extended Kripke structure and four kinds of fairness (weak global/local fairness and strong global/local fairness). The experimental results show the superiority of our method by the savings in memory (2.08%) and time consumption (26.45%).

关键词：非确定性基础验证 Kripke结构安全关键系统软件系统公正性消费量

来源：评论

学校读者我要写书评

暂无评论

Integrated Approach to Hypersonic Vehicle Modeling

Integrated Approach to Hypersonic Vehicle Modeling

引用

Chinese Control Conference

作者： Xiaofeng Su Yingmin Jia Junping Du Fashan Yu The Seventh Research Division and the Department of Systems and Control Beihang University (BUAA) Key Laboratory of Mathematics Informatics and Behavioral Semantics (LMIB) Ministry of Education SMSS Beihang University (BUAA) Beijing Key Laboratory of Intelligent Telecommunications Software and Multimedia School of Computer Science and Technology Beijing University of Posts and Telecommunications School of Electrical Engineering and Automation Henan Polytechnic University

ISBN: (纸本)9781467325813

This paper is devoted to the modeling problem of hypersonic vehicle with significant couplings. An integrated approach is developed to analytically model the dynamics of hypersonic vehicle, in which the effects of variable mass, spherical rotating earth, and couplings among the sub-models are considered. Furthermore, a preliminary analysis is conducted using the general data of a hypersonic vehicle. The simulation results show that the maximum of the Coriolis force can reach values up to 7.02% of the vehicle weight, and that the thermal load determined by the nonuniform aerodynamic heating and the properties of the structure has a significant influence on the elastic deformation.

关键词： Hypersonic vehicle modeling Inertial dynamics Aerodynamics Elasticity Heating hypersonic vehicles Aerodynamics elasticity Coriolis force Vehicle weight Heating Couplings Thermal loading elastic deformation

来源：评论

学校读者我要写书评

暂无评论

Learning-based automatic breast tumor detection and segmentation in ultrasound images

Learning-based automatic breast tumor detection and segmenta...

引用

IEEE International Symposium on Biomedical Imaging

作者： Peng Jiang Jingliang Peng Guoquan Zhang Erkang Cheng Vasileios Megalooikonomou Haibin Ling School of Computer Science and Technology Shandong Provincial Key Laboratory of Software Engineering P.R.China Department of Ultrasound Shandong Provincial Hospital Affiliated to Shandong University P.R. China Center for Data Analytics & Biomedical Informatics Temple University Philadelphia PA USA

ISBN: (纸本)9781457718571

Ultrasound (US) images have been widely used in the diagnosis of breast cancer in particular. While experienced doctors may locate the tumor regions in a US image manually, it is highly desirable to develop algorithms that automatically detect the tumor regions in order to assist medical diagnosis. In this paper, we propose a novel algorithm for automatic detection of breast tumors in US images. We formulate the tumor detection as a two step learning problem: tumor localization by bounding box and exact boundary delineation. Specifically, the proposed method uses an AdaBoost classifier on Harr-like features to detect a preliminary set of tumor regions. The preliminarily detected tumor regions are further screened with a support vector machine using quantized intensity features. Finally, the random walk segmentation algorithm is performed on the US image to retrieve the boundary of each detected tumor region. The proposed method has been evaluated on a data set containing 112 breast US images, including histologically confirmed 80 diseased ones and 32 normal ones. The data set contains one image from each patient and the patients are from 31 to 75 years old. Experiments demonstrate that the proposed algorithm can automatically detect breast tumors, with their locations and boundary shapes retrieved with high accuracy.

关键词： Image segmentation Support vector machines Breast tumors Ultrasonic imaging Feature extraction Accuracy

来源：评论

学校读者我要写书评

暂无评论

Artemis-FollowMe: An agent-based middleware for mobile context-aware applications

Artemis-FollowMe: An agent-based middleware for mobile conte...

引用

2011 6th International Conference on Pervasive Computing and Applications, ICPCA 2011

作者： Ma, Jun Wang, Liang Xu, Jingwei Tao, Xianping Lu, Jian State Key Laboratory for Novel Software Technology Department of Computer Science and Technology Nanjing University NO.22 Hankou Road Nanjing 210093 China

ISBN: (纸本)9781457702082

Context Awareness and Mobility are two fundamental characteristics of ubiquitous and pervasive computing, where users may wander among smart spaces equipped with kinds of devices providing types of services with respects to the changing contexts of the users, the environments and the services themselves. Generally, an underlying infrastructure or middleware is needed to support such mobile context aware applications. Inspired by the inherent autonomy and mobility of software agents, in this paper we propose a middleware named Artemis-FollowMe, which utilizes mobile agents as basic components both for handling contexts and building applications. Especially, we focus on how the mobile capability of agents could be used to enable distributed and efficient management of contexts. We also have built a prototype and conducted many experiments to show how and how well our FollowMe works. © 2011 IEEE.

关键词： Mobile agents

来源：评论

学校读者我要写书评

暂无评论

Competent predicate abstraction in model checking

引用

science China(Information sciences) 2011年第2期54卷 258-267页

作者： LI Li1,2,3, SONG XiaoYu4, GU Ming2,3 & LUO XiangYu2,3 1department of computer science & technology, Tsinghua University, Beijing 100084, China 2key laboratory for Information System Security, Ministry of Education of China, Beijing 100084, China 3School of software, Tsinghua University, Beijing 100084, China 4department of ECE, Portland state University, Portland, Oregon 97207, USA Department of Computer Science & Technology Tsinghua University Beijing China Key Laboratory for Information System Security Ministry of Education of China Beijing China School of Software Tsinghua University Beijing China Department of ECE Portland State University Portland USA

The paper presents a new approach to computing the abstract state and a maximum weight heuristic method for finding the shortest counter-example in verification of imperative programs. The strategy is incorporated in a verification system based on the counterexample-guided abstraction refinement method. The proposed method slashes both the size of the abstract state space and the number of invokes of a decision procedure. A number of benchmarks are employed to evaluate the effectiveness of the approach.

关键词： program model checking predicate abstraction weight heuristic

来源：评论

学校读者我要写书评

暂无评论

JITDefender: A defense against JIT spraying attacks

JITDefender: A defense against JIT spraying attacks

引用

作者： Chen, Ping Fang, Yi Mao, Bing Xie, Li State Key Laboratory for Novel Software Technology Nanjing University Nanjing 210093 China Department of Computer Science and Technology Nanjing University Nanjing 210093 China

ISBN: (纸本)9783642214233

JIT spraying is a new code-reuse technique to attack virtual machines based on JIT (Just-in-time) compilation. It has proven to be capable of circumventing the defenses such as data execution prevention (DEP) and address space layout randomization(ASLR), which are effective for preventing the traditional code injection attacks. In this paper, we describe JITDefender, an enhancement of standard JIT-based VMs, which can prevent the attacker from executing arbitrary JIT compiled code on the VM. Thereby JITDefender can block JIT spraying attacks. We prove the effectiveness of JITDefender by demonstrating that it can successfully prevent existing JIT spraying exploits. JITDefender reports no false positives when run over benign actionscript/javascript programs. In addition, we show that the performance overhead of JITDefender is low. © 2011 IFIP International Federation for Information Processing.

关键词： Network security

来源：评论

学校读者我要写书评

暂无评论

UML interaction model-driven runtime verification of Java programs

UML interaction model-driven runtime verification of Java pr...

引用

作者： Li, X. Qiu, X. Wang, L. Chen, X. Zhou, Z. Yu, L. Zhao, J. State Key Laboratory of Novel Software Technology Nanjing University Nanjing Jiangsu China Department of Computer Science and Technology Nanjing University Nanjing Jiangsu China

The authors use unified modelling language (UML) 2.0 interaction overview diagrams (IODs) and sequence diagrams to construct simple and expressive scenario-based specifications, and present an approach to runtime verification of Java programs for exceptional consistency and mandatory consistency. The exceptional consistency requires that any forbidden scenario described by a given IOD never happens during the execution of a program, and the mandatory consistency requires that if a reference scenario described by a given sequence diagram occurs during the execution of a program, it must immediately adhere to a scenario described by a given IOD. In the approach, the authors first instrument a program under verification so as to gather the program execution traces related to a given scenario-based specification;then they drive the instrumented program to execute for generating the program execution traces;finally they check if the collected program execution traces satisfy the given specification. The approach leads to a supporting tool for testing in which UML interaction models are used as automatic test oracles to detect the wrong temporal ordering of message interaction in programs. © 2011 The Institution of Engineering and technology.

关键词： Unified Modeling Language

来源：评论

学校读者我要写书评

暂无评论

Stochastic H_2 Optimal Control of Discrete-Time Markov Jump Systems with Periodic Coefficients

Stochastic H_2 Optimal Control of Discrete-Time Markov Jump ...

引用

American Control Conference

作者： Hongji Ma Yingmin Jia Junping Du Fashan Yu Seventh Research Division and the Department of Systems and Control Beihang University (BUAA) Beijing 100191 China Beijing Key Laboratory of Intelligent Telecommunications Software and Multimedia School of Computer Science and Technology Beijing University of Posts and Telecommunications Beijing 100876 China School of Electrical Engineering and Automation Henan Polytechnic University Jiaozuo 454000 Henan China

ISBN: (纸本)9781457710957

In this paper, the H_2 optimal state-feedback control problem is investigated for discrete-time Markov jump systems subject to periodic coefficients and multiplicative noise. First of all, an exhaustive analysis is pursued to set up an H_2 performance criterion (H_2 norm), which can be characterized by the periodic solutions of two generalized Lyapunov equations. Based on the obtained H_2 norm, the H_2 optimal state-feedback controller is designed in terms of the stabilizing solution of a discrete-time generalized Riccati equation with periodic coefficients. Moreover, this stabilizing solution can be computed efficiently by the available iterative algorithm.

关键词： Markov processes Noise Educational institutions Riccati equations Optimal control

来源：评论

学校读者我要写书评

暂无评论

Tagging web product titles based on hidden Markov model 11

Tagging web product titles based on hidden Markov model

引用

Proceedings of the 2011 ACM Symposium on Applied Computing

作者： Wang, Peng Xu, Baowen You, Yue Chen, Lu School of Computer Science and Engineering Southeast University China State Key Laboratory for Novel Software Technology Nanjing University China Department of Computer Science and Technology Nanjing University China College of Software and Engineering Southeast University China

ISBN: (纸本)9781450301138

E-commerce web sites usually have to maintain a large number of product information. To organize this product information, a feasible way is to add semantic tags to the information. However, the Web product information often consists of many irregular statements published by users. Therefore, it is difficult to find rules to automatically tag the product information. This paper mainly focus on the problem of tagging Web product titles and proposes a tagging method based on the hidden markov model (HMM). This method first trains HMM with the maximum likelihood (ML) algorithm, then employs the Viterbi algorithm to tag product titles. Moreover, some strategies including smoothing process, background knowledge, extraction rules and simplifying HMM output observations are used for improving the quality of results. Experimental results on the real world dataset show that our method can achieve more than 51% precision and 60% recall. © 2011 Authors.

关键词： Hidden Markov models

来源：评论

学校读者我要写书评

暂无评论

An adaptive method for shader simplification

An adaptive method for shader simplification

引用

2011 International Conference on Virtual Reality and Visualization, ICVRV 2011

作者： Song, Xijun Tu, Changhe Xu, Yanning Department of Computer Science and Technology Shandong Provincial Key Laboratory of Software Engineering Shandong University Jinan China

ISBN: (纸本)9780769546025

Programmable shader is a powerful tool to describe objects' appearances in the realm of computer graphics. However, executing shaders takes up much time during rendering and can easily go beyond the computer hardware capability. We present a novel method to simplify both programmable shaders based on Render Man Shading Language and geometries for reducing rendering time with little quality loss. Given a level, we use progressive mesh to simplify geometries adaptively to obtain an appropriate representation, besides, shaders can also be automatically simplified by applying our simplification rules. To our knowledge, research on geometry level of detail often combines texture level of detail, whereas our approach is the first to implement the combination of geometry level of detail and shader level of detail. © 2011 IEEE.

关键词： computer hardware

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：