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

IEEE International Symposim on High Assurance Systems engineering

作者： Luyao Wang Fengwei Sui Yanhong Huang Huibiao Zhu Shanghai Key Laboratory of Trustworthy Computing Software Engineering Institute East China Normal University China East China Normal University Shanghai CN National Trusted Embedded Software Engineering Technology Research Center East China Normal University China

ISBN: (纸本)9781479981120

As a dynamic memory virtualization technique, ballooning is widely applied in many virtualization platforms, i.e. Xen and VMware ESX Server. Since ballooning technology enables the guest OS to surrender unused memory back to the host during runtime, and it can increase utilization and flexibility of memory. Despite the rapid development and extensive use of memory virtualization technologies, it is still a challenge to analyze and verify its validity and some major properties through formal methods. In this paper, we model the ballooning under Xen architecture including Xen hyper visor, a set of virtual machines and balloon drivers using the process algebra Communication Sequential Process (CSP) in order to verify some resource control properties of ballooning. The model is implemented with Process Analysis Toolkit (PAT). As a result, the ballooning used in Xen architecture satisfies these major resource control properties in VM requirement document.

关键词： Memory management Virtual machining Virtualization Virtual machine monitors Hardware Computational modeling

来源：评论

学校读者我要写书评

暂无评论

Characterizing Multi-media Retrieval Applications

Characterizing Multi-media Retrieval Applications

引用

International Conference on Parallel Processing (ICPP)

作者： Yunping Lu Xin Wang Weihua Zhang Yi Li Wenyun Zhao Shanghai Key Laboratory of Data Science Fudan University Shanghai China State Key Lab of Mathematical Engineering and Advanced Computing Wuxi China Software School Fudan University Shanghai China Parallel Processing Institute Fudan University Shanghai China

Multimedia data, especially image and video data, have become one of the most overwhelming data types on the Internet recently. Considering the user experience and real application requirements, multimedia data always demand a real-time processing speed. As a result, the huge amount of such data make retrieving useful information from them not only data-intensive, but also computation-intensive, which poses significant challenges to current system and architecture designs. Unfortunately, most prior studies focus only on text based retrieval systems or traditional multimedia processing applications. As far as we know, there is no systematic study on analyzing the characteristics of multimedia retrieval applications and how they might impact system and architecture designs. In this paper, we make the first attempt to construct a multimedia retrieval benchmark suite (called MMR Bench) to evaluate the corresponding system and architecture designs. To embody diverse multimedia retrieval applications, we collect eight state-of-the-art multimedia retrieval algorithms which cover the whole retrieval stages, including feature extraction, feature matching, and spatial verification. To satisfy diverse evaluation purposes, we implement multiple versions for each algorithm, including sequential version, pthread version for multi-core evaluation and data-parallel (i.e., Map-reduce) version for data-center evaluation. Moreover, MMR Bench provides flexible interfaces through retrieval stages, as well as a tool to adjust parameters and regenerating different scales of reasonable input. With such a flexible design, the algorithms in MMR Bench may be not only suitable for individual kernel-level evaluation, but also capable to be integrated into a complete infrastructure for system-level evaluation. Based on MMR Bench, we further analyze the inherent architectural characteristics, such as input size sensitivity and workload balance, which provides some insights into system and archite

关键词： Multimedia communication Feature extraction Benchmark testing Streaming media Algorithm design and analysis Computer architecture

来源：评论

学校读者我要写书评

暂无评论

Real-time and personalized search over a microblogging system

Real-time and personalized search over a microblogging syste...

引用

作者： Gao, Ming Jin, Cheqing Qian, Weining Gong, Xueqing Shanghai Key Laboratory of Trustworthy Computing Software Engineering Institute East China Normal University Shanghai 200062 China

As the microblogging systems such as Twitter and Sina Weibo become more and more popular in recent years, the requirement for real-time and personalized search over microblogging systems also becomes more important. In general, a user may expect a quick response that also satisfies her personalized requirements. Unfortunately, since there exist a huge number of users and massive updating microblogs in a microblogging system, personalized search on the system becomes a challenging task. In this paper, we design a new search engine containing four modules to infer the topics of microblogs and update the interests of users, build indexes efficiently, return microblogs for a keyword search, and personalize the order of microblogs, respectively. We also conduct a series of experiments on a real dataset to illustrate the effectiveness and efficiency of the proposed methods. © The British Computer Society 2013. All rights reserved.

关键词： Search engines

来源：评论

学校读者我要写书评

暂无评论

Prototype tool for supporting a formal engineering approach to service-based software modeling

Prototype tool for supporting a formal engineering approach ...

引用

3rd International Workshop on Structured Object-Oriented Formal Language and Method, SOFL+MSVL 2013

作者： Miao, Weikai Liu, Shaoying Shanghai Key Laboratory of Trustworthy Computing Software Engineering Institute East China Normal University Shanghai China Department of Computer Science Hosei University Tokyo Japan

