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

2011 International Conference on computer science and Information technology(ICCSIT 2011)

作者： Litian Xiao Mengyuan Li Ming Gu Jiaguang Sun National Laboratory for Information Science and Technology Key Laboratory for Information System Security Ministry of EducationDepartment of Computer Science and Technology School of Software Tsinghua University Beijing Special Engineering Design and Research Institute National Laboratory for Information Science and Technology Key Laboratory for Information System Security Ministry of Education Department of Computer Science and Technology School of Software Tsinghua University

COQ is an interactive theorem proving tool. The paper abstractly describes the feature of COQ, the architecture and working modes of PLC program with the example of typical PLC. It also introduces the first-order logic syntax and semantics of Intuitionistic Logic. It briefly introduces the main Gallina language syntax elements, the corresponding use methods and main theorem proving tactic on COQ. The work has modeled kernel data type and basic statements and and the denotational semantics of PLC program with Gallina. It has given the correctness proof of PLC program based on theorem proving, i.e. based on semantics function the relationship of configuration between the before codes execution and the after is proved. The main purpose is to prove whether a PLC program satisfies certain nature within a scan period.

关键词： PLC Program, Embedded System, Verification, Denotational Semantics, Theorem Proving, COQ

来源：评论

学校读者我要写书评

暂无评论

A Lock-Free Solution for Load Balancing in Multi-Core Environment

A Lock-Free Solution for Load Balancing in Multi-Core Enviro...

引用

International Workshop on Intelligent Systems and Applications, ISA

作者： Xi Liu Lei Pan Chong-Jun Wang Jun-Yuan Xie National Key Laboratory for Novel Software Technology Department of Computer Science & Technology Nanjing University China Nanjing University Nanjing China

Load balancing device is an important part of cloud platform. One of the most common applications of load balancing is to provide a single powerful virtual machine from multiple servers. In multi-core environment, the load balancing device can run multiple physically parallel load-balancing processes to increase overall performance. An important issue when operating a load-balanced service is how to send all requests in a user session consistently to the same backend server, i.e. session maintaining. Most of multiprocessing load balancing solutions use shared memory and lock when manage session. By modifying Linux kernel, we avoid using shared memory and implement a lock-free multiprocessing load balancing solution.

关键词： Load management Sockets Kernel Servers Linux Throughput Virtual machining

来源：评论

学校读者我要写书评

暂无评论

AADL-based Modeling and TPN-based Verification of Reconfiguration in Integrated Modular Avionics

AADL-based Modeling and TPN-based Verification of Reconfigur...

引用

Asia-Pacific Conference on software Engineering

作者： Dajiang Suo Jinxia An Jihong Zhu State Key Laboratory on Intelligent Technology and Systems Tsinghua National Laboratory for Information Science and Technology Department of Computer Science and Technology Tsinghua University Beijing China

This paper seeks to model the Integrated Modular Avionics (IMA) using Architectural Analysis and Design Language (AADL). In particular, the mechanism to describe the dynamic reconfiguration of multimodal system is presented. By translating the AADL model into Time Petri Net (TPN), some real-time and logical properties (deadlock, reach ability, missed deadline) of reconfiguration could be checked. The analysis results could then be used to adjust the design of software at the early stage of system development and ensure that the reconfiguration of IMA meets the real-time constraints.

关键词： Aerospace electronics Hardware Real time systems software Firing Resource management computer architecture

来源：评论

学校读者我要写书评

暂无评论

Local Channel Assignments in Cognitive Radio Networks

Local Channel Assignments in Cognitive Radio Networks

引用

International Conference on computer Communications and Networks (ICCCN)

作者： Jie Wu Ying Dai Yanchao Zhao Department of Computer and Information Sciences Temple University Philadelphia PA USA State Key Laboratory of Novel Software Department of Computer Science and Technology Nanjing University China

