人民網首頁

--2014清華大學計算機系篇
動態消息
獲獎學生風採
中國人民大學|北京大學|清華新傳學院|中國傳媒大學|武漢大學|復旦大學
南京大學|華中科技大學|廈門大學|中央美術學院|北京郵電大學|清華計算機系
人民網 >> 傳媒 >> 傳媒專題 >> 人民網獎學金 >> 清華大學計算機科學與技術系 >> 清華計算機2014

歷年獲獎名單

        

人民網獎學金獲獎名單：
曾薇、周睿鳴、李暄、彭璟、劉建妮、楊健

人民網優秀論文獲獎者名單：
一等獎：
徐厚暢 韓梅映雪 李煜申 邢天意
二等獎：
寧威  葛明寧  童渝
三等獎：
毛逸嶸     

歷年獲獎名單：

2013     2012    2011    2010    2009

技術獎一等獎（4）

劉雲輝

基於結構化L2,1優化的多樣性關鍵幀提取
為了能對一段短視頻提供語義上有意義的表達，本文提出了一種能同時刻畫可重構能力和多樣性的結構化的L2,1優化模型。為了防止相似的樣本被同時選中，該模型加入了互抑制懲罰項。在互抑制因子的選擇方面，該模型有高度的靈活性，本文中，我們加入了視頻中的時序信息來保証結果的多樣性。對於本文中非凸的目標函數，我們推導出一個迭代算法，來解決這個優化問題。我們運用多個Youtube上的片段和室內的移動機器人拍攝的視頻來做性能評價。實驗結果明確地顯示出，相比於其他當前的方法，本文的策略能使優化模型得到更加多樣化的關鍵幀。
詳細 >>

姜宇

Design of Mixed Synchronous
Today’s system-on-chip and distributed systems are commonly equipped with multiple clocks. The key challenges in designing such systems are (1) how to model multi-clocked local synchronous component, local asynchronous component, and asynchronous communication among components in a single framework, (2) how to ensure the correctness of model, and keep consistency between the model and the implementation of real system. In this paper, we propose a novel computation model named GalsBlock for the design of multi-clocked embedded system with both synchronous and asynchronous components. The computation model consists of several hierarchical compound and atom blocks communicating with data port connections. Each atom block can be refined as parallel mealy automata. The unified operational semantic and formal semantic are defined, which can be used for simulation and verification, respectively. Then, we can generate efficient VHDL code from the validated model. The size of the generated code is reduced by up to 40% compared to simulink VHDL code generator of Stateflow for a function that can be modeled by both Galsblock and Stateflow. We have developed the graphical modeling, simulation, verification, and code generation toolkit to support the computation model, and applied them in the design of a sub-system used in the train communication control according to the standard IEC-61375. Two critical bugs in the standard are detected in the model validation process, and the automatically generated sub-system according to the revised model is now used in real subway control.
詳細 >>

戴惠辰

依據被動測量的鏈路負載均衡
研究提出了一種實時在線的流量工程方法在多條路徑之間實現負載均衡，即LAMP（load adaptation based on measuring passively）. LAMP將流量從高利用率的鏈路轉移到低利用率的鏈路上，轉移的依據是以被動方式收集的信息，包括數據包往返時延（round trip time，RTT）和鏈路利用率。LAMP不需要周期性地探測網絡，不需要路由器之間的大量通信，更不需要對輸入的流量和網絡拓扑做任何假設。評估結果表明，LAMP能夠有效降低鏈路利用率，而且具有良好的穩定性。
詳細 >>

單來祥

基於按需即時去擴展化的LTL公式到B?chi自動機直接轉換算法研究
在顯式狀態模型檢測技術領域，現實系統通常被表達成線性時序邏輯(LTL)公式，並被轉換成B?chi自動機(BA)。為了提高轉換的效率，當前很多轉換工具使用了中間自動機，如擴展的B?chi自動機(GBA)。去擴展化就是將GBA轉換成BA的過程。本文提出並實現了LTL公式到BA的直接轉換算法。本文中首次提出使用一個新的標簽---接受度(Acceptance Degree，)用於記錄轉換過程中狀態和變遷上已經滿足的接受條件。是給定的LTL公式中子公式的集合。根據，本文提出一種不同於經典去擴展化算法的方法---按需即時的去擴展化(On-the-fly De-generalization，)算法。算法在展開LTL公式的過程中根據需要執行，它不同於完全展開LTL公式后，再進行去擴展化的經典方法。利用算法，我們實現了LTL 公式到B?chi自動機的直接轉換，不需要使用中間自動機保存轉換過程中臨時結果。通過使用五組常用的LTL公式和四組隨機生成的LTL公式測試已有的轉換工具和本文提出轉換工具，實驗結果顯示本文提出的直接轉換方法避免了傳統轉換算法中的多重轉換步驟，降低了計算復雜度，所需的轉換時間更短。
詳細 >>

技術獎二等獎（2）

吳丹

