A Double-Level Model Checking Approach for an Agent-Based Autonomous Vehicle and Road Junction Regulations
| Autor: | Louise A. Dennis, Gleifer Vaz Alves, Michael Fisher |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: |
Model checking
Technology Control and Optimization Computer Networks and Communications Computer science Distributed computing 020207 software engineering 02 engineering and technology Tracing Autonomous Vehicles model checking Automaton agents Road junction Rules of the Road 0202 electrical engineering electronic engineering information engineering Java pathfinder Code (cryptography) 020201 artificial intelligence & image processing Instrumentation Formal verification Road user |
| Zdroj: | Alves, G V, Dennis, L & Fisher, M 2021, ' A Double-Level Model Checking Approach for an Agent-Based Autonomous Vehicle and Road Junction Regulations ', Journal of Sensor and Actuator Networks . https://doi.org/10.3390/jsan10030041 Journal of Sensor and Actuator Networks, Vol 10, Iss 41, p 41 (2021) Journal of Sensor and Actuator Networks Volume 10 Issue 3 |
| Popis: | Usually, the design of an Autonomous Vehicle (AV) does not take into account traffic rulesand so the adoption of these rules can bring some challenges, e.g., how to come up with a DigitalHighway Code which captures the proper behaviour of an AV against the traffic rules and at the sametime minimises changes to the existing Highway Code? Here, we formally model and implementthree Road Junction rules (from the UK Highway Code). We use timed automata to model the systemand the MCAPL (Model Checking Agent Programming Language) framework to implement an agentand its environment. We also assess the behaviour of our agent according to the Road Junction rulesusing a double-level Model Checking technique, i.e., UPPAAL at the design level and AJPF (AgentJava PathFinder) at the development level. We have formally verified 30 properties (18 with UPPAALand 12 with AJPF), where these properties describe the agent’s behaviour against the three RoadJunction 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 timeconstraints in UPPAAL timed automata to determine thresholds for the AVs actions and tracing theagent’s behaviour by using MCAPL, in a way that one can tell when and how a given Road Junctionrule was selected by the agent. This work provides a proof-of-concept for the formal verification ofAV behaviour with respect to traffic rules. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|