Cognitive radio networks (CRNs) promise to enable the next generation of communication networks. The channel assignment (CA) problem is one of the most important issues in CRNs. In this paper, our goal is to design highly efficient and localized protocols for CA. In addition, we want to maximize node connectivity after CA, which is important for packet delivery. To this end, we design two basic algorithms and an advanced algorithm framework. Within this framework, we can change the edge priority in CA to meet different requirements. Simulation results show that the proposed framework is fast (two rounds of communication among nodes, regardless of network size) and outperforms an existing method.

关键词： Interference Copper Algorithm design and analysis Partitioning algorithms Topology Simulation Bipartite graph

来源：评论

学校读者我要写书评

暂无评论

Throughput maximization in cognitive radio based wireless mesh networks

Throughput maximization in cognitive radio based wireless me...

引用

MILCOM, Military Communications Conference

作者： Yanchao Zhao Jie Wu Sanglu Lu State Key Laboratory of Novel Software Department of Computer Science and Technology Nanjing University China Department of Computer and Information Sciences Temple University Philadelphia PA USA

ISBN: (纸本)9781467300797

Cognitive radio is a key technology needed to better utilize the available spectrum more efficiently. In this paper, we consider the throughput optimization problem via spectrum allocation in the cognitive radio based wireless mesh networks (CR-based WMNs). Unlike prior research, we consider both the lower layer noncontinuous OFDM features and the physical interference model in designing our solution. We model the problem as a mixed integer nonlinear programming (MINLP) problem and show it to be NP-hard. Both a centralized and a localized approximation solution are provided to the problem. Our solution also includes a power information collection process to mitigate the effects of the propagation gain of power as well as a post-allocation adjustment process. Real world data is used in our evaluations to illustrate the effectiveness of our scheme.

关键词： Optimization Logic gates Interference Throughput

来源：评论

学校读者我要写书评

暂无评论

Converting sectional views to three orthographic views to reconstruct 3D models

引用

computer-Aided Design and Applications 2011年第4期8卷 571-582页

作者： Ding, Fengqing Zhang, Hui Wen, Yamei School of Software Tsinghua University China Tsinghua National Laboratory for Information Science and Technology China Department of Computer Science and Technology Tsinghua University China Key Laboratory for Information System Security Ministry of Education

Compared with the CSG-based approach, the Brep-based approach has several advantages to construct 3D models from 2D engineering drawings, such as the structure is simpler and the domain of objects that can be handled is wider. However, this approach cannot handle sectional views directly. In this paper, a new method of converting sectional views to three orthographic views is presented. Firstly, the views which have the same projection direction are merged into one view. If the number of views is two, then a new view will be added according to the coordinate relations. Secondly, elements which have been omitted in sectional views are recovered according to the matching information of the existing edges. Finally, the existing Brepbased approach is used to reconstruct the 3D models. The algorithm can handle full sections, broken-out sections, offset sections as well as two orthographic views. The algorithm has been validated by experiments. © 2011 CAD Solutions, LLC.

关键词： Three dimensional computer graphics

来源：评论

学校读者我要写书评

暂无评论

Scheduling Real-Time Embedded Systems Based on TCPNIA

Journal of Software

引用

Journal of software 2011年第3期6卷 340-348页

作者： Yang, Nianhua Yu, Huiqun Sun, Hua Qian, Zhilin Department of Computer Science and Engineering East China University of Science and Technology Shanghai 200237 China Shanghai Key Laboratory of Computer Software Evaluating and Testing Shanghai 201112 China

TCPNIA (Timed Colored Petri Nets with Inhibitor Arcs, TCPNIA) is a model for specifying real-time embedded systems. It integrates features of colored Petri nets, timed Petri nets and inhibitor arcs. The methods for modeling modules of systems using TCPNIA are proposed. A depth-first scheduling algorithm for TCPNIA is proposed. The system level resource's influence to schedulable path is considered. Different data in tokens will change an execution path and call different data operational functions. The influence from data operational functions is considered in the scheduling algorithm. The time requirement upper bound of a schedulable path can be calculated in the algorithm. Tasks' parallel executions have been considered when the time upper bound of the path is calculated. The soundness of the algorithm is proved. The time and space complexities of the algorithm are also analyzed. The compositional conditions and method for composing schedulable path are given. A case study shows the applicability and feasibility of the method. © 2011 ACADEMY PUBLISHER.

