https://www.mdu.se/

mdu.sePublications
Change search
Link to record
Permanent link

Direct link
Gu, Rong
Publications (10 of 25) Show all publications
Dust, L., Ekström, M., Gu, R., Mubeen, S. & Seceleanu, C. (2024). A Model-Based Methodology for Automated Verification of ROS 2 Systems. In: Proceedings - 2024 IEEE/ACM 6th International Workshop on Robotics Software Engineering, RoSE 2024: . Paper presented at 6th International Workshop on Robotics Software Engineering, RoSE 2024, co-located with the 46th International Conference on SoftwareLisbon15 April 2024 (pp. 35-42).
Open this publication in new window or tab >>A Model-Based Methodology for Automated Verification of ROS 2 Systems
Show others...
2024 (English)In: Proceedings - 2024 IEEE/ACM 6th International Workshop on Robotics Software Engineering, RoSE 2024, 2024, p. 35-42Conference paper, Published paper (Refereed)
Abstract [en]

To simplify the formal verification of ROS 2-based applications, in this paper, we propose a novel approach to the automation of their model-based verification using model-driven engineering techniques. We propose a methodology starting with ROS 2 execution traces, generated by ROS2_tracing and using models and model transformations in Eclipse to automatically initialize pre-defined formal model templates in UPPAAL, with system parameters. While the methodology targets the simplification of formal verification for robotics developers as users, the implementation is at an early stage and the toolchain is not fully implemented and evaluated. Hence, this paper targets tool developers and researchers to give a first overview of the underlying idea of automating ROS 2 verification.

Hence, we propose a toolchain that supports verification of implemented and conceptual ROS 2 systems, as well as iterative verification of timing and scheduling parameters. We propose using four different model representations, based on the ROS2_tracing output and self-designed Eclipse Ecore metamodels to model the system from a structural and verification perspective. The different model representations allow traceability throughout the modeling and verification process.Last, an initial proof of concept is implemented containing the core elements of the proposed toolchain and validated given a small ROS 2 system. 

National Category
Robotics and automation Embedded Systems Computer Sciences
Identifiers
urn:nbn:se:mdh:diva-67506 (URN)10.1145/3643663.3643970 (DOI)001285454300006 ()2-s2.0-85200922593 (Scopus ID)9798400705663 (ISBN)
Conference
6th International Workshop on Robotics Software Engineering, RoSE 2024, co-located with the 46th International Conference on SoftwareLisbon15 April 2024
Available from: 2024-06-14 Created: 2024-06-14 Last updated: 2025-02-05Bibliographically approved
Gu, R., Seceleanu, T., Xiong, N. & Naeem, M. (2024). A Service-Oriented Digital Twin Framework for Dynamic and Robust Distributed Systems. In: Proceedings - 2024 IEEE International Conference on Software Services Engineering, SSE 2024: . Paper presented at 2nd IEEE International Conference on Software Services Engineering, SSE 2024 Shenzhen, 7 July 2024 through 13 July 2024 (pp. 66-73). Institute of Electrical and Electronics Engineers Inc.
Open this publication in new window or tab >>A Service-Oriented Digital Twin Framework for Dynamic and Robust Distributed Systems
2024 (English)In: Proceedings - 2024 IEEE International Conference on Software Services Engineering, SSE 2024, Institute of Electrical and Electronics Engineers Inc. , 2024, p. 66-73Conference paper, Published paper (Refereed)
Abstract [en]

