郭建

中国计算机学会会员

    CCF嵌入式专委会

    CCF形式化专委会

嵌入式系统开发与分析，主要包括汽车电子、多复用智能卡

嵌入式实时操作系统，

嵌入式系统、智能系统的建模、分析与验证

形式化方法

本科生课程：

    嵌入式系统设计（国家一流课程（线上线下混合式教学））

    嵌入式系统设计实践

    嵌入式系统建模与规范

    操作系统

    软件工程数学（离散数学）

研究生课程：

    系统分析与验证

    软件分析与验证工具

科研项目

主持：

1. 自然科学基金委重点项目:

    大规模概率并发实时系统模型检验

2. 上海市科委科研计划项目：

    多行业复合应用智能IC卡安全机制与测评方法研究

3. 上海市科委重点项目：

    单元级测试数据设计与自动生成和代码动态缺陷发现技术

4. 上海市高可信计算重点实验室开放课题项目:

    AUTOSAR规范下汽车电子通讯模块的验证方法研究

5. 教育部软硬件协同设计工程中心开放项目:

    可信的软硬件协同设计

6. 南京大学计算机软件新技术国家重点实验室开发项目:

    混合系统的形式化建模与验证的研究

参与：

1. 国家863计划：

    网构化软件可信评估技术与工具

2. 国家自然科学基金委中丹合作项目：

    信息物理融合系统的基础研究

3. 973项目：

    物联网的基础理论与实践研究

4. 核高基：

    核心电子器件、高端通用芯片及基础软件产品

5. 核高基：

    国产汽车电子基础软件平台产品研制及产业化

6. 核高基：

    工业互联网、物联网安全操作系统产业化及规模化应用

教改项目

主持：

10. 2023年第二批国家级一流本科课程《嵌入式系统设计》（线上线下混合式教学）

9. 嵌入式系统设计，2021、2022年智慧树平台一流高校精品课程

8. 嵌入式系统设计，2021年华东师范大学大夏学堂优质示范课程

7. 嵌入式系统设计，2020年上海市高等学校一流本科课程（线上线下混合式课程）

6. 2019年上海高校课程思政重点改革领航课程“嵌入式系统设计”

5. “嵌入式系统设计”获得上海市2018年高校优质在线课程建设

4. 华东师范大学“2018年度在线开放课程建设项目”，嵌入式系统设计。

3. 2016年度华东师范大学在线教学平台课程建设项目，嵌入式系统规范与建模

2. 上海市精品课程项目“嵌入式系统设计”课程建设。2015年

1. 上海市市教委重点课程项目“嵌入式系统概论”课程建设，2011.7-2013.6。

参与：

1， 国家双语教学示范课程建设项目“软件工程数学”的课程建设，2015

英文论文：

25. Meiyi Dai1, Zhe Yang and Jian Guo, SuperDetector: A Framework for Performance Detection on Vulnerabilities of Smart Contracts，（EI）DMCIT 2022，2289 (2022) 012010

25. Yang, Z.; Dai, M.; Guo, Jian,  Formal Modeling and Verification of Smart Contracts with Spin. Electronics 2022, 11, 3091

24. YUQIAN GUAN , JIAN GUO , Adaptive Layered Segregated Fit Scheme for Dynamic Memory Allocation，Journal of Circuits, Systems, and Computers，vol.30, No.15,2150276(2021) 

23. YUQIAN GUAN  , JIAN GUO,  QIN LI  Formal Verification of a Hybrid IoT Operating System Model, IEEE Access,2021, vol.9: 59171-59183.Print ISSN: 2169-3536. Online ISSN: 2169-3536

22. Xiaoran Zhu , Min Zhang , Jian Guo, Xin Li, Huibiao Zhu, and Jifeng He Toward a Unified Executable Formal Automobile OS Kernel and Its Applications，IEEE TRANSACTIONS ON RELIABILITY, VOL. 68, NO. 3：1117-1133， SEPTEMBER 2019

21.Rongkun Yan and Jian Guo, “Timing Modeling and Analysis for AUTOSAR OS Schedule Tables”, Hase 2019：123-130

