史建琦

2007 - 2012 华东师范大学 计算机理论 博士学位

2003 - 2007 华东师范大学 软件工程  学士学位

国家可信嵌入式软件工程技术研究中心 / 软硬件协同设计技术与应用教育部工程研究中心 副主任

联合国工业发展组织UNIDO 国别技术顾问

国家标准委员会-工业过程测量控制和自动化标准化技术委员会(TC24)/SC5 委员

上海计算机学会 嵌入式与普适计算分委会 副主任

形式化方法，嵌入式操作系统，工业互联网软硬件

嵌入式实时操作系统

Real-Time Operating System

学术论文

• 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  Engineering Conference (APSEC) 2016,  Hamilton, New Zealand. (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, 2012, pp 293-301, 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, 2012, pp 211-219, 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, 2014, Volume 2014, a925402, pp 1-13, ISSN: 1563-5147.

• 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, 2014, Volume 2014, a451085, pp 1-14, ISSN: 1537-744X.

• 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 2012, pp 223-226, 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), 2012, pp 124-133, Washington, D.C., USA.

• Jianqi Shi, Xin Ye, Liangyu Chen, Pei Zhang, Ningkang Jiang, ESF-An Extensive Service Foundation from Internet of Things Perspective, In Proc. 15th ISORC, 2012, pp 59-64, 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. 2014, Volume 10, Issue 3 (2014), pp 219-234, ISSN: 1614-5046, Springer.

• 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). 2014, Volume 16, Issue 4, pp 339-361, ISSN:1614-5046, Springer.

• 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 2015: 55-62

• Zhimin Wu, Yang Liu, Jun Sun, Jianqi Shi, Shengchao Qin. GPU Accelerated On-the-Fly Reachability Checking. ICECCS 2015: 100-109

• Geguang Pu, Jianqi Shi, Zheng Wang, Lu Jin, Jing Liu and Jifeng He. The Validation and Verification of WSCDL. In Proc. 14th APSEC, 2007, pp 81-88, IEEE Computer Society, Nagoya, Japan.

• Huixing Fang, Huibiao Zhu, Jianqi Shi. An Object-Oriented Language for Modeling of Hybrid Systems. HASE 2015: 1-9

• 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. Sci. 309: 31-49 (2014)

• Liangyu Chen, Jianqi Shi, Ningkang Jiang, An Information Infrastructure for Enterprise Computing Towards The Internet of Things. In Proc. ICISCI, 2011, pp 84-91, 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. 21th APSEC, 2014, 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, 2014, pp 64-69,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, 2013, pp 15-20, 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, 2012, pp 131-146, 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, 2014, 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, 2013, pp 29-36, 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, 2012, pp 145-152, 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, 2011, pp 27-34, 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, 2011, pp 142-149, IEEE Computer Society, Xian, China.

专利

1. ZL 2011 1 0096707.3,汽车电子器件中断安全隐患检测系统及其检测方法,何积丰、朱龙飞、史建琦

2. ZL 2014 2 0378499.5,一种磁吸附式的单词反射平面激光生成器,史建琦、姜宁康、方徽星、黄滟鸿

3. ZL 2014 2 0378506.1,一种可调式单次反射平面激光生成器,史建琦、王振辉、姜宁康、郭占华、黄滟鸿

4. 201510670509.1 ,具有传感控制功能的工业自动化系统的互联网接入装置,史建琦、黄滟鸿、何积丰、王江涛

5. 201610456943.4 ,一种基于程序演进模型的目标代码逆向工程方法,史建琦、熊家文、黄滟鸿、何积丰、李昂、方徽星

6. 201610456941.5 ,一种基于程序演进模型的目标代码逆向工程系统,史建琦、熊家文、黄滟鸿、何积丰、李昂、方徽星

7. 201610459128.3 ,一种基于代数演算的中间代码优化系统,黄滟鸿、卜祥兴、史建琦、何积丰、李昂、方徽星

8. 201610456922.2 ,一种基于代数演算的中间代码优化方法,黄滟鸿、卜祥兴、史建琦、何积丰、李昂、方徽星

9. 201610456945.3 ,一种基于机器学习技术的可自感知异常的工控安全防护与报警系统,黄滟鸿、郭欣、史建琦、李昂、方徽星

10. 201610456944.9 ,一种基于机器学习技术的工控安防方法,黄滟鸿、郭欣、史建琦、李昂、方徽星

11. 201610459066.6 ,一种信号轨迹驱动的控制系统,史建琦、郭欣、黄滟鸿、李昂、方徽星

12. 201610456888.9,一种智能驱动控制系统,史建琦、郭欣、黄滟鸿、李昂、方徽星

13. 201610755248.8,一种基于进程代数的实时协议分析及验证系统,史建琦、庞海萍、黄滟鸿、李昂、何积丰、方徽星

14. 201610755243.5,一种实时协议的形式化分析及验证方法,史建琦、庞海萍、黄滟鸿、李昂、何积丰、方徽星