ISBN: (纸本)9783319049144

Despite the advances in service-based software modeling, few existing approaches and tools support a systematic engineering process in which precise specification construction and accurate web service selection are integrated coherently. Due to this reality, how to carry out service-based software modeling so that existing services can be accurately discovered, selected, and effectively reused in the system under development is still a challenge. To solve this problem, this paper describes a prototype tool that supports a formal engineering framework for service-based software modeling. Formal specification can be constructed in an evolutionary manner;meanwhile, appropriate services are discovered and selected through the specification evolution. We illustrate the basic principle underlying the tool. The tool design and its implementation are also described. An example is presented to demonstrate major features of this tool. © 2014 Springer International Publishing Switzerland.

关键词： Formal specification

来源：评论

学校读者我要写书评

暂无评论

26th Annual Computational Neuroscience Meeting (CNS*2017): Part 3 Antwerp, Belgium. 15-20 July 2017 Abstracts

引用

BMC NEUROSCIENCE 2017年第SUPPL 1期18卷 95-176页

作者： [Anonymous] Department of Neuroscience Yale University New Haven CT 06520 USA Department Physiology & Pharmacology SUNY Downstate Brooklyn NY 11203 USA NYU School of Engineering 6 MetroTech Center Brooklyn NY 11201 USA Departament de Matemàtica Aplicada Universitat Politècnica de Catalunya Barcelona 08028 Spain Institut de Neurobiologie de la Méditerrannée (INMED) INSERM UMR901 Aix-Marseille Univ Marseille France Center of Neural Science New York University New York NY USA Aix-Marseille Univ INSERM INS Inst Neurosci Syst Marseille France Laboratoire de Physique Théorique et Modélisation CNRS UMR 8089 Université de Cergy-Pontoise 95300 Cergy-Pontoise Cedex France Department of Mathematics and Computer Science ENSAT Abdelmalek Essaadi’s University Tangier Morocco Laboratory of Natural Computation Department of Information and Electrical Engineering and Applied Mathematics University of Salerno 84084 Fisciano SA Italy Department of Medicine University of Salerno 84083 Lancusi SA Italy Dipartimento di Fisica Università degli Studi Aldo Moro Bari and INFN Sezione Di Bari Italy Data Analysis Department Ghent University Ghent Belgium Coma Science Group University of Liège Liège Belgium Cruces Hospital and Ikerbasque Research Center Bilbao Spain BIOtech Department of Industrial Engineering University of Trento and IRCS-PAT FBK 38010 Trento Italy Department of Data Analysis Ghent University Ghent 9000 Belgium The Wellcome Trust Centre for Neuroimaging University College London London WC1N 3BG UK Department of Electronic Engineering NED University of Engineering and Technology Karachi Pakistan Blue Brain Project École Polytechnique Fédérale de Lausanne Lausanne Switzerland Departement of Mathematics Swansea University Swansea Wales UK Laboratory for Topology and Neuroscience at the Brain Mind Institute École polytechnique fédérale de Lausanne Lausanne Switzerland Institute of Mathematics University of Aberdeen Aberdeen Scotland UK Department of Integrativ

来源：评论

学校读者我要写书评

暂无评论

Survey on quality evaluation and control of online reviews

引用

Ruan Jian Xue Bao/Journal of software 2014年第3期25卷 506-527页

作者： Lin, Yu-Ming Wang, Xiao-Ling Zhu, Tao Zhou, Ao-Ying Shanghai Key Laboratory of Trustworthy Computing Software Engineering Institute East China Normal University Shanghai 200062 China Guilin 541004 China

With the development of Web2.0, more and more user-generated content (UGC) occur in Web applications. These contents, especially reviews, are opinion-rich and play important roles in e-commerce. According to the Cone's survey published in 2011, 64% of users like to read the related reviews on goods before they make purchase decisions. It is vital to provide users the accurate, succinct and true reviews. This work surveys the research progresses on quality evaluation and control of reviews focusing on the prediction, summarization and spam review detection. At the end, some potential research topics are pointed out based on these analyses. © Copyright 2014, institute of software, the Chinese Academy of Science. All rights reserved.

关键词： Surveys

来源：评论

学校读者我要写书评

暂无评论

On the security of a privacy-preserving key management scheme for location based services in VANETs

On the security of a privacy-preserving key management schem...

引用

6th International Symposium on Foundations and Practice of Security, FPS 2013

作者： Liu, Bao Zhang, Lei Domingo-Ferrer, Josep Shanghai Key Laboratory of Trustworthy Computing Software Engineering Institute East China Normal University Shanghai China UNESCO Chr. in Data Privacy Department of Computer Engineering and Mathematics Universitat Rovira i Virgili Tarragona Spain

ISBN: (纸本)9783319053011