Digital Twins (DTs) are virtual representations of physical products in many dimensions, such as geometry and behaviour. As a backbone of Industry 4.0, DTs help interpret and even predict the behaviour of physical processes, provide a virtual testbed for maintenance and upgrade, and enable automatic decision-making supported by artificial intelligence. Despite the promising future, challenges exist, such as the absence of a framework that facilitates the development and application of DTs in industrial contexts. We propose a service-oriented architecture (SOA) DT framework for dynamic and robust distributed systems. The framework contains two types of services. One includes the services provided to the users and is supported by an orchestration mechanism to ensure a quality of service (QoS). The other one refers to the common functions of all DTs. Further, we describe the DT-based decision-making enabled by our QoS-oriented learning of the framework and a Hoare-logic-based verification of QoS. 

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers Inc., 2024
Keywords
Digital Twins, Formal verification, Machine learning, SOA, System design, Adversarial machine learning, Decisions makings, Distributed systems, Machine-learning, Physical process, Physical products, Quality-of-service, Service Oriented, Soa (serviceoriented architecture), Virtual representations, Virtual testbeds, Service oriented architecture (SOA)
National Category
Computer Sciences
Identifiers
urn:nbn:se:mdh:diva-68719 (URN)10.1109/SSE62657.2024.00021 (DOI)001331809000008 ()2-s2.0-85205543259 (Scopus ID)9798350368512 (ISBN)
Conference
2nd IEEE International Conference on Software Services Engineering, SSE 2024 Shenzhen, 7 July 2024 through 13 July 2024
Available from: 2024-10-16 Created: 2024-10-16 Last updated: 2024-11-27Bibliographically approved
Naeem, M., Gu, R., Seceleanu, C., Guldstrand Larsen, K., Nielsen, B. & Albano, M. (2024). Energy-Efficient Motion Planning for Autonomous Vehicles Using Uppaal  Stratego. In: Theoretical Aspects of Software Engineering. TASE 2024. Lecture Notes in Computer Science.: . Paper presented at Theoretical Aspects of Software Engineering. TASE 2024 (pp. 356-373). Springer, 14777
Open this publication in new window or tab >>Energy-Efficient Motion Planning for Autonomous Vehicles Using Uppaal  Stratego
Show others...
2024 (English)In: Theoretical Aspects of Software Engineering. TASE 2024. Lecture Notes in Computer Science., Springer, 2024, Vol. 14777, p. 356-373Conference paper, Published paper (Refereed)
Abstract [en]

Energy-efficient motion planning for autonomous battery-powered vehicles is crucial to increase safety and efficiency by avoiding frequent battery recharge. This paper proposes algorithms for synthesizing energy- and time-efficient motion plans for battery-powered autonomous vehicles. We use stochastic hybrid games to model an appropriate abstraction of the autonomous vehicle and the environment. Based on the model, we synthesize energy- and time-efficient motion plans using Q-learning in Uppaal  Stratego. Via experiments, we show that pure Q-learning is insufficient when the problem becomes complex, e.g., Motion Planning (MOP) in large environments. To address this issue, we propose Concatenated Motion Planning (CoMOP), which divides the environment into several regions, synthesizes a motion plan in each region and concatenates the local plans into an entire motion plan for the whole environment. CoMOP enhances the applicability of Q-learning to large and complex environments, reduces synthesis time, and provides efficient navigation and precise motion plans. We conduct experiments with our approaches in an industrial use case. The results show that CoMOP outperforms MOP regarding synthesis time and the ability to deal with complex models. Moreover, we compare the energy- and time-efficient strategies and visualize their differences on different terrains.

Place, publisher, year, edition, pages
Springer, 2024
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:mdh:diva-69378 (URN)10.1007/978-3-031-64626-3_21 (DOI)001315662800021 ()9783031646256 (ISBN)9783031646263 (ISBN)
Conference
Theoretical Aspects of Software Engineering. TASE 2024
Available from: 2024-12-09 Created: 2024-12-09 Last updated: 2024-12-20Bibliographically approved
Gu, R., Barbuceanu, T., Xiong, N. & Seceleanu, T. (2024). Experiences in Building a Digital Twin Framework: Challenges and Possible Solutions. In: Proceedings - 2024 IEEE 48th Annual Computers, Software, and Applications Conference, COMPSAC 2024: . Paper presented at 48th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2024, Osaka, Japan, 2-4 July, 2024 (pp. 531-536). Institute of Electrical and Electronics Engineers (IEEE)
Open this publication in new window or tab >>Experiences in Building a Digital Twin Framework: Challenges and Possible Solutions
2024 (English)In: Proceedings - 2024 IEEE 48th Annual Computers, Software, and Applications Conference, COMPSAC 2024, Institute of Electrical and Electronics Engineers (IEEE), 2024, p. 531-536Conference paper, Published paper (Refereed)
Abstract [en]

Digital Twins (DTs) serve as the backbone of Industry 4.0, offering virtual representations of actual systems, enabling accurate simulations, analysis, and control. These representations help predict system behaviour, facilitate multiple real-time tests, and reduce risks and costs while identifying optimization areas. DTs meld cyber and physical realms, accelerating the design and modelling of sustainable innovations. Despite their potential, the complexity of DTs presents challenges in their industrial application. We continue here the development of our approach to build an adaptable and trustable framework for building and operating DT systems - A Digital Twin Framework for Dynamic and Robust Distributed Systems (D-RODS). D-RODS aims to address the challenges above, aiming to advance industrial digitalization and targeting areas like system efficiency, incorporating AI and verification techniques with formal support. We employ existing large-usage tools to illustrate the approach in development based on a synthetic adaptable use case.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE), 2024
Keywords
Digital twins, machine learning, system design, Actual system, Analysis and controls, Distributed systems, In-buildings, Machine-learning, Real-time test, Simulation analysis, Simulation control, System behaviors, Virtual representations
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-68521 (URN)10.1109/COMPSAC61105.2024.00078 (DOI)001308581200069 ()2-s2.0-85204058274 (Scopus ID)9798350376968 (ISBN)
Conference
48th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2024, Osaka, Japan, 2-4 July, 2024
Available from: 2024-09-27 Created: 2024-09-27 Last updated: 2024-12-11Bibliographically approved
ter Beek, M. H., Chapman, R., Cleaveland, R., Garavel, H., Gu, R., ter Horst, I., . . . Zhang, L. (2024). Formal Methods in Industry. Formal Aspects of Computing
Open this publication in new window or tab >>Formal Methods in Industry
Show others...
2024 (English)In: Formal Aspects of Computing, ISSN 0934-5043, E-ISSN 1433-299XArticle in journal (Refereed) Published
Abstract [en]

Formal methods encompass a wide choice of techniques and tools for the specification, development, analysis, and verification of software and hardware systems. Formal methods are widely applied in industry, in activities ranging from the elicitation of requirements and the early design phases all the way to the deployment, configuration, and runtime monitoring of actual systems. Formal methods allow one to precisely specify the environment in which a system operates, the requirements and properties that the system should satisfy, the models of the system used during the various design steps, and the code embedded in the final implementation, as well as to express conformance relations between these specifications. We present a broad scope of successful applications of formal methods in industry, not limited to the well-known success stories from the safety-critical domain, like railways and other transportation systems, but also covering other areas such as lithography manufacturing and cloud security in e-commerce, to name but a few. We also report testimonies from a number of representatives from industry who, either directly or indirectly, use or have used formal methods in their industrial project endeavours. These persons are spread geographically, including Europe, Asia, North and South America, and the involved projects witness the large coverage of applications of formal methods, not limited to the safety-critical domain. We thus make a case for the importance of formal methods, and in particular of the capacity to abstract and mathematical reasoning that are taught as part of any formal methods course. These are fundamental Computer Science skills that graduates should profit from when working as computer scientists in industry, as confirmed by industry representatives.

National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:mdh:diva-69381 (URN)10.1145/3689374 (DOI)
Available from: 2024-12-09 Created: 2024-12-09 Last updated: 2024-12-09Bibliographically approved
Gu, R., Moezkarimi, Z. & Sirjani, M. (2024). Guess and Then Check: Controller Synthesis for Safe and Secure Cyber-Physical Systems. In: Lecture Notes in Computer Science: . Paper presented at 44th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2024, held as part of the 19th International Federated Conference on Distributed Computing Techniques, DisCoTec 2024, Groningen, Netherlands, 17 June through 21 June, 2024 (pp. 230-238). Springer Science+Business Media B.V.
Open this publication in new window or tab >>Guess and Then Check: Controller Synthesis for Safe and Secure Cyber-Physical Systems
2024 (English)In: Lecture Notes in Computer Science, Springer Science+Business Media B.V., 2024, p. 230-238Conference paper, Published paper (Refereed)
Abstract [en]

In this paper, we report our ongoing work on safe and secure controller synthesis for cyber-physical systems (CPS). Our approach separates the synthesis process into three phases, in which we alternatively perform exhaustive and selective exploration of the system’s state space. In this way, we combine the strengths of exhaustive search and learning to mitigate the state-space-explosion problem in controller synthesis while preserving the guarantee of safety and security. We implement the synthesis algorithms in the Rebeca (Reactive Objects Language) platform, which provides modelling, verification, and state-space visualization. We evaluate the new approach in an experiment, demonstrating the reduced number of explored states, which shows the potential of our approach for synthesizing safe and secure controllers for complex CPS.

