The Simulated Automotive Environment (SAE) comprises: implementation and formal verification of controlling mechanisms using the MCAPL (Model Checking Agent Programming Language) framework. Our systems use intelligent agents representing basic Autonomous Vehicles mechanisms.
MCAPL framework is used in order to implement and formal verify basic controlling mechanism for Autonomous Vehicles.
Our Simulated Automotive Environment (SAE) comprises the following:
• Gwendolen rational agent responsible for basic driving plans and obstacle avoidance.
• Formal verification properties written in Temporal logic.
• Verification of these properties via AJPF model checking.
• Simulated environment implemented in Java.
In order to run the SAE it is necessary to use MCAPL and the related tools: Gwendolen agent programming, AJPF model checking. http://mcapl.sourceforge.net/
The SAE is part of AVIA (Autonomous Vehicles with Intelligent Agents) Research Project, which is a collaboration between Federal University of Technology - Parana (UTFPR) and University of Liverpool.
Contacts:
Lucas E. R. Fernandes lucfer@alunos.utfpr.edu.br
Vinicius Custodio viniciuscustodio@alunos.utfpr.edu.br
Gleifer Vaz Alves gleifer@utfpr.edu.br
Louise Dennis
Michael Fisher