20. Jizheng Ding, Xiaoran Zhu, Jian Guo. “End-to-End Automated Verification for OS Kernels”, The 25th Asia-Pacific Software Engineering Conference (APSEC)：139-148

19.Xin Li, Jian Guo, Yongxin Zhao, Xiaoran Zhu. “Formal Modeling and Verifying the TTCAN Protocol from a Probabilistic Perspective”, Journal of Circuits, Systems and Computers. accepted.

18.  Xiaoran Zhu, Min Zhang, Jian Guo, Xin Li, Huibiao Zhu, Jifeng He. “Towards a unified executable formal automobile OS kernel and its applications”, IEEE Transactions on Reliability. DOI: 10.1109/TR.2018.2863744 Print ISSN: 0018-9529 Electronic ISSN: 1558-1721

17.Xiaoran Zhu,  Yuanmin Xu,  Xin Li, Jian Guo,  Huibiao Zhu, Phan Cong Vinh, Formal Analysis of the PKMv3 Protocol, Mobile Networks and Applications 2017，21（1）,44-56.

16.Xiaoran Zhu, Yuanmin Xu, Jian Guo, Xi Wu, Huibiao Zhu, Weikai Miao. Formal Verification of PKMv3 Protocol Using DT-Spin, TASE Proc 2015: 9th IEEE International Symposium on Theoretical Aspects of Software Engineering, pp.71-78, IEEE Computer Society,11-13 Sep. 2015 Nanjing, JiangsuChina.

15.Tang Yiting, Wu Xi, Zhu Huibiao, Guo Jian. Formalization and Verification of REST Architecture in Viewpoints. Proc. HASE 2015: 16th IEEE International Symposium on High Assurance Systems Engineering, IEEE Computer Society, pp. 197~206, 8-10 January, 2015, Florida, USA

14.Xin Li,  Yanhong Huang, Jianqi Shi, Jian Guo, Huibiao Zhu, Yuanmin Xu, pIML - An Interrupt Program Modelling Language for Real-Time and Embedded Systems, APSEC 2014,p85-92.

13.Qin wen Ran,Xi Wu, Xin Li, Jianqi Shi, Jian Guo, and Huibiao Zhu  Modeling and Verifying the TTCAN Protocol Using Timed CSP, TASE Proc 2014: 8th IEEE International Symposium on Theoretical Aspects of Software Engineering, pp. 90-97, IEEE Computer Society,1-3 July 2014 Changsha, Hunan, China.

12. 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，International Journal on Software Tools for Technology Transfer: Volume 16, Issue 4 (2014), Page 339-361

11. Ting Yuan, Yiting Tang, Xi Wu, Yue Zhang，Huibiao Zhu, Jian Guo, Formalization and Verification of REST on HTTP Using CSP, This paper is electronically published journal in Electronic Notes in Theoretical Computer Science Volume 309, 22 December 2014, Pages 75-93 Proceedings of the Sixth International Workshop on Harnessing Theories for Tool Support for Software(TTSS) .

10.Can Pan, Jian Guo, Longfei Zhu，Jianqi Shi, Huibiao Zhu, Xinyun Zhou, Modeling and Verification of CAN Bus with Application Layer using UPPAAL, This paper is electronically published journal in Electronic Notes in Theoretical Computer Science Volume 309, 22 December 2014, Pages 31–49. Proceedings of the Sixth International Workshop on Harnessing Theories for Tool Support for Software(TTSS)

9.Yunhui Peng, Yanhong Huang, Ting Su, Jian Guo, Modeling and Verification of AUTOSAR OS and EMS Application, TASE Proc 2013: 7th IEEE International Symposium on Theoretical Aspects of Software Engineering, pp. 37-44, IEEE Computer Society,1-3 July 2013 Birmingham, United Kingdom.

8.Fang Huixing, Guo Jian, Zhu Huibiao, Shi Jianqi. Formal Verification and Simulation: Co-Verification for Subway Control Systems. Proc. TASE 2012: 6th IEEE International Symposium on Theoretical Aspects of Software Engineering, pp. 145-152, IEEE Computer Society, 4-6 July 2012, Beijing, China