15. 201610757043.3,一种基于形式语义推理和深度学习的自然语言知识挖掘方法,史建琦、吴双、黄滟鸿、王祥丰、吴苑斌

16. 201610755226.1,一种基于形式语义推理和深度学习的自然语言知识挖掘系统,史建琦、吴双、黄滟鸿、王祥丰、吴苑斌

17. 201610757031.0,一种空间飞行器的自适应重构方法及系统,黄滟鸿、李炬、史建琦、李昂、何积丰、方徽星

18. 201610754975.2,一种空间飞行器的重构飞行控制方法及系统,黄滟鸿、李炬、史建琦、李昂、何积丰、方徽星

19. 201610927633.6,一种面向目标代码的程序静态分析系统,何积丰、卜祥兴、史建琦、黄滟鸿、李昂、方徽星

20. 201610927632.1,一种面向目标代码的程序静态分析方法,何积丰、卜祥兴、史建琦、黄滟鸿、李昂、方徽星

21. 201611137739.2,一种软件体系结构建模和仿真系统,黄滟鸿、施健、史建琦、方徽星、李昂、李新、何积丰

22. 201611137729.9,一种软件体系结构建模与仿真方法,黄滟鸿、施健、史建琦、方徽星、李昂、李新、何积丰

23. 201611219520.7,一种软件自适应决策验证系统,史建琦、胡志成、黄滟鸿、方徽星、李昂、李新、何积丰

24. 201611218766.2,一种软件自适应决策验证方法,史建琦、胡志成、黄滟鸿、方徽星、李昂、李新、何积丰

25. 201611168496.9,一种目标代码控制流图生成方法,何积丰、熊家文、史建琦、黄滟鸿、李昂、方徽星

26. 201611169736.7,一种目标代码控制流图生成系统,何积丰、熊家文、史建琦、黄滟鸿、李昂、方徽星

27. 201611169725.9,一种恶意程序识别系统,熊家文、史建琦、黄滟鸿、李昂、方徽星、何积丰

28. 201611167528.3,一种恶意程序识别方法,熊家文、史建琦、黄滟鸿、李昂、方徽星、何积丰

29. 201611167121.0,基于微内核原型的进程间通信安全性形式化分析验证系统,毛侠、史建琦、黄滟鸿、李昂

30. 2.0171E+11,基于加权下推系统的中断验证方法,黄滟鸿、郭欣、史建琦、何积丰、李昂、方徽星

31. 201710139023.4,基于加权下推系统的中断验证系统,黄滟鸿、郭欣、史建琦、何积丰、李昂、方徽星

32. 201710138192.6,一种工业环境实景增强式交互终端及系统,何积丰、毛侠、史建琦、黄滟鸿、李昂、方徽星

33. 201710139083.6,一种工业环境实景增强式交互方法,何积丰、毛侠、史建琦、黄滟鸿、李昂、方徽星

34. 201710139684.7,一种线性时态逻辑规范的通用并行挖掘方法,何积丰、熊家文、史建琦、黄滟鸿、李昂、方徽星

35. 201710138191.1,一种线性时态逻辑规范的通用并行挖掘系统,何积丰、熊家文、史建琦、黄滟鸿、李昂、方徽星

36. 201710138988.1,基于时态逻辑的微控制器运行时验证系统,史建琦、胡志成、黄滟鸿、李昂、方徽星、

37. 201710139008.X,基于时态逻辑的微控制器运行时验证方法,史建琦、胡志成、黄滟鸿、李昂、方徽星、

38. 201710322901.6,一种工厂智能预警系统,史建琦、李志辉、黄滟鸿、王祥丰、吴苑斌

39. 201710322900.1,一种工厂智能预警方法,史建琦、李志辉、黄滟鸿、王祥丰、吴苑斌

40. 201710322906.9,一种基于运行时验证技术的嵌入式系统软件调试系统,黄滟鸿、赵慧、史建琦、何积丰、李昂、方徽星

41. 201710322903.5,一种基于运行时验证技术的嵌入式系统软件调试方法,黄滟鸿、赵慧、史建琦、何积丰、李昂、方徽星

42. 201710434655.3,带过去时态的线性时态逻辑性质有界运行时验证系统,黄滟鸿、熊家文、史建琦、何积丰、李昂

43. 201710434656.8,带过去时态的线性时态逻辑性质有界运行时验证方法,黄滟鸿、熊家文、史建琦、何积丰、李昂

44. 201710434650.0,一种基于协同开发系统的构件交互关系建模方法,史建琦、陈心宇、黄滟鸿、李昂、王泊涵

45. 201710433623.1,一种基于协同开发系统的构件交互关系建模系统,史建琦、陈心宇、黄滟鸿、李昂、王泊涵

46. 201710433625.0,一种接入多类型协同件的服务总线平台的工作方法,史建琦、皮兴兴、黄滟鸿、李昂、王泊涵

