王国辉 博士

高级实验师,硕士生导师

永利官网 yl9193永利

地址：北京市海淀区西三环北路56号323办公室

邮编：100048

Email：ghwang(at)cnu(dot)edu(dot)cn

基本信息

      王国辉，理学博士，高级实验师，硕士生导师。2011年加入yl9193永利。研究领域为形式化验证与高可靠性嵌入式系统，主要包括机器人机构学、运动学及动力学理论的高阶逻辑定理证明，苛刻环境下高可靠电子系统，新型存储系统优化。研究成果包括在JAR、FAOC、TC等国际顶级学术会议和期刊发表论文10余篇，获得国家授权发明专利9项，主持或参与国家自然科学基金，国家重点研发计划，JW科技创新特区项目等多个国家级和省部级项目。

 

研究兴趣

形式化验证，高可靠嵌入式系统。

 

教育经历

2013.09 – 2020.06，永利官网，数学科学学院，理学博士

2010.03 – 2011.03，香港理工大学，电子计算学系，研究助理

2008.09 – 2011.06，永利官网，yl9193永利，工学硕士

2003.09 – 2007.06，重庆理工大学，电子信息与自动化学院，工学学士

科研项目

1、[主持]国家自然科学基金面上项目，哈密顿动力学的形式化及其在协作机器人验证中的应用，2023/01-2026/12

2、[参与]国家自然科学基金面上项目，形式模型驱动的人机协作机器人设计与验证方法研究，2019/01-2022/12

3、[参与] JW科技创新特区项目，机器人运动学形式化建模理论，2019/03-2021/02

4、[参与]国家自然科学基金面上项目，复杂路况下自动驾驶传感器及关键技术研究，2018/01-2021/12

5、[主持]横向项目，医学影像特征识别算法开发，2018/10-2019/4

6、[参与]国家重点研发计划“公共安全风险防控与应急技术装备”重点专项子课题，地面伤员抢运机器人系统集成研究与实现，2017/07-2020/06

代表论文

[1]. Guohui Wang, Shanyan Chen, Yong Guan, Zhiping Shi, Ximeng Li, Jingzhi Zhang. Formalization of the inverse kinematics of three-fingered dexterous hand. Journal of Logical and Algebraic Methods in Programming. Volume 133, June 2023, 100861. (SCI)

[2]. Zhengang Chen, Guohui Wang∗, Zhiping Shi, Yong Guan, Tianyu Wang. Region-based Flash Caching with Joint Latency and Lifetime Optimization in Hybrid SMR Storage Systems. 2023 Design, Automation & Test in Europe Conference (DATE 2023). 17-19 April 2023. Antwerp, Belgium. (CCF-B,SCI)

[3]. Ximeng Li, Qianying Zhang, Guohui Wang, Zhiping Shi, Yong Guan. A unified proof technique for verifying program correctness with big-step semantics. Journal of Systems Architecture, Volume 136,2023,102820. (CCF-B,SCI)

[4]. 陈善言,关永,施智平,王国辉.机器人碰撞检测方法形式化.软件学报,2022,33(6):2246-2263

[5]. 尹晓娜,王国辉*,施智平,关永,张倩颖,张景芝. 群机器人区域覆盖算法高阶逻辑建模与验证. 小型微型计算机系统, 2022 Vol. 43 (3): 475-482

[6]. 王畅,王国辉*,施智平,关永,张倩颖,邵振洲. 协作机器人逆运动学形式化建模与验证. 小型微型计算机系统, 2021, 42(7): 1353-1359.

[7]. Guan Yong, Zhang Jingzhi, Wang Guohui*. et al. Formalization of Euler–Lagrange Equation Set Based on Variational Calculus in HOL Light. Journal of Automated Reasoning， volume 65, pages1–29(2021).(CCF-B,SCI)

[8]. 王国辉，许京然，刘永梅，施智平*，关永. 摄动开普勒问题形式化建模与验证. 小型微型计算机系统 2020 Vol. 41 (2): 440-444

[9]. 陈琦,王国辉*,张倩颖,施智平,陈善言,关永. 平面并联机构的形式化建模与验证. 小型微型计算机系统.2020 Vol. 41 (5): 925-931 

[10]. Chen Shanyan, Wang Guohui*, Li Ximeng. et al. Formalization of Camera Pose Estimation Algorithm based on Rodrigues Formula. Formal Aspects of Computing volume 32, pages417–437(2020). (CCF-B,SCI)

[11]. Jingzhi Zhang, Guohui Wang*, Zhiping Shi, Yong Guan, Yongdong Li. Formalization of functional variation in HOL Light, Journal of Logical and Algebraic Methods in Programming, Volume 106, 2019, Pages 29-38. SCI)

[12]. Nie Yuhan,Shi Zhiping, Wu Aixuan, Li Ximeng, Wang Guohui and Guan Yong. A HOL Theory of the Differential for Matrix Functions. 2019 13th International Symposium on Theoretical Aspects of Software Engineering.(CCF-C)