DIMR：不相交多路徑域間路由
域間多路徑路由, 它使源AS可以使用多條路 徑發送流量到同一個目的AS, 是一種有前途的技術, 可以提高帶寬,提高容錯性和故障的快速恢復。 但是,以前的域間多路徑路由協議,往往會產生一些相交的路徑, 相交的地方形成了瓶頸, 這使得他們很容易在瓶頸處形成單點故障,因此效率不高, 降低了域間流量工程或並發多徑傳輸的效率。 在本文中,我們提出了不相交多路徑域間路由(DIMR), 試圖讓更多的AS找到兩條不相交的路徑。 在這個協議中,我們提出了路徑組合的概念並設計了的路徑組合選擇的規則。 我們評估DIMR仿真。 實驗結果表明,DIMR能使90%以上的多連接AS找到兩條不相交的路徑。
詳細 >>

沈志榮

可搜索加密機制研究與進展
隨著雲計算的迅速發展，用戶開始數據遷移到雲端服務器，以此避免繁瑣的本地數據管理並獲得更加便捷的服務。為了保証數據安全和用戶隱私，數據一般是以密文存儲在雲端服務器中，但是用戶將會遇到如何在密文上進行查找的難題。可搜索加密(Searchable Encryption, 簡稱SE)是近年來發展的一種支持用戶在密文上進行關鍵字查找的密碼學原語，它能夠為用戶節省大量的網絡和計算開銷，並充分利用雲端服務器龐大的計算資源進行密文上的關鍵字查找。本文介紹了SE機制的研究背景和目前的研究進展，對比闡述了基於對稱密碼學和基於公鑰密碼學而構造的SE機制的不同特點，分析了SE機制在支持單詞搜索、連接關鍵字搜索和復雜邏輯結構搜索語句的研究進展。最后闡述了其所適用的典型應用場景，並討論了SE機制未來可能的發展趨勢。
詳細 >>

技術獎三等獎（3）

張寶寶、王??

IP-to-AS映射修正粒度的系統分析
獲得精確的IP-to-AS映射表，對於網絡管理人員診斷網絡故障和對於網絡研究人員發現AS級網絡拓扑有著重要的意義。一種獲得IP-to-AS映射表的方法是基於traceroute路徑和BGP 的AS路徑是一致的假設，通過最大化匹配traceroute和BGP路徑對的數量，來修正從路由表裡提取的初始的IP-to-AS映射表。關於修正這個初始的IP-to-AS映射表，有兩種粒度的修正方法，一種是/24前綴粒度的修正方法[1]，另一種是IP地址粒度的修正方法[2]。IP地址粒度的修正方法相比於前綴粒度的修正方法，可以大大提高路徑對的匹配度。但是前綴粒度的方法和IP地址粒度的方法各有優缺點，本文提出了一種系統化的基於分類樹的分析方法，可以系統、全面和定量的分析前綴粒度方法和IP地址粒度方法各自的優缺點。
詳細 >>

蔣運韞、楊弋、肖 天

使用調試寄存器進行Linux內核數據競爭檢測
並發程序中的數據競爭問題很難被檢測和修復.以往的研究大多針對用戶層的數據競爭檢測並在此問題上取得了重大的進展,但在操作系統內核層面的數據競爭問題卻幾乎沒有涉及.內核代碼使用的同步機制遠比用戶層應用程序中復雜,如不同種類的鎖,軟硬件中斷,大量的信號量原語以及各種底層的共享資源等.這些差別使得原有的用戶層檢測方法很難被應用到內核環境中.本文給出一個可有效檢測Linux操作系統內核數據競爭問題的工具,基於當前通用處理器中現有的硬件結構調試寄存器,使用動態檢測方法在內核程序運行過程中捕獲數據競爭.初步的實驗結果顯示,本工具可有效地檢測到內核中的數據競爭實例.
詳細 >>

單來祥

基於按需即時去擴展化的LTL公式到B?chi自動機直接轉換算法研究
在顯式狀態模型檢測技術領域，現實系統通常被表達成線性時序邏輯(LTL)公式，並被轉換成B?chi自動機(BA)。為了提高轉換的效率，當前很多轉換工具使用了中間自動機，如擴展的B?chi自動機(GBA)。去擴展化就是將GBA轉換成BA的過程。本文提出並實現了LTL公式到BA的直接轉換算法。本文中首次提出使用一個新的標簽---接受度(Acceptance Degree，)用於記錄轉換過程中狀態和變遷上已經滿足的接受條件。是給定的LTL公式中子公式的集合。根據，本文提出一種不同於經典去擴展化算法的方法---按需即時的去擴展化(On-the-fly De-generalization，)算法。算法在展開LTL公式的過程中根據需要執行，它不同於完全展開LTL公式后，再進行去擴展化的經典方法。利用算法，我們實現了LTL 公式到B?chi自動機的直接轉換，不需要使用中間自動機保存轉換過程中臨時結果。通過使用五組常用的LTL公式和四組隨機生成的LTL公式測試已有的轉換工具和本文提出轉換工具，實驗結果顯示本文提出的直接轉換方法避免了傳統轉換算法中的多重轉換步驟，降低了計算復雜度，所需的轉換時間更短。
詳細 >>