One of the challenges in designing safe, reliable and trustworthy Autonomous Vehicles (AVs) is to ensure that the AVs abide by traffic rules. For this, the AVs need to be able to understand and reason about traffic rules. In previous work, we introduce the spatial traffic logic USL-TR to allow for the unambiguous, machine-readable, formalisation of traffic rules. This is only the first step towards autonomous traffic agents that verifiably follow traffic rules. In this research preview, we focus on two further steps: a) retrieving behaviour diagrams directly from traffic rules and b) converting the behaviour diagrams into timed automata that are using formulae of USL-TR in guards and invariants. With this, we have a formal representation for traffic rules and can move towards the establishment of a Digital Highway Code. We briefly envision further steps which include adding environment and agent models to the timed automata to finally implement and verify these traffic rule models using a selection of formal verification tools.


    Zugriff

    Download


    Exportieren, teilen und zitieren



    Titel :

    Towards a Digital Highway Code using Formal Modelling and Verification of Timed Automata


    Beteiligte:

    Erscheinungsdatum :

    2022


    Anmerkungen:

    In Proceedings FMAS2022 ASYDE2022, arXiv:2209.13181
    EPTCS 371, 2022, pp. 77-85



    Medientyp :

    Preprint


    Format :

    Elektronische Ressource


    Sprache :

    Englisch




    Towards a Digital Highway Code using Formal Modelling and Verification of Timed Automata

    Alves, Gleifer Vaz / Schwammberger, Maike / Luckcuck, Matt et al. | DataCite | 2022

    Freier Zugriff

    An Innovative Approach for Modelling Urban Road Traffic Using Timed Automata and Formal Methods

    Eduardo Valente / Camelia Avram / José Machado et al. | DOAJ | 2018

    Freier Zugriff


    Runtime Verification of Railway Interlocking Software with Parametric Timed Automata

    Chai, Ming / Wang, Haifeng / Zhang, Jian et al. | IEEE | 2018


    Methods for Modeling Urban Road Traffic Using Timed Automata

    Avram, Camelia / Machado, Jose / Astilean, Adina | TIBKAT | 2020