Place, publisher, year, edition, pages
Springer Science+Business Media B.V., 2024
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 14678 LNCS
Keywords
Controllers, Cybersecurity, Embedded systems, Explosions, Modeling languages, Controller synthesis, Cybe-physical systems, Cyber-physical systems, Explosion problems, S state, State-space, State-space explosion, Synthesis process, Three phase, Three phasis, Cyber Physical System
National Category
Control Engineering
Identifiers
urn:nbn:se:mdh:diva-68046 (URN)10.1007/978-3-031-62645-6_13 (DOI)001273649500013 ()2-s2.0-85197245258 (Scopus ID)9783031626449 (ISBN)
Conference
44th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2024, held as part of the 19th International Federated Conference on Distributed Computing Techniques, DisCoTec 2024, Groningen, Netherlands, 17 June through 21 June, 2024
Available from: 2024-07-12 Created: 2024-07-12 Last updated: 2024-09-11Bibliographically approved
Gu, R. (2024). Learning in Uppaal for Test Case Generation for Cyber-Physical Systems. In: Lecture Notes in Computer Science: . Paper presented at 8th International Conference on Engineering of Computer-Based Systems, ECBS 2023, Västerås, 16 October 2023 through 18 October 2023 (pp. 70-74). Springer Science and Business Media Deutschland GmbH
Open this publication in new window or tab >>Learning in Uppaal for Test Case Generation for Cyber-Physical Systems
2024 (English)In: Lecture Notes in Computer Science, Springer Science and Business Media Deutschland GmbH , 2024, p. 70-74Conference paper, Published paper (Refereed)
Abstract [en]

We propose a test-case generation method for testing cyber-physical systems by using learning and statistical model checking. We use timed game automata for modelling. Different from other studies, we construct the model from the environment’s perspective. After building the model, we synthesize policies for different kinds of environments by using reinforcement learning in Uppaal and parse the policies for test-case generation. Statistical model checking enables us to analyse the test cases for finding the ones that are more likely to detect bugs. 

Place, publisher, year, edition, pages
Springer Science and Business Media Deutschland GmbH, 2024
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 14390 LNCS
Keywords
Embedded systems, Learning systems, Model checking, Reinforcement learning, Cybe-physical systems, Cyber-physical systems, Generation method, Learning models, Reinforcement learnings, Statistical model checking, Test case, Test case generation, Timed game automata, Cyber Physical System
National Category
Computer Sciences
Identifiers
urn:nbn:se:mdh:diva-65241 (URN)10.1007/978-3-031-49252-5_7 (DOI)2-s2.0-85180147773 (Scopus ID)9783031492518 (ISBN)
Conference
8th International Conference on Engineering of Computer-Based Systems, ECBS 2023, Västerås, 16 October 2023 through 18 October 2023
Available from: 2024-01-03 Created: 2024-01-03 Last updated: 2024-01-03Bibliographically approved
Gu, R. (2024). Model Checking for Reinforcement Learning in Autonomous Driving: One Can Do More Than You Think!. In: Proceedings Sixth International Workshop on Formal Methods for Autonomous Systems: . Paper presented at Sixth International Workshop on Formal Methods for Autonomous Systems (FMAS), Manchester, England, 11/11-13/11, 2024 (pp. 160-177). , 411
Open this publication in new window or tab >>Model Checking for Reinforcement Learning in Autonomous Driving: One Can Do More Than You Think!
2024 (English)In: Proceedings Sixth International Workshop on Formal Methods for Autonomous Systems, 2024, Vol. 411, p. 160-177Conference paper, Published paper (Refereed)
Abstract [en]

Most reinforcement learning (RL) platforms use high-level programming languages, such as OpenAI Gymnasium using Python. These frameworks provide various API and benchmarks for testing RL algorithms in different domains, such as autonomous driving (AD) and robotics. These platforms often emphasise the design of RL algorithms and the training performance but neglect the correctness of models and reward functions, which can be crucial for the successful application of RL. This paper proposes using formal methods to model AD systems and demonstrates how model checking (MC) can be used in RL for AD. Most studies combining MC and RL focus on safety, such as safety shields. However, this paper shows different facets where MC can strengthen RL. First, an MC-based model pre-analysis can reveal bugs with respect to sensor accuracy and learning step size. This step serves as a preparation of RL, which saves time if bugs exist and deepens users' understanding of the target system. Second, reward automata can benefit the design of reward functions and greatly improve learning performance especially when the learning objectives are multiple. All these findings are supported by experiments. 