7. Shi Jianqi, Zhu Longfei, Huang Yanhong, Guo Jian, Zhu Huibiao, Fang Huixing, and Ye Xin. Binary Code Level Verification for Interrupt Safety Properties of Real-Time Operating System.. Proc. TASE 2012: 6th IEEE International Symposium on Theoretical Aspects of Software Engineering, pp. 223-226, IEEE Computer Society, 4-6 July 2012,Beijing, China

6.Shi Jianqi, Zhu Longfei, Fang Huixing, Guo Jian, Zhu Huibiao, and Ye Xin. xBIL–A Hardware Resource Oriented Binary Intermediate Language. Proc. ICECCS 2012: 17th IEEE International Conference on Engineering of Complex Computer Systems, pp. 211-219, IEEE Computer Society, 18-20 July 2012,Paris, France

5.Wen Su，Fan Yang，Xiaofeng Wu,  Jian Guo,    Huibiao Zhu，Formal Approaches to Mode Conversion and Positioning for Vehicle System，2011 35th IEEE Annual Computer Software and Applications Conference Workshops，415-421.

4.Zhou Jiaming, Guo Jian, Song fu, Integrating the B-method into PVS, International Conference on Information Engineering and Computer Science, wuhan, China, 2009 vol(4): 2626-2629.

3.Guo Jian, Han Jungang, Symbolic Checking for Three valued logic, International conference on communications and mobile computing, CMC2009, vol(3):401-405.

2. Jian Guo, Han Jungang, Jin Naiyong Witness And Counter-example on 3-valued Model Checking, ICNC2008，vol(2):633-637.

1.Jian Guo, Jungang Han, Hongli Yang, Bo Wang, Model Checking with “X” Value Based on PSL, IEEE SUPPORT ICEMI07, I,P556-562.

中文编著：

1. 郭建、王高翃、赵涌鑫，蒲戈光，基于ISO26262的汽车电子功能安全：方法与应用，出版日期：2021.6，机械工业出版社，ISBN：978-7-111-68067-3 

中文论文：

12.董星河，郭建，基于在线模型检验技术的微内核验证，微纳电子与智能制造，2020（2）1：102-109 

11.郭建, 丁继政, 朱晓冉. 嵌入式实时操作系统内核混合代码的自动化验证框架[J]. 软件学报, 2020, 31(5): 1353-1373

10.李青，朱晓冉，郭建， AUTOSAR OS存储保护机制的形式化验证框架，计算机工程，2017， Vol. 43 (1): 79-85

9.徐骏,王玲,徐立华,郭建,朱惠彪.ProMiner:系统性质驱动的双向一致性检验框架.软件学报,2016,27(7)：1757−1771.

8.章玥，郭建，朱晓冉，基于模型的开发方法在多应用智能卡中的应用，信息网络安全，2013（156）：75-79。

7.章玥，郭建，朱晓冉等.基于Event-B 方法的多应用智能卡的建模与开发[J]. 计算机工程与科学, 2014,36(10): 1943-1951。

6.郭建，韩俊刚，三值逻辑证明系统及正例与反例的提取，2011.7，《计算机辅助设计与图形学学报》，vol23(7);1270:1279, 2011

5.郭建，韩俊岗．基于PSL的FIFO的验证．第五届中国测试学术会议．2008年，5月．295-289。

4. 郭建  LTL公式到自动机的转换，计算机科学，2008（7）：241-244。

3. 郭建  模型检验中对CTL公式的空属性探测，西安电子科技大学学报，2007，vol.34(5),p794-798.

2. 郭建基于不完全Kripke结构三值逻辑的模型检验，计算机科学，2006(3): 263-266.

1.郭建，基于模态转移系统的三值逻辑模型检验，计算机辅助设计几图形学学报，2006, 18(6)：881-884。

教材：

1.郭建等，嵌入式系统设计基础及应用——基于ARM Cortex-M4微处理器，北京：清华大学出版社，2022. ISBN：978-7-302-59530-4

