華僑大學(xué)計算機科學(xué)與技術(shù)學(xué)院導(dǎo)師駱翔宇 正文

　　姓名：駱翔宇
　　性別：男　
　　職稱：副教授
　　學(xué)院：計算機科學(xué)與技術(shù)學(xué)院
　　研究方向：形式化驗證、模型檢測、多智能體系統(tǒng)、知識推理、時態(tài)邏輯、認(rèn)知邏輯和安全協(xié)議驗證等；
 　 電子郵箱：

　　
　　基本情況

　　駱翔宇，男，工學(xué)博士，博士后，副教授，碩士生導(dǎo)師。1992年9月至1996年6月在電子科技大學(xué)應(yīng)用數(shù)學(xué)系學(xué)習(xí)，獲理學(xué)學(xué)士學(xué)位；1996年7月至2010年9月在桂林電子科技大學(xué)計算機科學(xué)與工程學(xué)院任教，擔(dān)任副教授和碩士生導(dǎo)師；2001年9月起攻讀中山大學(xué)計算機應(yīng)用技術(shù)專業(yè)的碩士研究生，兩年后提前攻讀中山大學(xué)計算機軟件與理論專業(yè)的博士研究生，2006年6月畢業(yè)并獲工學(xué)博士學(xué)位。攻讀碩士和博士期間分別獲得2002年度中山大學(xué)優(yōu)秀研究生和2006年度廣東省南粵優(yōu)秀研究生獎學(xué)金，2005年下半年在澳大利亞Griffith大學(xué)擔(dān)任助理研究員；2008年8月至2010年10月在清華大學(xué)軟件學(xué)院從事博士后研究；2010年10月調(diào)到華僑大學(xué)計算機科學(xué)與技術(shù)學(xué)院工作至今。

　　研究方向主要包括形式化驗證、模型檢測、多智能體系統(tǒng)、知識推理、時態(tài)邏輯、認(rèn)知邏輯和安全協(xié)議驗證等。當(dāng)前主要研究和開發(fā)模型檢測多智能體系統(tǒng)的關(guān)鍵理論和技術(shù)并用之于形式化分析分布式軟件系統(tǒng)的可靠性和安全性。研究興趣還包括軟件工程、數(shù)據(jù)挖掘和人工智能等。

　　 國內(nèi)外主要學(xué)術(shù)及社會兼職

　　(1) 國家自然科學(xué)基金委員會項目評審專家；
　　(2) 廣西科技項目評估專家；
　　(3) 《中國科學(xué)F輯:信息科學(xué)》、《計算機學(xué)報》、《Knowledge-Based Systems》、《Frontiers of Computer Science in China(FCS)》、《計算機科學(xué)》、《小型微型計算機系統(tǒng)》、《桂林電子科技大學(xué)學(xué)報》的審稿人；
　　(4) 第九屆亞太人工智能國際會議PRICAI-06（SCI收錄，兩年一屆）和第十九屆澳大利亞人工智能國際會議AI-06（SCI收錄）的審稿人

 　　承擔(dān)的部分科研項目　　

　　(1) 2012.1至2015.12，基于多主體認(rèn)知邏輯模型檢測的 Web 服務(wù)組合驗證（No.61170028），國家自然科學(xué)基金（面上項目），主持，55萬，在研
　　(2) 2008.1至2010.12，基于時態(tài)認(rèn)知邏輯的特征交互無界模型檢測（No.60763004），國家自然科學(xué)基金（地區(qū)科學(xué)基金），主持，22萬，2010年底結(jié)題
　　(3) 2009.9至2011.9，基于多智能體邏輯的可信Web服務(wù)模型檢測研究（No.20090450389），中國博士后科學(xué)基金，主持，3萬，已結(jié)題
　　(4) 2007.5至2010.5，模型檢測動態(tài)認(rèn)知邏輯及其應(yīng)用（No.桂科青0728090），廣西青年科學(xué)基金，主持，4萬，已結(jié)題，評為優(yōu)秀
　　(5) 2010.02至2014.02，基于多主體認(rèn)知邏輯的Web服務(wù)模型檢測（No.JB-GJ1001），2010年度華僑大學(xué)“中央高?；究蒲袠I(yè)務(wù)費”國家杰出青年基金培育計劃專項項目，主持，在研
　　(6) 2011.02至2013.01，模型檢測多智能體系統(tǒng)及其應(yīng)用（No. 11BS108），2011年度第一期華僑大學(xué)高層次人才科研啟動費項目，主持，在研
　　(7) 2005.1至2007.12，系統(tǒng)規(guī)范表示與驗證的認(rèn)識邏輯途徑（No.60473004），國家自然科學(xué)基金，參與，23萬，已結(jié)題
　　(8) 2005.12至2007.12，海量信息的協(xié)同性和可生存性的理論與實踐研究（No.2005CB321902），973項目子課題，參與，10萬，已結(jié)題
　　(9) 2010.1 至2012.12，基于描述邏輯和模型檢測的行動理論研究（No.60903079），國家自然科學(xué)基金，排名第二，18萬，在研

