Personal homepage: https://sites.google.com/view/ronggu/home.
- Ph.D. of Computer Science, Mälardalen University, Sweden, 2017 - 2022.
- Master of Engineer in Software Engineering School, Xi'an Jiaotong University, China, 2010-2013.
- Bachelor in Software Engineering School, Xi'an Jiaotong University, China, 2006-2010.
Rong had been working as an embedded system engineer in a top avionic institute in China from 2013 - 2017. His work covers the embedded software development of the safety-critical systems deployed in aircrafts, trains, etc, as well as tools for system simulation, testing, and demonstration. He has a rich experience of model-based software engineering and the relevant methods and tools, e.g., SysML, AADL, Simulink, etc.
Rong's research is problem oriented and closely connected to real-world problems. He has worked with many industrial partners, e.g., Volvo Construction Equipment, and Volvo cars. His goal of the research is to synthesize correctness-guaranteed controllers for autonomous systems and the testers to find potential design errors in the early time of development by using his tools that are based on formal methods. His research interest is listed but not limited as follows:
- Formal modelling and verification of embedded systems (discrete models, hybrid models, etc.)
- Formal specification of requirements
- Machine Learning, Reinforcement Learning
- Controller synthesis of linear and nonlinear dynamic systems
- Tools I use: UPPAAL (SMC), UPPAAL Stratego. Tools I develop: MALTA, to be continued...
- Formal Modelling and Analysis of Embedded Systems, member, 2017 - now.
- Formal Methods Europe (FME), member, 2020 - now.
- Doctoral Student Council at MDH, member, 2019 - 2021.
- Community service as a reviewer: AST(2020), FMICS(2019), ISEC(2021), NFM(2020, 2021, 2022), SERENE(2018, 2019), TAP(2022), Journal of Robotics, IEEE Transactions on Intelligent Transportation Systems.
Rong is actively involved in supervising postgraduate students' thesis and teaching the following courses:
- DAV231: Development of Web Application (2017 - 2019)
- DVA218: Data Communication (2018 - now)
- DVA468: Catching Bugs by Formal Verification (2018 - now)
- DVA128: Program with Python (2022 - now)
- Embedded System II: a guest lecture (2021)
He has supervised the following Master thesis:
- Safety-Guaranteed Mission Planner for Autonomous Vehicles (2020)
Autonomous systems, such as self-driving cars, drones, and autonomous construction equipment, are safety-critical and thus are supposed to operate autonomously with very high dependability. My research mainly focuses on applying formal verification in the development of autonomous systems. Formal verification benefits finding design errors that are difficult to be discovered in the early phases of development or reappeared in the laboratory. With the help of formal verification, we can not only find bugs but also prove the absence of bugs in autonomous systems.
I am also working on providing advanced methods and tools to synthesize controllers of autonomous systems operating in a closed environment. Those controllers are generated automatically and are guaranteed to be correct in the sense that they must satisfy the requirements of the systems, e.g., never collide with any obstacles in the environment.
- MALTA has been published on GitHub (click here). The tool is for solving the pathfinding and task scheduling problems of multi-agent systems. The introduction video of the tool: click here. Co-authors of the tool: Afshin Ameri, Baran Çürüklü, and Eduard Baranov (from UCLouvain).
- MCRL (Model Checking + Reinforcement Learning) for mission planning of multi-agent systems is being integrated into UPPAAL Stratego through a collaboration with Aalborg University.
- June 2022 - I have defended my doctoral dissertation "Formal Methods for Scalable Synthesis and Verification of Autonomous Systems". The opponent of the defense was Professor Rajeev Alur, from the University of Pennsylvania.
- November 2021 - I have given a presentation in FM'21 (24th International Symposium of Formal Methods). The video of the presentation is online (click here).
- October 2021 - I have given a presentation in ISoLA2021 (10th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation). The video of the presentation is online (click here).
- May 2021 - I have given a presentation of my research for the MER 21 evaluation of MDH (click here).
- September 2020 - I have participated in the 25th International Conference on Formal Methods for Industrial Critical Systems (FMICS 2020) and given a presentation about our paper: Verifiable and Scalable Mission-Plan Synthesis for Multiple Autonomous Agents. This paper has honourably won the Best-paper Award. The presentation is available online (click here).
- June 2020 - I have attended the 14th Summer School on Modelling and Verification of Parallel Processes (MOVEP) and given a presentation about my research: Controller Synthesis and Verification for Multi-Agent Systems.
- June 2020 - I have defended my licentiate thesis: Automatic Model Generation and Scalable Verification for Autonomous Vehicles - Mission Planning and Collision Avoidance. The opponent of the defense was Professor Kim Larsen, from Aalborg University.
- April 2020 - I have participated in the 35th ACM/SIGAPP Symposium On Applied Computing (SAC 2020) and given a presentation about our paper: TAMAA: UPPAAL-based Mission Planning for Autonomous Agents. The presentation is available online (click here).
- November 7, 2019 - I have given a presentation about our research and tool (TAMAA) in the VCE/MDH Partnership Celebration, Eskilstuna, Sweden.
- June 10, 2019 - I have attended the 2019 Summer School on Cyber-Physical Systems in KTH, Stockholm, Sweden.
- May 9, 2019 - I have given a presentation at the 11th Annual NASA Formal Methods Symposium (NFM 2019) in Houston, USA - Towards a Two-layer Framework for Verifying Autonomous Vehicles.
- April 22, 2019 - I have attended the 12th IEEE Conference on Software Testing, Validation and Verification (ICST 2019) in Xi'an, China.
- Feb 14, 2019 - I have given a presentation at the workshop: Formal Verification - Secure SW Functions for Operating Autonomous Machine with Humans in VOLVO Construction Equipment.
- Aug 13, 2018 - I have attended the Marktoberdorf Summer School 2018.
- Jun 2, 2018 - I have given a presentation at the 6th FormaliSE 2018 (International Conference on Formal Methods in Software Engineering) about our paper: Formal Verification of an Autonomous Wheel Loader using Model Checking.
- Apr 25, 2018 - I have given a presentation about the formal verification of autonomous vehicles at DPAC summit 2018.
- Apr 9 - 13, 2018 - I have participated in the 11th ICST as a volunteer.
[Show all publications]
[Google Scholar author page] Latest publications:
Correctness-Guaranteed Strategy Synthesis and Compression for Multi-Agent Autonomous Systems
(Sep 2022) Rong Gu, Peter Jensen
, Cristina Seceleanu, Eduard Paul Enoiu, Kristina Lundqvist Science of Computer Programming (SCICO-223)
Formal Methods for Scalable Synthesis and Verification of Autonomous Systems
(May 2022) Rong Gu
Strategy Synthesis and Compression for Multi-Agent Autonomous Systems: A Correctness-Guaranteed Approach
(Apr 2022) Rong Gu, Peter Jensen
, Cristina Seceleanu, Eduard Paul Enoiu, Kristina Lundqvist
Mission Planning for Multiple Autonomous Agents under Complex Road Conditions: Model-Checking-Based Synthesis and Verification
(Apr 2022) Rong Gu, Eduard Baranov
, Afshin Ameri E., Eduard Paul Enoiu, Baran Çürüklü, Cristina Seceleanu, Axel Legay
, Kristina Lundqvist
Verifiable Strategy Synthesis for Multiple Autonomous Agents: A Scalable Approach
(Feb 2022) Rong Gu, Peter Jensen
, Danny Poulsen
, Cristina Seceleanu, Eduard Paul Enoiu, Kristina Lundqvist International Journal on Software Tools for Technology Transfer (STTT)
Model Checking Collision Avoidance of Nonlinear Autonomous Vehicle Models
(Nov 2021) Rong Gu, Cristina Seceleanu, Eduard Paul Enoiu, Kristina Lundqvist Formal Methods 2021 (FM'21)