Location based services (LBSs) are promising value-added services in vehicular ad hoc networks (VANETs), which can yield substantial economic profits. To extensively deploy LBSs in VANETs, it is essential to establish an efficient privacy-preserving key management scheme. In this paper, we point out a privacy weakness in a recent key management scheme based on group signatures for LBSs in VANETs;then we propose a secure and privacy-enhanced version. In our scheme, roadside units (RSUs) act as group managers. Vehicles are distributed into groups maintained by these RSUs. If a vehicle's member key is compromised, one just needs to update the group public key corresponding to its group manager. With this method, the member revocation and privacy leakage problems in schemes based on group signatures are solved effectively. As a result, a vehicle may enjoy LBSs efficiently without surrendering its privacy. © 2014 Springer International Publishing Switzerland.

关键词： Location based services

来源：评论

学校读者我要写书评

暂无评论

Comprehensive economic strength assessment based on decision tree algorithm

引用

Computer Modelling and New Technologies 2014年第12期18卷 403-407页

作者： Hou, Yuan Wu, Min Shanghai Key Lab of Trustworthy Computing Software Engineering Institute East China Normal University Shanghai China

In this paper, we apply some computer software techniques in socio-economics to study an economic decision-making problem, the comprehensive economic strength assessment problem. To achieve delicacy socio-economical decision, we first conduct an asses-sment of various influencing factors involved in the decision problem based on analytic hierarchy process, and then apply two deci-sion-tree algorithms to establish the appropriate models with corresponding classification rules. We also use Matlab to fit the data for the purpose of prediction and validation. The experiments show the effectivity and accuracy of decision-tree algorithms in supplying valuable suggestions for economic decision-making problems.

关键词： Data mining

来源：评论

学校读者我要写书评

暂无评论

Modeling and verification of CAN bus with application layer using UPPAAL

Modeling and verification of CAN bus with application layer ...

引用

作者： Pan, Can Guo, Jian Zhu, Longfei Shi, Jianqi Zhu, Huibiao Zhou, Xinyun Software/Hardware Co-design Engineering Research Center East China Normal University Shanghai China School of Computing National University of Singapore Singapore Singapore Shanghai Key Laboratory of Trustworthy Computing East China Normal University Shanghai China State Key Laboratory of Information Security Institute of Information Engineering Chinese Academy of Sciences China

Controller Area Network (CAN) is a high-speed serial bus system with real-time capability. In this paper, we present a formal model of the CAN bus protocol, mainly focusing on the arbitration process, transmission process, and fault confinement mechanism. Moreover, 11 important properties are formalized in terms of the protocol. Based on the verification tool UPPAAL, we describe the system model and properties for performing verification work of the CAN bus protocol. The verification results indicate that some properties are not satisfied in CAN bus system, most of which are caused by the starvation and bus-off nodes. On this basis, the dynamic priority scheduling algorithm and bus-off recovery mechanism are applied, which indicates that some problems can be solved on the application layer. © 2014 The Authors. Published by Elsevier B.V.

关键词： Scheduling algorithms

来源：评论

学校读者我要写书评

暂无评论

Extending temporal logics with data variable quantifications 34

Extending temporal logics with data variable quantifications

引用

34th International Conference on Foundations of software Technology and Theoretical Computer Science, FSTTCS 2014

作者： Song, Fu Wu, Zhilin Shanghai Key Laboratory of Trustworthy Computing and National Trusted Embedded Software Engineering Technology Research Center East China Normal University China State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences China LIAFA Université Paris Diderot France

ISBN: (纸本)9783939897774

Although data values are available in almost every computer system, reasoning about them is a challenging task due to the huge data size or even infinite data domains. Temporal logics are the well-known specification formalisms for reactive and concurrent systems. Various extensions of temporal logics have been proposed to reason about data values, mostly in the last decade. Among them, one natural idea is to extend temporal logics with variable quantifications ranging over an infinite data domain. In this paper, we focus on the variable extensions of two widely used temporal logics, Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). Grumberg, Kupferman and Sheinvald recently investigated the extension of LTL with variable quantifications. They defined the extension as formulas in the prenex normal form, that is, all the variable quantifications precede the LTL formulas. Our goal in this paper is to do a relatively complete investigation on this topic. For this purpose, we define the extensions of LTL and CTL by allowing arbitrary nestings of variable quantifications, Boolean and temporal operators (the resulting logics are called respectively variable-LTL, in brief VLTL, and variable-CTL, in brief VCTL), and identify the decidability frontiers of both the satisfiability and model checking problem. In particular, we obtain the following results: 1) Existential variable quantifiers or one single universal quantifier in the beginning already entails undecidability for the satisfiability problem of both VLTL and VCTL, 2) If only existential path quantifiers are used in VCTL, then the satisfiability problem is decidable, no matter which variable quantifiers are available. 3) For VLTL formulas with one single universal variable quantifier in the beginning, if the occurrences of the non-parameterized atomic propositions are guarded by the positive occurrences of the quantified variable, then its satisfiability problem becomes decidable. Based on these results o

关键词： Temporal logic

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：