关键词： Petri nets

来源：评论

学校读者我要写书评

暂无评论

Mobility support in Multi-Path TCP

Mobility support in Multi-Path TCP

引用

IEEE International Conference on Communication software and Networks

作者： Sun, Yonghao Cui, Yong Wang, Wendong Ma, Tianze Ismailov, Yuri Zheng, Xin State Key Laboratory of Networking and Switching Technology BUPT Beijing China Department of Computer Science Tsinghua University Beijing China Networks and Systems Ericsson Research Kista Sweden Google Inc. Beijing China

ISBN: (纸本)9781612844855

Mobile devices are emerging with multiple interfaces with diverse access technologies. Simultaneously use multiple interfaces can bring lots of benefits to users. However, current TCP fails to support to simultaneously use multiple interfaces. Thus Multi-Path TCP is proposed to overcome the limitation. But MPTCP itself cannot provide mobility support, which may impose mobility restriction on mobile devices. We thus propose a mobility management scheme inside MPTCP protocol. We first propose several requirements for Multi-Path TCP mobility management and then present our solution. Our solution is based on the concept of ID/Locator separation. We use a permanent address and several temporary addresses to separate host identity and locations. By the cooperation of dynamic DNS and MPTCP, our solution has a good support in MPTCP mobility. Finally, we implement a real-world system of MPTCP with mobility support as a proof of feasibility of our approach. © 2011 IEEE.

关键词： Transmission control protocol

来源：评论

学校读者我要写书评

暂无评论

An approach to analyzing time constrained service composition

引用

Journal of computers 2011年第8期6卷 1723-1731页

作者： Fan, Guisheng Yu, Huiqun Chen, Liqiong Tong, Ruan Department of Computer Science and Engineering East China University of Science and Technology Shanghai 200237 China Shanghai Key Laboratory of Computer Software Evaluating and Testing Shanghai 200237 China Department of Computer Science and Information Engineering Shanghai Institute of Technology Shanghai 200235 China

Service composition is widely applied in different applications. One key issue is how to model and analyze time-related properties for service composition. A model called service composition time-constrained Petri Net (SCTNet) is proposed in the paper, which is capable of capturing time behavior of services accurately. The basic relationships, priority and preemption between services are characterized, meanwhile the transaction properties of service are also considered. In order to reduce the state space of model, we propose four simplification schemas which can maintain structural feature and time delay of SCT-Net, a theorem is given to explain the rational of simplification schemas. We present the concept of the greatest concurrent set and analyze the consistency of overtime handling based on the state space of the model. Finally, a heuristic algorithm for schedule computation is created and the experiments are given to explain the feasibility of our method. © 2011 ACADEMY PUBLISHER.

关键词： Petri nets

来源：评论

学校读者我要写书评

暂无评论

A linear algorithm for pseudo recognition in 3D reconstruction

引用

computer-Aided Design and Applications 2011年第6期8卷 827-839页

作者： Li, Qi Zhang, Hui School of Software Tsinghua University China Department of Computer Science and Technology Tsinghua University China Key Laboratory for Information System Security Ministry of Education China Tsinghua National Laboratory for Information Science and Technology China

Pseudo recognition is essential to reconstruct correct 3D models from engineering drawings. This paper proposes a novel linear algorithm to recognize pseudo elements based on the existence of non-manifold edges. First, mini face loops are defined to construct correct face loops and avoid overlapped loops, which previous loop construction methods would always result in when pseudo elements exist. Then, suspect faces whose all boundary edges are non-manifold edges, are defined to reduce the searching space of the algorithm for pseudo recognition, thus the algorithm can achieve linear time complexity. The algorithm is applicable for wireframe models including planes and basic conicoid surfaces. Experimental results are provided to demonstrate the algorithm. © 2011 CAD Solutions.

关键词： Three dimensional computer graphics

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：