Series
Electronic Proceedings in Theoretical Computer Science, ISSN 2075-2180
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-69356 (URN)10.4204/eptcs.411.11 (DOI)
Conference
Sixth International Workshop on Formal Methods for Autonomous Systems (FMAS), Manchester, England, 11/11-13/11, 2024
Available from: 2024-12-09 Created: 2024-12-09 Last updated: 2024-12-09Bibliographically approved
Gu, R., Baranov, E., Ameri, A., Enoiu, E. P., Curuklu, B., Seceleanu, C., . . . Lundqvist, K. (2024). Synthesis and Verification of Mission Plans for Multiple Autonomous Agents under Complex Road Conditions. ACM Transactions on Software Engineering and Methodology, 33(7), 1-46, Article ID 173.
Open this publication in new window or tab >>Synthesis and Verification of Mission Plans for Multiple Autonomous Agents under Complex Road Conditions
Show others...
2024 (English)In: ACM Transactions on Software Engineering and Methodology, ISSN 1049-331X, Vol. 33, no 7, p. 1-46, article id 173Article in journal (Other academic) Published
Abstract [en]

Mission planning for multi-agent autonomous systems aims to generate feasible and optimal mission plans that satisfy the given requirements. In this article, we propose a mission-planning methodology that combines (i) a path-planning algorithm for synthesizing path plans that are safe in environments with complex road conditions, and (ii) a task-scheduling method for synthesizing task plans that schedule the tasks in the right and fastest order, taking into account the planned paths. The task-scheduling method is based on model checking, which provides means of automatically generating task execution orders that satisfy the requirements and ensure the correctness and efficiency of the plans by construction. We implement our approach in a tool named MALTA, which offers a user-friendly GUI for configuring mission requirements,  a module for path planning, an integration with the model checker UPPAAL, and functions for automatic generation of formal models, and parsing of the execution traces of models. Experiments with the tool demonstrate its applicability and performance in various configurations of an industrial case study of an autonomous quarry. We also show the adaptability of our tool by employing it on a special case of the industrial case study.

National Category
Computer Sciences
Identifiers
urn:nbn:se:mdh:diva-58047 (URN)10.1145/3672445 (DOI)2-s2.0-85202215443 (Scopus ID)
Available from: 2022-04-20 Created: 2022-04-20 Last updated: 2024-12-09Bibliographically approved
Dust, L., Gu, R., Seceleanu, C., Ekström, M. & Mubeen, S. (2024). UPPAAL-Based Modeling and Verification of ROS 2 Multi-threaded Execution and Operating System Reservations. In: Lect. Notes Comput. Sci.: . Paper presented at 29th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2024. Milan. 9 September 2024 through 11 September 2024. Code 317649. Notes in Bioinformatics) (pp. 40-59). Springer Science and Business Media Deutschland GmbH
Open this publication in new window or tab >>UPPAAL-Based Modeling and Verification of ROS 2 Multi-threaded Execution and Operating System Reservations
Show others...
2024 (English)In: Lect. Notes Comput. Sci., Springer Science and Business Media Deutschland GmbH , 2024, p. 40-59Conference paper, Published paper (Refereed)
Abstract [en]

In this paper, we propose a formal modeling approach in Uppaal to simulate and verify multi-threaded robotics middleware execution based on ROS 2. In the modeling process, we consider middleware-specific scheduling by creating formal models that simulate the execution behavior of a ROS 2-based system. Furthermore, we show how to model potential underlying operating system’s influences on execution, by modeling reservation servers. We propose timed automata templates to model the multi-threaded execution of ROS 2 systems and the reservations of the underlying operating system in Uppaal. We show how to use the created templates to simulate a ROS 2 application. We demonstrate the application of the formal models and model checking in various ROS 2 experiments. Furthermore, we validate the created models by comparing the observed execution traces in experiments on ROS 2 systems and the simulated traces of our models. Overall, this paper showcases the application and usefulness of model-based verification of distributed middleware applications, including internal scheduling and influences of underlying operating system actions.

Place, publisher, year, edition, pages
Springer Science and Business Media Deutschland GmbH, 2024
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 14952 LNCS
Keywords
Model Checking, Pattern-Based Modeling, Robot Operating System 2, Multipurpose robots, Reservation systems, Robot Operating System, Based modelling, Formal modeling, Modeling and verifications, Modeling approach, Modeling process, Models checking, Multithreaded, Pattern-based models, Robotic middlewares, Middleware
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-68428 (URN)10.1007/978-3-031-68150-9_3 (DOI)001308668900003 ()2-s2.0-85202641490 (Scopus ID)9783031681493 (ISBN)
Conference
29th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2024. Milan. 9 September 2024 through 11 September 2024. Code 317649. Notes in Bioinformatics)
Available from: 2024-09-11 Created: 2024-09-11 Last updated: 2024-10-16Bibliographically approved
Organisations

Search in DiVA

Show all publications