史建琦

史建琦，男，華東師範大學副研究員，院長助理，國家可信嵌入式軟體工程技術研究中心總師辦主任。

基本介紹

• 中文名：史建琦
• 職業：教師
• 專業方向：形式化方法、嵌入式作業系統、工業網際網路軟硬體
• 職務：院長助理
• 就職院校：華東師範大學

研究方向

形式化方法、嵌入式作業系統、工業網際網路軟硬體。

學術成果

• Haiping Pang, Ju Li, Yijia Ruan, Yanhong Huang, Jianqi Shi, Shengchao Qin.Formalization and Verification of the Powerlink Protocol using CSP. In the Proc.23rd Asia-Pacific Software EngineeringConference (APSEC) 2016, Hamilton, NewZealand. (Accepted,Acceptance Rate:19.7%)
• Jianqi Shi, Jifeng He, Huibiao Zhu, Yanhong Huang, Xiaoxian Zhang. ORIENTAIS: Formal Verified OSEK/VDX Real-Time Operating System. In the Proc. 17th ICECCS, Association for Computing Machinery, Paris, France.
• Jianqi Shi, Longfei Zhu, Huixing Fang, Huibiao Zhu, Jian Guo. xBIL - A Hardware Resource Oriented Binary Intermediate Language. In the Proc. 17th ICECCS, Association for Computing Machinery, Paris, France.
• Jianqi Shi, Qin Li, Longfei Zhu, Xin Ye, Yanhong Huang, Huixing Fang and Fu Song. Towards A Binary Intermediate Language for Real-Time Embedded System. Mathematical Problems in Engineering, Volume
• Jianqi Shi, Huixing Fang, Yanhong Huang, Fu Song, Jian Guo and Qin Li. Verifying Interrupt Properties of Real-Time Embedded System in Binary Code Perspective. The Scientific World Journal, Volume
• Jianqi Shi, Longfei Zhu, Huibiao Zhu, Jian Guo, Huixing Fang, Xin Ye and Yanhong Huang. Binary Code Level Verification for Interrupt Safety Properties of Real-Time Operating System. In Proc. 6th TASE IEEE Computer Society, Beijing, China.
• Jianqi Shi, Huixing Fang, Huibiao Zhu and Xin Ye. Formal Verification of OSEK/VDX Real-Time Operating System. Proc. 6th SERE(SSIRI),
• Jianqi Shi, Xin Ye, Liangyu Chen, Pei Zhang, Ningkang Jiang, ESF-An Extensive Service Foundation from Internet of Things Perspective, In Proc. 15th ISORC, IEEE Computer Society, Shenzhen, China.
• Qin Li, Jianqi Shi*, Huibiao Zhu. A Formal Framework for Service Mashups with Dynamic Service Selection. In Proc. Innovation in Systems and Software Engineering.
• Huixing Fang, Jianqi Shi, Huibiao Zhu, Jian Guo, Kim Guldstrand Larsen, Alexandre David. Formal verification and simulation for platform screen doors and collision avoidance in subway control systems. In Proc. International Journal on Software Tools for Technology Transfer (STTT).
• Yanhong Huang, Jifeng He, Huibiao Zhu, Yongxin Zhao, Jianqi Shi, Shengchao Qin: Semantic Theories of Programs with Nested Interrupts. Frontiers of Computer Science, FCS. 2014.
• Conghua Zhou, Yong Wang, Meiling Cao, Jianqi Shi*, Yang Liu. Formal Analysis of MAC in IEEE 802.11p with Probabilistic Model Checking. TASE
• Zhimin Wu, Yang Liu, Jun Sun, Jianqi Shi, Shengchao Qin. GPU Accelerated On-the-Fly Reachability Checking. ICECCS
• Geguang Pu, Jianqi Shi, Zheng Wang, Lu Jin, Jing Liu and Jifeng He. The Validation and Verification of WSCDL. In Proc. IEEE Computer Society, Nagoya, Japan.
• Huixing Fang, Huibiao Zhu, Jianqi Shi. An Object-Oriented Language for Modeling of Hybrid Systems. HASE
• Can Pan, Jian Guo, Longfei Zhu, Jianqi Shi, Huibiao Zhu, Xinyun Zhou. Modeling and Verification of CAN Bus with Application Layer using UPPAAL. Electr. Notes Theor. Comput.
• Liangyu Chen, Jianqi Shi, Ningkang Jiang, An Information Infrastructure for Enterprise Computing Towards The Internet of Things. In Proc. ICISCI, IEEE Computer Society, Harbin, China.
• Xin Li, Yanhong Huang, Jianqi Shi, Jian Guo and Huibiao Zhu. pIML - An Interrupt Program Modelling Language for Real-Time and Embedded Systems. In Proc. IEEE Computer Society, Jeju, Korea.
• Qiu Fang, Xin Ye, Jianqi Shi and Xiaoxian Zhang. A New Approach for Developing Safety-Critical Software in Automotive Industry. In Proc. 5th ICSESS,,IEEE Computer Society, Beijing, China.Yanhong Huang, Yongxin Zhao, Jianqi Shi, and Huibiao Zhu: A Denotational Model for Interrupt-Driven Programs. In Proc. 6th ICST, IEEE Computer Society, Luxembourg.
• Yanhong Huang, Yongxin Zhao, Jianqi Shi, Huibiao Zhu, Shengchao Qin: Investigating Time Properties of Interrupt-Driven Programs. In Proc. 15th SBMF, Association for Computing Machinery, Natal, Brazil.
• Qinwen Ran, Xi Wu, Xin Li, Jianqi Shi, Jian Guo and Huibiao Zhu. Modelling and Verifying the TTCAN Protocol Using Timed CSP. In Proc. 8th TASE, IEEE Computer Society, Changsha, China.
• Longfei Zhu, Peng Liu, Zheng Wang, Jianqi Shi and Huibiao Zhu: A Timing Verification Framework for AUTOSAR OS Component Development based on Real-Time Maude. In Proc. 7th TASE, IEEE Computer Society, Birmingham, UK.
• Huixing Fang, Jian Guo, Huibiao Zhu and Jianqi Shi. Formal Verification and Simulation: Co-Verification for Subway Control Systems. In Proc. 6th TASE,IEEE Computer Society, Beijing, China.
• Longfei Zhu, Min Zhang, Yanhong Huang, Jianqi Shi, Huibiao Zhu. Formalising Application Programming Interfaces of the OSEK/VDX Operating System Specification. In Proc. 5th TASE, IEEE Computer Society, Xian, China.
• Yanhong Huang, Yongxin Zhao, Longfei Zhu, Qin Li, Huibiao Zhu, Jianqi Shi. Modelling and verifying the code-level OSEK/VDX operating system with CSP. In Proc. 5th TASE, IEEE Computer Society, Xian, China.

