Rong Gu, Doctoral student
Personal homepage: https://sites.google.com/view/ronggu/home.
Education Background:
- 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.
Research:
In 2017, Rong started his PhD research, which is about controller synthesis and verification of autonomous systems. His research is closely connected to industrial partners, e.g., Volvo Construction Equipment. His goal is to enable the system designers to synthesize correctness-guaranteed controllers for their 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...
Community service as a reviewer: AST(2020), NFM(2020, 2021, 2022), FMICS(2019), SERENE(2018, 2019), ISEC(2021), Journal of Robotics.
- 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.
Teaching:
Rong is actively involved in supervising postgraduate students' thesis and teaching the following courses:
- DAV231: Development of Web Application
- DVA218: Data Communication
- DVA468: Catching Bugs by Formal Verification
- Embedded System II: a guest lecture
He has supervised the following Master thesis:
- Safety-Guaranteed Mission Planner for Autonomous Vehicles (2020)
Research topic:
In an attempt to increase productivity and the workers’ safety, the construction industry is moving towards autonomous construction sites, where various construction equipment operates without human intervention. Such systems are safety-critical and should operate autonomously with very high dependability. My research mainly focuses on applying formal verification in the development of autonomous systems. Formal verification benefits to find design errors that are difficult to be discovered or reappeared. I am also working on providing advanced methods and tools to synthesize path and mission plans for multiple autonomous vehicles operating in a closed environment. Those plans can also be simulated and analyzed by using our tools so that the planning conflicts and errors are not delayed to be discovered in practical prototypes or products.
Tools:
- 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.
Recent experience:
- 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. For more information on the thesis, please click here.
- 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.
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)
DPAC Newsletter Spring 2021 (Jun 2021) Kristina Lundqvist, Mikael Sjödin, Nandinbaatar Tsog, Saad Mubeen, Fredrik Bruhn, Jakob Danielsson, Marcus Jägemar, Tiberiu Seceleanu, Moris Behnam, Afshin Ameri E., Baran Çürüklü, Branko Miloradovic, Mikael Ekström, LanAnh Trinh, Rong Gu, Eduard Paul Enoiu, Cristina Seceleanu, Fereidoun Moradi, Sara Abbaspour Asadollah, Ali Sedaghatbaf, Aida Causevic, Marjan Sirjani, Carolyn Talcott
Formal Verification of Collision Avoidance for Nonlinear Autonomous Vehicle Models (Apr 2021) Rong Gu, Cristina Seceleanu, Eduard Paul Enoiu, Kristina Lundqvist
Probabilistic Mission Planning and Analysis for Multi-agent Systems (Oct 2020) Rong Gu, Eduard Paul Enoiu, Cristina Seceleanu, Kristina Lundqvist 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2020)
Verifiable and Scalable Mission-Plan Synthesis for Multiple Autonomous Agents (Sep 2020) Rong Gu, Eduard Paul Enoiu, Cristina Seceleanu, Kristina Lundqvist 25TH INTERNATIONAL CONFERENCE ON FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS (FMICS)
| Project Title | Status |
|---|---|
| DPAC - Dependable Platforms for Autonomous systems and Control | active |