高可信軟體技術教育部重點實驗室

高可信軟體技術教育部重點實驗室(北京大學)

高可信軟體技術教育部重點實驗室依託北京大學,由北京大學信息科學技術學院具體承建,是“計算機軟體與理論”國家重點學科的主要支撐。

簡要概況


北京大學計算機軟體與理論學科的建設歷史可以追溯到1955年。1955年,北京大學計算數學專業建立,培養了我國第一批程序設計專業人員。1978年計算機科學技術系成立,並開始招收第一屆計算機軟體和計算機科學理論的碩士研究生,1984年獲計算機軟體博士學位授予權,1985年獲計算機科學理論博士學位授予權,1996年成為國內首批獲得計算機科學與技術一級學科博士學位授予權的單位之一。2001年北京大學計算機軟體與理論以100%的評審通過率被評為全國重點學科,2007年再次以學科評審第一的成績蟬聯全國重點學科。同時,北京大學的計算機科學與技術學科被認定為全國一級學科重點。
2002年9月,北京大學組建信息科學技術學院,其中,由原計算機科學技術系軟體工程研究所、信息安全研究室、人機交互與多媒體研究室和計算機科學理論研究室組建形成軟體研究所,由原計算機科學技術系網路研究室、資料庫研究室和人工智慧研究室組建形成了網路與信息系統研究所。本實驗室覆蓋了北京大學軟體研究所的絕大部分(除人機交互與多媒體研究室)和網路與信息系統研究所的一部分(資料庫研究室)。
歷史上,北京大學在軟體技術研究方面取得了突出成績。作為我國最早開展操作系統研究的高等學校之一,在楊芙清院士的領導下,曾經在1970年代和1980年代創造過國產操作系統的輝煌,楊芙清主持的我國第一台百萬次集成電路計算機(150機)操作系統獲1978年全國科學大會獎,我國第一個用高級語言書寫的大型操作系統-240機操作系統獲1985年電子工業部科技成果一等獎。資料庫研究始於二十世紀1970年代末,是國內最早從事資料庫與信息系統研究並有重要影響的團隊之一,曾獲國家科技進步二等獎、電子工業部科技進步特等獎等。1990年代後期,隨著分散式對象技術的發展和網路計算的逐步興起,開始進入中間件和信息安全領域的研究。
1980年代初,結合當時我國軟體產業起步和發展的需要,開始進行軟體工程技術與理論的研究。1980年代以來,先後主持了國家“六五”、“七五”、“八五”和“九五”重點科技攻關項目研究開發工作(即青鳥工程,國內20多家單位、300多研究人員參與了聯合攻關)以及多項863高技術計劃課題、自然科學基金課題、教育部博士點基金課題和教育部重點課題等研究工作,在軟體工程技術和理論方面進行了全面、深入、系統、實用的創新性研究。青鳥工程作為我國軟體產業建設的基礎性工作,對我國軟體工程的發展和軟體產業的發展做出了突出貢獻,產生了很好的社會經濟效益。大型軟體開發環境-青鳥系統獲1996年電子工業部科技進步特等獎和1998年國家科技進步二等獎。
“十五”期間,本學科共承擔了國家級、部委、國際合作、橫向合作的各種研究項目近100項,獲得的總合同額過1億元。科研成果“基於Internet、以構件庫為核心的軟體開發平台”獲2006年國家科技進步二等獎,並被選為北京大學211建設標誌性成果。發表學術論文500多篇,其中,發表在國內一級學報以上和國際刊物、國際重要會議上的論文400餘篇,申請發明專利25項,獲授權9項。楊芙清院士應邀在ICSE 2006會議上做主題報告(Keynote),這是ICSE 28年歷史以來所邀請的第一位華人學者主題報告;“基於體系結構、面向構件的軟體開發方法—ABC方法”也被ICSE 2006接受為專題教程(Tutorial),這也是ICSE歷史上首次來自中國的專題教程;在FSE和SIGMOD這2個國際頂級學術會議上實現了中國大陸學術論文的首次發表,ICSE2004上的論文被評為當年的5篇優秀論文之一,其擴展版發表於ACM Transactions on SEM,這也是中國大陸學者的首次。完成了一批國家標準的制定工作,已經主持或參加制定的標準規範有國際標準1項,國家標準6項,信息產業部頒布、立項研究的行業技術標準10項。
“十五”期間本學科的人才培養工作取得了很好成果,共招收博士生113人,碩士生322人;獲博士學位62人,獲碩士學位211人(其中部分碩士生轉為博士生)。其中1篇博士論文被國家教育部評為2005年度百篇優秀論文(2006年公布),3篇博士論文被評為北京大學優秀博士論文(2003,2005和2006),1篇博士論文獲中國計算機學會首屆優秀博士論文(2006),3名博士生獲“微軟學者獎”,1名博士生2005和2006連續兩年入選“IBM PhD Fellowship”獎。
本實驗室於2005年初以軟體所為主體開始申報籌備工作,2006年8月形成申請書初稿,2007年1月正式向教育部遞交實驗室申請書,2007年2月,教育部下文正式批複開始建設,2007年3月,正式上報建設項目計劃任務書,2007年7月,通過建設計劃可行性論證,實驗室進入建設階段。
本實驗室以我國著名科學家楊芙清院士作為主要學術帶頭人,有一支學風嚴謹、研究深入、瞄準國際前沿、以發展我國計算機事業為己任的科學研究隊伍。
目前,實驗室的工作人員共57人,其中固定研究人員47人,包括教授17名(含中國科學院院士2名,博士生導師14名),副教授(副研究員)21人,講師等中級職稱9名,2名專職教輔人員和8名博士后研究人員。此外,還有7位國內外知名的學者在本實驗室任客座研究員和博士生、碩士生指導教師。
實驗室有多人入選各類人才支持計劃或獎勵,包括:國家傑出青年科學基金獲得者3人、教育部長江學者獎勵計劃特聘教授1人、新世紀百千萬人才工程國家級人選1人、中國青年科技獎獲得者2人、中國優秀博士后獎獲得者1人、教育部新世紀人才計劃入選者4人、全國百篇優秀博士學位論文獲得者1人、北京市科技新星2人、中創軟體人才獎獲得者4人。