專利

1. 汽車電子器件中斷安全隱患檢測系統及其檢測方法,何積豐、朱龍飛、史建琦。
2. 一種磁吸附式的單詞反射平面雷射生成器,史建琦、姜寧康、方徽星、黃灩鴻。
3. 一種可調式單次反射平面雷射生成器,史建琦、王振輝、姜寧康、郭占華、黃灩鴻。
4. 具有感測控制功能的工業自動化系統的網際網路接入裝置,史建琦、黃灩鴻、何積豐、王江濤。
5. 一種基於程式演進模型的目標代碼逆向工程方法,史建琦、熊家文、黃灩鴻、何積豐、李昂、方徽星。
6. 一種基於程式演進模型的目標代碼逆向工程系統,史建琦、熊家文、黃灩鴻、何積豐、李昂、方徽星。
7. 一種基於代數演算的中間代碼最佳化系統,黃灩鴻、卜祥興、史建琦、何積豐、李昂、方徽星。
8. 一種基於代數演算的中間代碼最佳化方法,黃灩鴻、卜祥興、史建琦、何積豐、李昂、方徽星。
9. 一種基於機器學習技術的可自感知異常的工控安全防護與報警系統,黃灩鴻、郭欣、史建琦、李昂、方徽星。
10. 一種基於機器學習技術的工控安防方法,黃灩鴻、郭欣、史建琦、李昂、方徽星。
11. 一種信號軌跡驅動的控制系統,史建琦、郭欣、黃灩鴻、李昂、方徽星。
12. 一種智慧型驅動控制系統,史建琦、郭欣、黃灩鴻、李昂、方徽星。
13. 一種基於進程代數的實時協定分析及驗證系統,史建琦、龐海萍、黃灩鴻、李昂、何積豐、方徽星。
14. 一種實時協定的形式化分析及驗證方法,史建琦、龐海萍、黃灩鴻、李昂、何積豐、方徽星。
15. 一種基於形式語義推理和深度學習的自然語言知識挖掘方法,史建琦、吳雙、黃灩鴻、王祥豐、吳苑斌。
16. 一種基於形式語義推理和深度學習的自然語言知識挖掘系統,史建琦、吳雙、黃灩鴻、王祥豐、吳苑斌。
17. 一種空間飛行器的自適應重構方法及系統,黃灩鴻、李炬、史建琦、李昂、何積豐、方徽星。
18. 一種空間飛行器的重構飛行控制方法及系統,黃灩鴻、李炬、史建琦、李昂、何積豐、方徽星。
19. 一種面向目標代碼的程式靜態分析系統,何積豐、卜祥興、史建琦、黃灩鴻、李昂、方徽星。
20. 一種面向目標代碼的程式靜態分析方法,何積豐、卜祥興、史建琦、黃灩鴻、李昂、方徽星。
21. 一種軟體體系結構建模和仿真系統,黃灩鴻、施健、史建琦、方徽星、李昂、李新、何積豐。
22. 一種軟體體系結構建模與仿真方法,黃灩鴻、施健、史建琦、方徽星、李昂、李新、何積豐。
23. 一種軟體自適應決策驗證系統,史建琦、胡志成、黃灩鴻、方徽星、李昂、李新、何積豐。
24. 一種軟體自適應決策驗證方法,史建琦、胡志成、黃灩鴻、方徽星、李昂、李新、何積豐。
25. 一種目標代碼控制流圖生成方法,何積豐、熊家文、史建琦、黃灩鴻、李昂、方徽星。
26. 一種目標代碼控制流圖生成系統,何積豐、熊家文、史建琦、黃灩鴻、李昂、方徽星。
27. 一種惡意程式識別系統,熊家文、史建琦、黃灩鴻、李昂、方徽星、何積豐。
28. 一種惡意程式識別方法,熊家文、史建琦、黃灩鴻、李昂、方徽星、何積豐。
29. 一種基於微核心原型的進程間通信安全性形式化分析驗證系統,毛俠、史建琦、黃灩鴻、李昂。
30. 基於加權下推系統的中斷驗證方法,黃灩鴻、郭欣、史建琦、何積豐、李昂、方徽星。
31. 基於加權下推系統的中斷驗證系統,黃灩鴻、郭欣、史建琦、何積豐、李昂、方徽星。
32. 一種工業環境實景增強式互動終端及系統,何積豐、毛俠、史建琦、黃灩鴻、李昂、方徽星。
33. 一種工業環境實景增強式互動方法,何積豐、毛俠、史建琦、黃灩鴻、李昂、方徽星。
34. 一種線性時態邏輯規範的通用並行挖掘方法,何積豐、熊家文、史建琦、黃灩鴻、李昂、方徽星。
35. 一種線性時態邏輯規範的通用並行挖掘系統,何積豐、熊家文、史建琦、黃灩鴻、李昂、方徽星。
36. 基於時態邏輯的微控制器運行時驗證系統,史建琦、胡志成、黃灩鴻、李昂、方徽星。
37. 基於時態邏輯的微控制器運行時驗證方法,史建琦、胡志成、黃灩鴻、李昂、方徽星。
38. 一種工廠智慧型預警系統,史建琦、李志輝、黃灩鴻、王祥豐、吳苑斌。
39. 一種工廠智慧型預警方法,史建琦、李志輝、黃灩鴻、王祥豐、吳苑斌。
40. 一種基於運行時驗證技術的嵌入式系統軟體調試系統,黃灩鴻、趙慧、史建琦、何積豐、李昂、方徽星。
41. 一種基於運行時驗證技術的嵌入式系統軟體調試方法,黃灩鴻、趙慧、史建琦、何積豐、李昂、方徽星。
42. 帶過去時態的線性時態邏輯性質有界運行時驗證系統,黃灩鴻、熊家文、史建琦、何積豐、李昂。
43. 帶過去時態的線性時態邏輯性質有界運行時驗證方法,黃灩鴻、熊家文、史建琦、何積豐、李昂。
44. 一種基於協同開發系統的構件互動關係建模方法,史建琦、陳心宇、黃灩鴻、李昂、王泊涵。
45. 一種基於協同開發系統的構件互動關係建模系統,史建琦、陳心宇、黃灩鴻、李昂、王泊涵。
46. 一種接入多類型協同件的服務匯流排平台的工作方法,史建琦、皮興興、黃灩鴻、李昂、王泊涵。
47. 一種接入多類型協同件的服務匯流排平台,史建琦、皮興興、黃灩鴻、李昂、王泊涵。
48. 一種基於Group Lasso的半監督哈希圖像搜尋方法,黃灩鴻、史建琦、王祥豐、吳苑斌。
49. 一種基於Group Lasso的半監督哈希圖像搜尋裝置,黃灩鴻、史建琦、王祥豐、吳苑斌。
50. 一種基於虛擬機的程式運行方法,史建琦、魏漢生、黃灩鴻、李昂、王泊涵。
51. 一種基於虛擬機的程式運行系統,史建琦、魏漢生、黃灩鴻、李昂、王泊涵。
52. 一種可信飛行控制系統協同開發的任務分配建模方法,史建琦、李炬、黃灩鴻、李昂、王振輝。
53. 一種可信飛行控制系統協同開發的任務分配建模裝置,史建琦、李炬、黃灩鴻、李昂、王振輝。
54. 一種網聯智慧型能源計量結算方法,史建琦、郭欣、黃灩鴻、熊家文、毛俠。
55. 一種網聯智慧型能源計量結算系統,史建琦、郭欣、黃灩鴻、熊家文、毛俠。
56. 一種結構化文本程式的自動化驗證方法,史建琦、黃灩鴻、卜祥興、熊家文、佘慶。
57. 一種基於中斷控制流圖的中斷驗證系統,史建琦、黃灩鴻、卜祥興、熊家文、佘慶。
58. 一種結構化文本程式的自動化驗證裝置,史建琦、佘慶、黃灩鴻、郭欣、熊家文、毛俠。
59. 一種基於中斷控制流圖的中斷驗證方法,史建琦、佘慶、黃灩鴻、郭欣、熊家文、毛俠。
60. 一種基於區塊鏈的能源網聯監控方法及存儲介質,毛俠、何積豐、史建琦、黃灩鴻、朱罡。
61. 一種基於區塊鏈的能源網聯智慧型裝置及系統,毛俠、何積豐、史建琦、黃灩鴻、朱罡。
62. 一種提高域名系統可用性的方法及系統, 黃灩鴻 熊家文 史建琦 何積豐 李昂。
63. 一種域名系統攻擊檢測方法、裝置及系統,。
64. 一種可程式控制的通用匯流排接口轉換方法,陳晶,史建琦,何積豐,黃灩鴻。
65. 一種可程式控制的通用匯流排接口轉換系統,陳晶,史建琦,何積豐,黃灩鴻。
66. 可程式邏輯控制器程式語言轉換系統,史建琦,黃灩鴻,何積豐,李昂,蔡方達。
67. 可程式邏輯控制器程式語言轉換方法,史建琦,黃灩鴻,何積豐,李昂,蔡方達。
68. 一種基於中間語言的PLC程式驗證系統,史建琦,黃灩鴻,何積豐,李昂,蔡方達。
69. 一種基於中間語言的PLC程式驗證方法,史建琦,黃灩鴻,何積豐,李昂,蔡方達。
70. 一種基於IMCL模型的異構式多平台代碼生成方法,黃灩鴻,史建琦,李炬,李昂,蔡方達。
71. 一種基於IMCL模型的異構式多平台代碼生成系統,黃灩鴻,史建琦,李炬,李昂,蔡方達。
72. 一種複雜工業控制系統的實現方法,黃灩鴻,史建琦,李炬,李昂,蔡方達。
73. 一種複雜工業控制系統,黃灩鴻,史建琦,李炬,李昂,蔡方達。
74. 一種需求功能點智慧型識別系統 ,史建琦,李志輝,黃灩鴻,鮑鈺,戰雲龍,孫文聖。
75. 一種需求功能點智慧型識別方法 ,史建琦,李志輝,黃灩鴻,鮑鈺,戰雲龍,孫文聖。
76. 一種智慧型功能點識別的軟體計價方法 ,史建琦,皮興興,黃灩鴻,鮑鈺,孫文聖,戰雲龍。
77. 一種智慧型功能點識別的軟體計價系統 ,史建琦,皮興興,黃灩鴻,鮑鈺,孫文聖,戰雲龍。
78. 一種基於神經風格遷移的測試用例生成系統 ,史建琦,李志輝,黃灩鴻,蔡方達,王祥豐,金博。
79. 一種基於神經風格遷移的測試用例生成方法 ,史建琦,李志輝,黃灩鴻,蔡方達,王祥豐,金博。