郭建
软件工程学院??????


导航
个人资料
研究方向
开授课程
科研项目
学术成果
荣誉及奖励







个人资料
部门： 软件工程学院
毕业院校：
学位：
学历：
邮编：
联系电话： （021）**
传真： （021）**
电子邮箱： jguo@sei.ecnu.edu.cn
办公地址： 数学馆308
通讯地址： 上海市中山北路3663号华东师范大学计算机科学与软件工程学院

教育经历

工作经历

个人简介

社会兼职
中国计算机学会会员


研究方向
嵌入式系统开发与分析，主要包括汽车电子、多复用智能卡
嵌入式实时操作系统，
嵌入式系统、智能系统的建模、分析与验证
形式化方法


开授课程


科研项目


学术成果
英文论文：
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.** 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 Veri?cation 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.
中文论文
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。
专利：
6.“基于霍尔逻辑的嵌入式实时操作系统的自动化验证方法”，受理。
5.“一种针对源代码的运行时形式化验证方法及系统”，受理。
4.“一种操作系统规范形式化验证与测试方法”，受理号。
3.“一种汽车电子产品功能安全的保证及验证方法”，受理。
2.“汽车开放系统架构操作系统的分析和验证装置及其方法”，授理。
1.“一种多复用智能卡形式化建模与验证方法”，授权。
软件著作权：
7. 车载操作系统可调度性分析软件2018；
6. 基于切面的软件运行时验证与监视器生成软件，2017；
5. ISO26262汽车电子功能安全评估软件，2016；
4. 车载操作系统应用验证软件，2016；
3. TTCAN调度矩阵模型生成器软件， 2016；
2. pIML语?言仿真器软件，2014；
1.BPEL语言推理系统证明器，2014.

主持、参与项目：
12.自然科学基金委重点项目（**）大规模概率并发实时系统模型检验，2016年01月1日 -- 2020年12月31日，华师大负责人。
11. 核高基，工业互联网、物联网安全操作系统产业化及规模化应用（2017ZX**），2017年1月1日-2019年12月31日。
10.上海市科委项目：多行业复合应用智能IC卡安全机制与测评方法研究（编号：），2012-09-30至2014-09-30，主持人。
9.南京大学计算机软件新技术国家重点实验室开发项目（KFKT2011B26）“混合系统的形式化建模与验证的研究”2011.6-2013.6；
8.教育部软硬件协同设计工程中心开放项目‚“可信的软硬件协同设计”‚2011.7-2013.7；
7.上海市高可信计算重点实验室开放课题项目，“AUTOSAR规范下汽车电子通讯模块的验证方法研究”2011.11-2012.11；
6.公安部第三研究所开放课题：基于eID应用规范的形式化建模与分析，2012年6月-2013年12月；
5. 国家自然科学基金重大项目（**）“面向车联网的可信网络应用软件系统试验环境与示范应用”，2011年1月1日-2015年12月31日；
4.国家863计划（2012AA011205）“网构化软件可信评估技术与工具”，2012年1月1日-2014年12月31日；
3. 核高基（2009ZX01038-001-07）“核心电子器件、高端通用芯片及基础软件产品”的子课题“汽车电子系统可靠性分析和验证方法研究”，项目负责人：何积丰，2009年1月-2010年 12 月；
2.973项目（2011CB302904）：“物联网的基础理论与实践研究”的子课题“物联网可信软件设计理论与方法研究”，项目负责人,何积丰，主要参加者。2011年1 月1 日-2013 年8 月31 日；
1.国家自然科学基金委中丹合作项目（二期）信息物理融合系统的基础研究，2014年1月1日-2016年12月31日。



荣誉及奖励


招生信息














10 访问


相关教师