47. 201710434096.6,一种接入多类型协同件的服务总线平台,史建琦、皮兴兴、黄滟鸿、李昂、王泊涵

48. 201710434078.8,一种基于Group Lasso的半监督哈希图像搜索方法,黄滟鸿、史建琦、王祥丰、吴苑斌

49. 201710437582.3,一种基于Group Lasso的半监督哈希图像搜索装置,黄滟鸿、史建琦、王祥丰、吴苑斌

50. 201710423864.8,一种基于虚拟机的程序运行方法,史建琦、魏汉生、黄滟鸿、李昂、王泊涵

51. 201710434653.4,一种基于虚拟机的程序运行系统,史建琦、魏汉生、黄滟鸿、李昂、王泊涵

52. 201710434654.9,一种可信飞行控制系统协同开发的任务分配建模方法,史建琦、李炬、黄滟鸿、李昂、王振辉

53. 201710434652.X,一种可信飞行控制系统协同开发的任务分配建模装置,史建琦、李炬、黄滟鸿、李昂、王振辉

54. 201810130188.X,一种网联智能能源计量结算方法,史建琦、郭欣、黄滟鸿、熊家文、毛侠

55. 201810130185.6,一种网联智能能源计量结算系统,史建琦、郭欣、黄滟鸿、熊家文、毛侠

56. 201810167496.X,一种结构化文本程序的自动化验证方法,史建琦、黄滟鸿、卜祥兴、熊家文、佘庆

57. 201810160216.2,一种基于中断控制流图的中断验证系统,史建琦、黄滟鸿、卜祥兴、熊家文、佘庆

58. 201810167489.X,一种结构化文本程序的自动化验证装置,史建琦、佘庆、黄滟鸿、郭欣、熊家文、毛侠

59. 201810160219.6,一种基于中断控制流图的中断验证方法,史建琦、佘庆、黄滟鸿、郭欣、熊家文、毛侠

60. 201810338428.5,一种基于区块链的能源网联监控方法及存储介质,毛侠、何积丰、史建琦、黄滟鸿、朱罡

61. 201810337908.X ,一种基于区块链的能源网联智能装置及系统,毛侠、何积丰、史建琦、黄滟鸿、朱罡

62. 201810189855.1,一种提高域名系统可用性的方法及系统, 黄滟鸿 熊家文 史建琦 何积丰 李昂

63. 201810189854.7,一种域名系统攻击检测方法、装置及系统,

64. 201810611535.0,一种可编程控制的通用总线接口转换方法,陈晶,史建琦,何积丰,黄滟鸿

65. 201810611556.2,一种可编程控制的通用总线接口转换系统,陈晶,史建琦,何积丰,黄滟鸿

66. 201810609281.9,可编程逻辑控制器编程语言转换系统,史建琦,黄滟鸿,何积丰,李昂,蔡方达

67. 201810609274.9,可编程逻辑控制器编程语言转换方法,史建琦,黄滟鸿,何积丰,李昂,蔡方达

68. 201810667143.6,一种基于中间语言的PLC程序验证系统,史建琦,黄滟鸿,何积丰,李昂,蔡方达

69. 201810667508.5,一种基于中间语言的PLC程序验证方法,史建琦,黄滟鸿,何积丰,李昂,蔡方达

70. 201810772287.8,一种基于IMCL模型的异构式多平台代码生成方法,黄滟鸿,史建琦,李炬,李昂,蔡方达

71. 201810776825.0,一种基于IMCL模型的异构式多平台代码生成系统,黄滟鸿,史建琦,李炬,李昂,蔡方达

72. 201810770780.6,一种复杂工业控制系统的实现方法,黄滟鸿,史建琦,李炬,李昂,蔡方达

73. 201810770767.0,一种复杂工业控制系统,黄滟鸿,史建琦,李炬,李昂,蔡方达

74. 201811132214.9,一种需求功能点智能识别系统 ,史建琦,李志辉,黄滟鸿,鲍钰,战云龙,孙文圣

75. 201811132200.7,一种需求功能点智能识别方法 ,史建琦,李志辉,黄滟鸿,鲍钰,战云龙,孙文圣

76. 201811133405.7,一种智能功能点识别的软件计价方法 ,史建琦,皮兴兴,黄滟鸿,鲍钰,孙文圣,战云龙

77. 201811133423.5,一种智能功能点识别的软件计价系统 ,史建琦,皮兴兴,黄滟鸿,鲍钰,孙文圣,战云龙

78. 201811133388.7,一种基于神经风格迁移的测试用例生成系统  ,史建琦,李志辉,黄滟鸿,蔡方达,王祥丰,金博

79. 201811132209.8,一种基于神经风格迁移的测试用例生成方法 ,史建琦,李志辉,黄滟鸿,蔡方达,王祥丰,金博

2019年度上海市科技进步奖《面向重大工业装备核心控制软件的安全可信保障技术及应用》 特等奖

2018年度上海市青年科技“启明星”人才