研究領域


學科前沿:高可信軟體研究涉及到軟體理論、軟體技術與原理、軟體生產過程和管理、以及軟體支撐平台等諸多方面。高可信軟體技術的研究和發展將對未來軟體產業、信息社會的發展起到決定性的作用。高可信軟體技術教育部重點實驗室以北京大學信息科學技術學院軟體研究所為基礎進行建設,以我國著名的科學家楊芙清院士作為主要學術帶頭人,擁有一支學風嚴謹、研究深入、瞄準國際前沿、以振興我國計算機事業為己任的科學研究力量
研究方向 高可信軟體技術教育部重點實驗室的預期研究目標是以高可信軟體技術為核心,從軟體計算模型和形式化方法、軟體工程基礎理論及方法、軟體運行平台及其可信性結構和機理、軟體可信性的監測、評估、度量、驗證、及保障方法,以及領域特定的可信性技術五個方面形成較為系統、全面的高可信軟體技術理論基礎。
本實驗室將以研究高可信軟體技術為主攻方向,主要研究方向分為:
1. 可信軟體的計算模型和形式化方法
2. 高可信軟體工程基礎理論及方法
3. 軟體運行平台及其可信性結構和機理
4. 軟體可信性的評測和保障方法 5. 領域特定的可信性技術
這五個方向構成了高可信軟體從基礎理論、生產、評估和應用的整體環境,其間關係如下圖所示。本實驗室以貫穿高可信軟體技術的應用基礎研究為核心。
研究內容 在可信軟體技術研究中,建立完善的可信軟體的形式化理論體系將為量化、推導和驗證軟體系統的可信性提供理論基礎,建立有效的可信軟體工程方法學將為構造高可信的軟體系統提供高效的開發技術,而研發功能完備的高可信軟體開發和運行支撐平台將為可信軟體的開發、運行、以及監測和評估提供技術支持。本實驗室正在圍繞什麼是可信及可信軟體、如何構造高可信的軟體產品、以及如何度量和驗證軟體產品的可信等核心問題展開研究。
主要研究內容概述如下:
軟體基礎理論方面:探討將各類計算機基礎理論,從傳統的形式系統(如邏輯系統,代數系統等)到Petri網理論以及時段演算等基礎理論,用於可信軟體的形式化建模、描述和驗證;並從量子計算、生物計算等方面方面出發,研究可信計算的新型計算模型及其理論。
軟體開發方法學方面:從經典的開發范型出發,以基於UML軟體建模方法為基礎,研究基於元模型的軟體建模技術、MDA支持框架及元模型(語言)質量評價框架,為可信軟體的開發和評價提供技術基礎;發展基於軟體體系結構、面向構件的軟體開發方法,研究在CBSD中支持軟體可信性分析、設計和驗證的相關理論、技術,為大規模、工業化生產可信軟體提供方法學基礎;研究針對軟體資產的基於信譽的可信性分析、評估理論和技術,研究可信軟體管理機制。
系統軟體及軟體運行平台方面:從操作系統層次,研究運行平台可信性保障技術和機制,支持構造可信的軟體開發平台,為可信軟體的可信運行奠定技術基礎;在軟體中間件技術與平台方面,研究基於微內核的中間件平台可信機制及其構造方法,以及相關的開放式互操作框架、構件在線演化方法、基於體系結構的反射式原理、中間件自適應原理與技術等,為開發可信軟體的運行支撐平台提供重要的實踐基礎。
軟體可信性評測和保障方法方面:將圍繞什麼是可信及可信軟體、如何度量和驗證軟體產品的可信等核心問題展開研究。分別從軟體質量評估和軟體過程兩方面進行研究。前者注重研究可信屬性建模技術、可信軟體分析技術、可信軟體驗證技術、可信軟體測試技術;後者重點研究可信軟體開發擴展技術,形成貫穿軟體生命周期、統一的可信軟體開發過程模型,包括支持量化分析的項目管理、過程監控與效能分析、可信性保障過程及其與其他開發過程的有機結合等技術,支持可信過程的管理與集成,並在度量的基礎上提供過程可信性和效能評估。領域特定的軟體應用技術方面:從網路攻防及信息對抗、安全漏洞發掘技術、以及基於ID的密鑰管理及身份鑒別等與可信軟體的安全性有關的方面進行深入的研究;以虛擬現實技術和企業業務集成這兩類關鍵性軟體應用技術為背景,研究其領域特定的可信性需求及保證理論和技術。
研究團隊 實驗室各研究小組及學術帶頭人和主要骨幹人員如下:
1、可信軟體理論研究組:學術帶頭人:陸汝鈐(院士)、許進(教授)、蘇開樂(教授)、王捍貧(教授);學術骨幹:屈婉玲(教授)、陳一峰(研究員)、焦文品(教授)、劉田(副教授)、曹永知(副教授)。
2、可信軟體工程研究組:學術帶頭人:楊芙清(院士)、梅宏(院士)、邵維忠(教授)、金芝(教授);學術骨幹:謝冰(教授)、麻志毅(副教授)、趙海燕(副教授)、王亞沙(副教授)、趙俊峰(副教授)。
3、可信軟體平台研究組:學術帶頭人:梅宏(院士)、楊冬青(教授)、陳向群(教授);學術骨幹:王千祥(教授)、張路(教授)、黃罡(教授)、孫艷春(副教授)、崔斌(研究員)、王騰蛟(教授)、高軍(教授)。
4、信息安全研究組:學術帶頭人:陳鍾(教授)、王立福(教授);學術骨幹:孫家驌(教授)、胡建斌(副教授)、唐禮勇(副研究員)。
5、可信軟體應用研究組:學術帶頭人:張世琨(研究員);學術骨幹:趙文(副教授)、胡文惠(副教授)。
客座研究人員:李大維(美國Ohio州立大學講座教授,IEEE Fellow),盧琪(美國海軍研究生院教授,IEEE Fellow),李實恭IBM中國研究院院長),鮑豐(新加坡國立研究院信息安全領域首席科學家),Robert Deng(新加坡管理大學信息學院科研主管)。

實驗設備


實驗室的主體在北京大學理科1號樓,目前擁有3、4、5、6、7、8六層的6個大型實驗室和先進的網路環境,實驗室面積約2300平方米。另外,在這些樓層中,實驗室相關的辦公室約20間,提供了約700平方米的辦公空間。已具備的總體研究空間約3000平方米。

項目成果


多年來,實驗室所包含的科研團隊一直得到北京大學211和985的重點支持,也先後承擔了國家計委科技攻關計劃、國家科技部863、973等科技計劃、國家自然科學基金等很多科研項目的研究工作,形成了良好的科研條件。目前,本實驗室已具備由十餘台大型伺服器和先進的網路環境組成的大型軟體開發環境,並具有大量的關鍵性軟體工具,以及軟硬體設計模擬環境。北京大學在這些建設中直接投資超過1000萬元,結合相關科研項目的設備採購支持,總體設備原值超過1500萬元。作為軟體技術研究,本實驗室已具備很好的研究環境,能夠滿足各方面的研究要求。