　　發(fā)表或錄用的部分學(xué)術(shù)論文

　　截至2011年3月，在《計算機學(xué)報》、《軟件學(xué)報》、《計算機科學(xué)》、《小型微型計算機系統(tǒng)》、《中國科學(xué)F輯》、《The Computer Journal》、《Journal of Software》、《Knowledge-based Systems》等國內(nèi)外期刊，以及MoChArt2010、AAMAS2005、AI2006等國際會議發(fā)表學(xué)術(shù)論文40余篇，其中SCI收錄4篇，EI收錄18篇，ISTP收錄3篇。下面列出部分論文。

　　[1] 駱翔宇, 譚征, 蘇開樂, 吳立軍. 一種基于認(rèn)知模型檢測的Web服務(wù)組合驗證方法. 計算機學(xué)報, 2011, 34(6):1041-1061 (EI收錄)
　　[2] 駱翔宇, 蘇開樂, 顧明. 一種求解認(rèn)知難題的模型檢測方法. 計算機學(xué)報, 2010, 33(3): 406-414 (EI收錄)
　　[3] Xiangyu Luo, Kaile Su, Ming Gu, Lijun Wu, Jinji Yang. Symbolic Model Checking the Knowledge in Herbivore Protocol. Sixth Workshop on Model Checking and Artificial Intelligence (MoChArt 2010), July 11, 2010 (EI收錄)
　　[4] Xiangyu Luo, Jingjing Lu, Kaile Su, Rongsheng Dong. Translation-based Verification of Web Services Composition via ZING. 2010 IEEE International Conference on Intelligent Computing and Integrated Systems, October 22, 2010 (EI收錄)
　　[5] Xiangyu Luo, Kaile Su, Abdul Sattar, Yan Chen. Solving Sum and Product Riddle via BDD-Based Model Checking. 2008 IEEE/WIC/ACM International Conference on Web Intelligence and Intelligent Agent Technology, 2008,3(3): 630-633 (EI收錄)
　　[6] Xiangyu Luo, Yan Chen, Ming Gu, and Lijun Wu. Model Checking Needham-Schroeder Security Protocol based on Temporal Logic of Knowledge. 2009 International Conference on Networks Security, Wireless Communications and Trusted Computing, 2009,2: 548-551 (EI,ISTP收錄)
　　[7] Xiangyu Luo, Zheng Tan, Rongsheng Dong. Automatic Verification of Composite Web Services Based on Temporal and Epistemic Logic. Third International Conference on Genetic and Evolutionary Computing, 2009 : 693-696 (EI收錄)
　　[8] Xiangyu Luo, Aicheng Xuan, Rongsheng Dong. Detecting Feature Interactions in Web Services with Timed Automata. Third International Conference on Genetic and Evolutionary Computing, 2009: 276-279 (EI收錄)
　　[9] 駱翔宇, 軒愛成, 沙宗魯. 基于Verics 的組合Web 服務(wù)有界模型檢測. 小型微型計算機系統(tǒng), 32(3):412-415
　　[10] 駱翔宇, 陳艷, 古天龍, 董榮勝. 基于時態(tài)認(rèn)知邏輯的Web服務(wù)模型檢測. 計算機科學(xué),2009, 36(8): 153-157
　　[11] 駱翔宇, 古天龍, 董榮勝. 和與積數(shù)迷的符號化模型檢測. 計算機科學(xué),2008, 35(5): 184-186
　　[12] 駱翔宇, 陳艷. Web服務(wù)的形式化驗證. 計算機工程,2010,36(5): 257-259
　　[13] 駱翔宇, 軒愛成, 沙宗魯. 基于Verics的組合Web服務(wù)有界模型檢測. 小型微型計算機系統(tǒng),2011年3期
　　[14] 駱翔宇, 軒愛成, 沙宗魯. 基于時間自動機的Web服務(wù)模型檢測. 計算機科學(xué),2010年8期
　　[15] 駱翔宇, 譚征, 董榮勝. 一種Web服務(wù)特征交互自動檢測方法. 計算機科學(xué),2010年12期
　　[16] 駱翔宇, 蘇開樂, 楊晉吉. 有界模型檢測同步多智能體系統(tǒng)的知識與時間. 軟件學(xué)報,2006,17(12): 2485-2498 (EI收錄)
　　[17] Xiangyu Luo, Kaile Su, Abdul Sattar, Mark Reynolds. Verification of Multi-agent Systems via Bounded Model Checking. The 19th Australian Joint Conference on Artificial Intelligence,Volume 4304 of LNCS, Springer, 2006: 69–78 (EI,ISTP收錄)
　　[18] Xiangyu Luo, Kaile Su, Abdul Sattar, Qingliang Chen, Guanfeng Lv. Bounded Model Checking Knowledge and Branching Time in Synchronous Multi-agent Systems. The fourth International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2005),ACM, 2005: 1129–1130 (EI收錄)
　　[19] 駱翔宇, 成良玉. 用面向?qū)ο蠓椒ㄔO(shè)計并實現(xiàn)數(shù)據(jù)庫的動態(tài)查詢. 計算機工程與應(yīng)用,2003,15:200-202
　　[20] 蘇開樂, 駱翔宇, 呂關(guān)鋒. 符號化模型檢測CTL*. 計算機學(xué)報,2005, 28(11): 1798-1806 (EI收錄)
　　[21] Kaile Su, Xiangyu Luo, Abdul Sattar, Mehmet A Orgun. The Interpreted System Model of Knowledge, Belief, Desire and Intention. The fifth International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2006),ACM, 2006: 220–222 (EI收錄)
　　[22] Guohun Zhu, Xiangyu Luo, Yuqing Miao. Exact Weight Perfect Matching of Bipartite Graph is NP-Complete. The 2008 International Conference of Applied and Engineering Mathematics,World Congress on Engineering, 2008: 878-880 (ISTP收錄)
　　[23] 軒愛成, 駱翔宇, 沙宗魯, 董榮勝. 一種執(zhí)行代價較小的Web服務(wù)動態(tài)合成方法. 微電子學(xué)與計算機,28(2):166-170
　　[24] 何青, 駱翔宇, 蘇開樂. 基于符號化模型檢測的對弈必勝策略驗證. 計算機工程與應(yīng)用,2008,44(17)
　　[25] 楊晉吉, 蘇開樂, 駱翔宇, 林翰, 肖茵茵. 有界模型檢測的優(yōu)化. 軟件學(xué)報,2009, 20(8): 2005?2014 (EI收錄)
　　[26] Kaile Su, Abdul Sattar and Xiangyu Luo（通訊作者）. Model Checking Temporal Logics of Knowledge Via OBDDs. The Computer Journal,2007, 50(4): 403-420 (SCI收錄)
　　[27] Rongsheng Dong, Zhao Wei, Xiangyu Luo, Fang Liu. Testing Conformance of BPEL Business Process Based on Model Checking. JOURNAL OF SOFTWARE, 5(9): 1030-1037, SEPTEMBER 2010 （EI收錄）
　　[28] Lijun Wu, Jinshu Su, Xiangyu Luo. A Concurrent Dynamic Logic of Knowledge, Belief and Certainty for Multi-Agent Systems. The twenty-second Canadian Conference on Artificial Intelligence, LNAI 5549, 2009: 146–157 (EI, ISTP收錄)
　　[29] Rongsheng Dong, Zhao Wei, Xiangyu Luo. Model Checking Behavioral Specification of BPEL Web Services. The 2008 International Conference of Computer Science and Engineering, World Congress on Engineering, 2008: 198-203 (ISTP收錄)
　　[30] 董榮勝, 吳光偉, 駱翔宇, 古天龍. 一類具有“開端”結(jié)構(gòu)安全協(xié)議的分析方法研究. 計算機科學(xué),2008, 35(7): 45-49
　　[31] DONG Rong-sheng, WANG Fei-ming, LUO Xiang-yu. Dynamic Web Services Composition Based on QoS Model. 2010 IEEE International Conference on Intelligent Computing and Integrated Systems, October 22, 2010（EI收錄）
　　[32] Lijun Wu, Jinshu Su, Kaile Su, Xiangyu Luo, Zhihua Yang. A concurrent dynamic logic of knowledge, belief and certainty for multi-agent systems. Knowledge-Based Systems,23 (2010): 162–168 (SCI收錄)
　　[33] Kaile Su, Abdul Sattar, Kewen Wang, Xiangyu Luo, Guido Governatori, Vineet Nair. Observation-based Model for BDI-Agents. AAAI 2005,AAAI Press / The MIT Press, 2005: 190–195 (EI收錄)
　　[34] Lijun Wu, Zili Chen, Jinshu Su, Xiangyu Luo. The Based-role PMI Model for Access Control in large Scale Netware System. 2010 International Conference on Computer Design and Applications (ICCDA 2010), Vol.2: 81-84 （EI收錄）
　　[35] LI Li, Song XiaoYu, Gu Ming, Luo XiangYu. Competent Predicate Abstraction in Model Checking. SCIENCE CHINA INFORMATION SCIENCES, 54(2): 258-267, Feb. 2011 （SCI收錄）
　　[36] Kaile Su, Weiya Yue, Abdul Sattar, Mehmet A. Orgun, Xiangyu Luo. Observation-Based Logic of Knowledge, Belief, Desire and Intention. First International Conference on Knowledge Science, Engineering and Management,Volume 4092 of LNCS, Springer, 2006: 366–378 (SCI收錄)