[13]. Guohui Wang, Yong Guan, Zhiping Shi, Qianying Zhang, Xiaojuan Li, Yongdong Li: Formalization of Symplectic Geometry in HOL-Light. The 20th International Conference on Formal Engineering Methods: 270-283. (CCF-C)

[14]. 赵荣波,施智平,关永,邵振洲,王国辉,吴立峰.基于旋量理论和代数消元6R机器人逆解算法.传感器与微系统, 2018, 37(12): 114-117+121.

[15]. Zhao Rongbo, Shi Zhiping, Guan Yong, Shao Zhenzhou, Zhang Qianying, & Wang Guohui. Inverse kinematic solution of 6R robot manipulators based on screw theory and the Paden–Kahan subproblem. International Journal of Advanced Robotic Systems:15(6). (SCI)

[16]. Yong Guan, Guohui Wang, Chenlin Ma, Renhai Chen, Yi Wang*, Zili Shao, A Block-Level Log-Block Management Scheme for MLC NAND Flash Memory Storage Systems, IEEE Transactions on Computers, vol. 66, pp. 1464-1477, Sept. 2017.(SCI)

[17]. Wang, Guohui， Guan, Yong， Wang, Yi， Shao, Zili； Energy-aware assignment and scheduling for hybrid main memory in embedded systems，Computing，March 2016, Volume 98, Issue 3, pp 279-301.(SCI)

[18]. Jingzhi Li, Guohui Wang*, Yong Guan, Lifeng Wu, Xiaojuan Li, Failure prediction of ultracapacitor stack using fuzzy inference system, Engineering Review, vol.35, no.1, May.2015.

[19]. Yong Guan, Guohui Wang, Yi Wang, Renhai Chen, Zili Shao, BLog: block-level log-block management for NAND flash memorystorage systems, ACM SIGPLAN Notices，Volume 48 Issue 5，May 2013, Pages 111-120.(SCI)

[20]. Guohui Wang, Zhiquan Dai, Yong Guan, Pengfei Dong, and Lifeng Wu, Power Management of Hybrid Power Systems with Li-Fe Batteries and Supercapacitors for Mobile Robots, Advances in Mechanical Engineering, vol. 2014, Article ID 270537, 11 pages, 2014.(SCI)

专著

1、施智平，王国辉，关永，王瑞. 哈密顿力学理论的形式化与机器人动力学形式化分析. 北京：科学出版社. 2022.09 [ISBN: 9787030532046]

授权专利

1. 施智平;王国辉;关永;陈琦;张倩颖;李希萌;邵振洲. 平面并联机构形式化验证的方法及装置. 专利号：ZL 2019 1 1032684.2 申请日：2019-10-28 授权日：2023-03-31

2. 王国辉;关永;施智平;聂玉涵;张倩颖;李希萌;邵振洲. 机械臂稳定性形式化分析方法、装置、设备及存储介质. 专利号：ZL 2019 1 1067971.7 申请日：2019-11-04 授权日：2023-04-14

3. 施智平，赵荣波，关永，张倩颖，王国辉，邵振洲，王瑞，李晓娟. 串联机器人的关节旋转角度确定方法及装置. 专利号：ZL 2018 1 0195251.8 授权日期：2022-04-22 

4. 王国辉，施智平，关永，陈善言，王畅，张倩颖，邵振洲，王瑞，李晓娟，李希萌. 三指机器人灵巧手逆运动学的形式化验证方法及电子设备. 专利号：ZL 2021 1 0719629.1 申请日：2021-06-28 授权日：2022-07-05

5. 张倩颖, 张美玉, 施智平, 关永, 李晓娟, 王瑞, 王国辉, 李希萌，基于内存加密保障可信执行环境抗物理攻击的方法及系统，ZL201910979558.1，授权日：2022.4.19，中国

6. 施智平, 赵荣波, 关永, 张倩颖, 王国辉, 邵振洲, 王瑞, 李晓娟, 6自由度串联机器人的关节旋转角度确定方法及装置, ZL201810195262.6

7. 李晓娟, 关永, 李艳春, 王瑞, 施智平, 张倩颖, 谈金东, 邵振洲, 张杰, 王国辉, 刘永梅, 吴敏华, 一种用于机器人分布式控制系统的形式建模方法及装置, ZL201611197597.9

8. 关永，周松文，吴立锋，潘巍，王国辉，一种DC-DC电源系统故障检测与预测方法，ZL201210088086.9

9. 吴立锋，关永，郑学艳，李晓娟，王国辉，潘巍，郑宇，电源功率模块劣化状态在线判断方法，ZL201210516838.7

承担课程

计算机组成原理实验、可编程逻辑器件与HDL、数字系统综合设计实践

获奖情况

1、2020年，第十四届北京发明创新大赛铜奖，废水处理技术评价方法及系统

2、2012年，北京市科学技术二等奖，SpaceWire形式化验证和SpaceFibre的样机研制

公司产品

公司产品方向： 机器人运动学、动力学定理证明/新型存储系统优化

欢迎对上述方向感兴趣的同学攻读研究生，也欢迎高年级本科生加入。