kth.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
CommonUppRoad: A Framework of Formal Modelling, Verifying, Learning, and Visualisation of Autonomous Vehicles
Mälardalen University, Västerås, Sweden.
KTH, School of Industrial Engineering and Management (ITM), Engineering Design, Mechatronics and Embedded Control Systems.ORCID iD: 0000-0003-4535-3849
Aalborg University, Aalborg, Denmark.
KTH, School of Industrial Engineering and Management (ITM), Engineering Design, Mechatronics and Embedded Control Systems.ORCID iD: 0000-0001-5703-5923
Show others and affiliations
2025 (English)In: Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification - 12th International Symposium, ISoLA 2024, Proceedings, Springer Nature , 2025, p. 385-404Conference paper, Published paper (Refereed)
Abstract [en]

Combining machine learning and formal methods (FMs) provides a possible solution to overcome the safety issue of autonomous driving (AD) vehicles. However, there are gaps to be bridged before this combination becomes practically applicable and useful. In an attempt to facilitate researchers in both FMs and AD areas, this paper proposes a framework that combines two well-known tools, namely CommonRoad and UPPAAL. On the one hand, CommonRoad can be enhanced by the rigorous semantics of models in UPPAAL, which enables a systematic and comprehensive understanding of the AD system’s behaviour and thus strengthens the safety of the system. On the other hand, controllers synthesised by UPPAAL can be visualised by CommonRoad in real-world road networks, which facilitates AD vehicle designers greatly adopting formal models in system design. In this framework, we provide automatic model conversions between CommonRoad and UPPAAL. Therefore, users only need to program in Python and the framework takes care of the formal models, learning, and verification in the backend. We perform experiments to demonstrate the applicability of our framework in various AD scenarios, discuss the advantages of solving motion planning in our framework, and show the scalability limit and possible solutions.

Place, publisher, year, edition, pages
Springer Nature , 2025. p. 385-404
Keywords [en]
Autonomous vehicles, CommonRoad, Motion planning, Reinforcement learning, UPPAAL
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:kth:diva-356658DOI: 10.1007/978-3-031-75380-0_22ISI: 001419014500022Scopus ID: 2-s2.0-85208574191OAI: oai:DiVA.org:kth-356658DiVA, id: diva2:1914828
Conference
12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2024, Crete, Greece, October 27-31, 2024
Note

Part of ISBN 9783031753794

QC 20241121

Available from: 2024-11-20 Created: 2024-11-20 Last updated: 2025-03-17Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Tan, KaigeFeng, Lei

Search in DiVA

By author/editor
Tan, KaigeFeng, Lei
By organisation
Mechatronics and Embedded Control Systems
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 71 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf