A Double-Level Model Checking Approach for an Agent-Based Autonomous Vehicle and Road Junction Regulations

Alves, Gleifer Vaz, Dennis, Louise ORCID: 0000-0003-1426-1896 and Fisher, Michael (2021) A Double-Level Model Checking Approach for an Agent-Based Autonomous Vehicle and Road Junction Regulations. JOURNAL OF SENSOR AND ACTUATOR NETWORKS, 10 (3). p. 41.

Access the full-text of this item by clicking on the Open Access link.

Official URL: http://dx.doi.org/10.3390/jsan10030041

Abstract

<jats:p>Usually, the design of an Autonomous Vehicle (AV) does not take into account traffic rules and so the adoption of these rules can bring some challenges, e.g., how to come up with a Digital Highway Code which captures the proper behaviour of an AV against the traffic rules and at the same time minimises changes to the existing Highway Code? Here, we formally model and implement three Road Junction rules (from the UK Highway Code). We use timed automata to model the system and the MCAPL (Model Checking Agent Programming Language) framework to implement an agent and its environment. We also assess the behaviour of our agent according to the Road Junction rules using a double-level Model Checking technique, i.e., UPPAAL at the design level and AJPF (Agent Java PathFinder) at the development level. We have formally verified 30 properties (18 with UPPAAL and 12 with AJPF), where these properties describe the agent’s behaviour against the three Road Junction rules using a simulated traffic scenario, including artefacts like traffic signs and road users. In addition, our approach aims to extract the best from the double-level verification, i.e., using time constraints in UPPAAL timed automata to determine thresholds for the AVs actions and tracing the agent’s behaviour by using MCAPL, in a way that one can tell when and how a given Road Junction rule was selected by the agent. This work provides a proof-of-concept for the formal verification of AV behaviour with respect to traffic rules.</jats:p>

Item Type:	Article
Uncontrolled Keywords:	Rules of the Road, Autonomous Vehicles, agents, model checking
Divisions:	Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User:	Symplectic Admin
Date Deposited:	23 Dec 2021 15:05
Last Modified:	15 Mar 2024 05:04
DOI:	10.3390/jsan10030041
Open Access URL:	https://www.mdpi.com/2224-2708/10/3/41
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3145968