2.曹喜信，郭建等，嵌入式系统设计实验教程，北京：清华大学出版社，2022. ISBN：978-7-302-59385-0

教改论文：

4.郭建，蒲戈光，缪炜凯，半翻转课堂的混合教学法-结合“嵌入式系统设计”教学的思考，计算机教育，2021. 9， v321(9):123-132

3.郭建、蒲戈光，半翻转课堂的嵌入式系统设计课程混合式教学模式，计算机教育，2021.8,v320(8):157-160

2.郭建，章玥，《嵌入式系统概论》课程教学改革与实践，第三届全国高校软件工程专业教育年会，《计算机工程与科学》,2011，Vol33（A1）：19：22.

1.朱惠彪，郭建，《软件工程数学》课程双语教学改革与实践，《南京大学学报》增刊，2009，vol(45):34-38.

授权专利： 

13. “一种实时操作系统内存管理算法性能测试方法及系统”，授权时间：2022.10.25

12. “基于内存回收方案的非阻塞算法的形式化验证方法”，授权时间：2022.7.8

11. “一种ROS底层通讯机制的形式化建模与验证方法”，授权时间：2023.6.9

10. “一种基于中间格式及SMT 技术的微内核IPC 验证方法”, 授权时间：2023.2.17

9. “利用在线模型检验的嵌入式实时操作系统验证方法及系统”，授权时间：2023.3.31

8. “一种实时操作系统内存管理算法性能测试方法及系统” ，授权时间：2022.10.25

7. “基于边界模型检测技术的微内核操作系统接口的形式化验证方法”，授权时间：2022.7.26

6. “一种基于形式化规范的服务总线微内核框架设计方法”，授权时间：2022.7.26

5.“一种汽车电子产品功能安全的保证及验证方法”，授权时间：2022.4.5

4.“基于霍尔逻辑的嵌入式实时操作系统的自动化验证方法”，授权时间：2021.7.27

3.“一种针对源代码的运行时形式化验证方法及系统”，授权时间：2018.3.8

2. “一种操作系统规范形式化验证与测试方法”，授权时间：2018.3.5

1.“一种多复用智能卡形式化建模与验证方法”，授权时间：2013.10.25

软件著作权：

13．ROS安全性测试工具软件2022

12．调度算法的在线模拟软件2021

11．基于行为驱动开发的测试软件2020

10．面向微内核API验证的中间代码转换2019

9．嵌入式操作系统即时模型检验软件2019

8．基于ESB总线的异构系统通讯软件2019  

7. 车载操作系统可调度性分析软件2018；

6. 基于切面的软件运行时验证与监视器生成软件，2017；

5. ISO26262汽车电子功能安全评估软件，2016；

4. 车载操作系统应用验证软件，2016；

3. TTCAN调度矩阵模型生成器软件， 2016；

2. pIML语⾔言仿真器软件，2014；

1.BPEL语言推理系统证明器，2014.

科研获奖：

1. 2020年4月，上海市科技进步奖特等奖：面向重大工业装备核心控制软件的安全可信保障技术与应用，（5/15）

2. 2018年教育部高等学校科学研究优秀成果奖（科学技术）技术发明一等奖：强防护环境下持续性共计的构建和追踪溯源关键技术及应用。（5/6）

3. 2019年，上海科技进步二等奖：面向高端装备的安全嵌入式基础软件，（5/10）

教学获奖：

1. 2018年，国家教学成果奖二等奖（9/11）

2. 2017年，上海市教学成果一等奖（8/10）

3. 2018年，华东师范大学教学成果一等奖(8/10)

4. 2022年，华东师范大学教学成果二等奖（1/3）

指导学生获奖：

1. 2014年指导学生参加美国大学生数学建模竞赛，获得一等奖。

2. 2015年指导学生参加美国大学生数学建模竞赛，获得二等奖一项、三等奖各二项

3. 2018年指导学生获得美国大学生数学建模竞赛二等奖

4. 2021全国大学生系统能力大赛操作系统设计优胜奖