　　 發(fā)表的部分教學(xué)論文

　　[1] 駱翔宇, 古天龍, 董榮勝. 模型檢測課程建設(shè)初探. 計算機科學(xué), 第35卷, 第11期專輯: 150-155
　　[2] 駱翔宇, 董榮勝, 古天龍. 模型檢測課程實踐教學(xué)初探. 計算機科學(xué), 第36卷, 第7期專輯: 255-259
　　[3] 駱翔宇, 古天龍, 董榮勝. “離散結(jié)構(gòu)”課程中有關(guān)OBDD的教學(xué)實踐. 計算機科學(xué), 第 34卷, 第7期專輯
　　[4] 俸皓, 朱細(xì)平, 駱翔宇, 董榮勝. 以計算思維能力培養(yǎng)為核心的《程序設(shè)計基礎(chǔ)》課程教學(xué)改革與實踐. 計算機科學(xué), 第35卷, 第11期專輯: 96-98
　　[5] 鄧珍榮, 黃文明, 駱翔宇, 周婭. 以計算思維培養(yǎng)為核心的”數(shù)據(jù)結(jié)構(gòu)與算法”課程教學(xué)改革與實踐. 計算機科學(xué), 第35卷, 第11期專輯: 99-101
　　
　　*如果發(fā)現(xiàn)導(dǎo)師信息存在錯誤或者偏差，歡迎隨時與我們聯(lián)系，以便進(jìn)行更新完善。

添加華僑大學(xué)學(xué)姐微信，或微信搜索公眾號“考研派小站”，關(guān)注[考研派小站]微信公眾號，在考研派小站微信號輸入[華僑大學(xué)考研分?jǐn)?shù)線、華僑大學(xué)報錄比、華僑大學(xué)考研群、華僑大學(xué)學(xué)姐微信、華僑大學(xué)考研真題、華僑大學(xué)專業(yè)目錄、華僑大學(xué)排名、華僑大學(xué)保研、華僑大學(xué)公眾號、華僑大學(xué)研究生招生）]即可在手機上查看相對應(yīng)華僑大學(xué)考研信息或資源。

華僑大學(xué)