Rong Gu, Ph.D.
Postdoc at Mälardalen University, Sweden
Office: U2-201, Västerås Campus
Work phone: +46(0)736621483
Email: rong.gu at mdu.se
Official page: http://www.es.mdh.se/staff/3552-Rong_Gu
CV: download
Selected Presentations
LiVe'24 - Integrating the Power of Machine Learning and Model Checking in Safety-Critical Systems
FM'21 - Model Checking Collision Avoidance of Nonlinear Autonomous Vehicles
FMICS 2020 - Verifiable and Scalable Mission-Plan Synthesis for Autonomous Agents
Selected Publications
FORTE'24: Guess and then Check: Controller Synthesis for Safe and Secure Cyber-Physical Systems. R Gu, Z Moezkarimi, M Sirjani. [BibTex][website]
LiVe'24: Integrating the Power of Machine Learning and Model Checking in Safety-Critical Systems. R Gu. [BibTex][PDF]
FM'24: Journal-first paper: Correctness-Guaranteed Strategy Synthesis and Compression for Multi-Agent Autonomous Systems.
AISoLA'23: Studying Formal Models Using ChatGPT. P Backeman, R Gu, F Lorber. To appear.
FMICS'23: Pattern-Based Verification of ROS 2 Nodes Using UPPAAL. L Dust, R Gu, C Seceleanu, M Ekström, S Mubeen. [website]
ETFA'23: Experimental Evaluation of Callback Behavior in ROS 2 Executors. Lukas Dust, Emil Persson, Mikael Ekström, Saad Mubeen, Cristina Seceleanu, Rong Gu. [website]
QUATIC'23: Journal-first paper: Correctness-Guaranteed Strategy Synthesis and Compression for Multi-Agent Autonomous Systems.
A-MOST'23: Model-Based Policy Synthesis and Test-Case Generation for Autonomous Systems. R Gu, E Enoiu. [BibTex][PDF][website].
Science of Computer Programming, 2022, vol. 224: Correctness-Guaranteed Strategy Synthesis and Compression for Multi-Agent Autonomous Systems. R Gu, P Jensen, C Seceleanu, E Enoiu, K Lundqvist. [BibTex][PDF].
Doctoral Dissertation: Formal Methods for Scalable Synthesis and Verification of Autonomous Systems - Mission Planning and Collision Avoidance. R Gu. [BixTex][PDF]
Software Tools for Technology Transfer, 2022, vol.24: Verifiable Strategy Synthesis for Multiple Autonomous Agents: A Scalable Approach. R Gu, P Jensen, D Poulsen, C Seceleanu, E Enoiu, K Lundqvist. [BibTex][PDF].
FM'21: Model Checking Collision Avoidance of Nonlinear Autonomous Vehicles. R Gu, C Seceleanu, E Enoiu, K Lundqvist. [BibTex] [PDF].
ISoLA'21: Probabilistic Mission Planning and Analysis for Multi-Agent Systems. R Gu, E Enoiu, C Seceleanu, K Lundqvist. [BibTex] [PDF].
FMICS'20: Verifiable and Scalable Mission-Plan Synthesis for Autonomous Agents. R Gu, E Enoiu, C Seceleanu, K Lundqvist. Best-paper Award. [BibTex] [PDF].
SAC'20: TAMAA: UPPAAL-based Mission Planning for Autonomous Agents. R Gu, E Enoiu, C Seceleanu. [BibTex] [PDF].
NFM'19: Towards a Two-Layer Framework for Verifying Autonomous Vehicles. R Gu, R Marinescu, C Seceleanu, K Lundqvist. [BibTex] [PDF].
FormaliSE'18: Formal Verification of an Autonomous Wheel Loader by Model Checking. R Gu, R Marinescu, C Seceleanu, K Lundqvist. [BibTex] [PDF].
Selected Tools
MALTA: mission planning of autonomous agents
GitHub: https://github.com/rgu01/MALTA
The tool is open for extension. If you have your own algorithms for pathfinding, task scheduling, and collision avoidance, please have a try!
Contact "rong.gu at mdu.se" for further information.
Research Profile
Research Description
My research fields are formal methods, software engineering, and machine learning. I have been studying the combination of machine learning with formal methods in the domain of autonomous systems. Autonomous systems can move and execute tasks within a confined environment, without or with a little human intervention. As they often work alongside humans, e.g., self-driving cars, the guarantee of their safety requirement is highly evaluated. Machine learning bears the promise of letting machines learn by themselves given enough training data. However, machine learning has no guarantee of correctness, safety, and security. My research aims at solving these problems with the support of formal methods, which are based on mathematics and well-known for providing rigorous analysis of complex systems.
Specifically, I use reinforcement learning for training autonomous systems, such as motion planning, and model checking (e.g., UPPAAL) for verification. I also explore the usage of generative AI, such as ChatGPT, in facilitating the work of requirement engineering.
Academic Activities
Community service as a reviewer/sub-reviewer: FM Symposium, AST, NFM, FMICS, SERENE, ISEC, Journal of Robotics, IEEE Transactions on Intelligent Transportation Systems, Journal of Supercomputing, etc.
Organizing conferences/workshops: ICST 2018 (Volunteer), ECBS 2023 (Tool Demo Chair), MODELS 2023 (Volunteer).
Collaborations with Industry
My doctoral study is problem-oriented and strongly connected to the industry. My project, DPAC (Dependable Platforms for Autonomous Systems and Control), involves several import industry players in Sweden, including VOLVO Construction Equipment, ABB, etc. We have annual summits to communicate our thoughts, and workshops every once in a while to let us, the academic researchers, introduce the state-of-the-art methodologies and seek effective combinations with their technologies.
Teaching Profile
Teaching:
PhD course: Formal Methods (to be announced)
Teaching assistant:
Catching Bugs by Formal Verification (2018 - now)
Development of Web Application (2017 - 2019)
Data Communication (2018 - now)
Programming with Python (2022 - 2023)
Lecture:
Guest lecturer of course: Embedded Systems II. 2021 - now.
Supervision:
Supervisor of Bachelor theses.
Model Checked Reinforcement Learning For Multi-Agent Planning. 2023.
Synthesis and Verification of Neural Networks by Using UPPAAL. 2023.
Supervisor of Master theses.
Overcoming the ambiguity and inconsistency of requirements by using generative AI. 2024.
Safety-Guaranteed Mission Planner for Autonomous Vehicles. 2020.
Co-supervisor of PhD students