Integrated simulation and formal verification of a simple autonomous vehicle

Adriano Fagiolini, Andrea Domenici, Maurizio Palmieri

Risultato della ricerca: Paper

2 Citazioni (Scopus)

Abstract

This paper presents a proof-of-concept application of an approach to system development based on the integration of formal verification and co-simulation. A simple autonomous vehicle has the task of reaching an assigned straight path and then follow it, and it can be controlled by varying its turning speed. The correctness of the proposed control law has been formalized and verified by interactive theorem proving with the Prototype Verification System. Concurrently, the system has been co-simulated using the Prototype Verification System and the MathWorks Simulink tool: The vehicle kinematics have been simulated in Simulink, whereas the controller has been modeled in the logic language of the Prototype Verification System and simulated with the interpreter for the same language available in the theorem proving environment. With this approach, co-simulation and formal verification corroborate each other, thus strengthening developers’ confidence in their analysis
Lingua originaleEnglish
Stato di pubblicazionePublished - 2017

Fingerprint

Theorem proving
Kinematics
Controllers
Formal verification

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cita questo

Integrated simulation and formal verification of a simple autonomous vehicle. / Fagiolini, Adriano; Domenici, Andrea; Palmieri, Maurizio.

2017.

Risultato della ricerca: Paper

@conference{b67801619ed64b55bfb6a3363c911b45,
title = "Integrated simulation and formal verification of a simple autonomous vehicle",
abstract = "This paper presents a proof-of-concept application of an approach to system development based on the integration of formal verification and co-simulation. A simple autonomous vehicle has the task of reaching an assigned straight path and then follow it, and it can be controlled by varying its turning speed. The correctness of the proposed control law has been formalized and verified by interactive theorem proving with the Prototype Verification System. Concurrently, the system has been co-simulated using the Prototype Verification System and the MathWorks Simulink tool: The vehicle kinematics have been simulated in Simulink, whereas the controller has been modeled in the logic language of the Prototype Verification System and simulated with the interpreter for the same language available in the theorem proving environment. With this approach, co-simulation and formal verification corroborate each other, thus strengthening developers’ confidence in their analysis",
author = "Adriano Fagiolini and Andrea Domenici and Maurizio Palmieri",
year = "2017",
language = "English",

}

TY - CONF

T1 - Integrated simulation and formal verification of a simple autonomous vehicle

AU - Fagiolini, Adriano

AU - Domenici, Andrea

AU - Palmieri, Maurizio

PY - 2017

Y1 - 2017

N2 - This paper presents a proof-of-concept application of an approach to system development based on the integration of formal verification and co-simulation. A simple autonomous vehicle has the task of reaching an assigned straight path and then follow it, and it can be controlled by varying its turning speed. The correctness of the proposed control law has been formalized and verified by interactive theorem proving with the Prototype Verification System. Concurrently, the system has been co-simulated using the Prototype Verification System and the MathWorks Simulink tool: The vehicle kinematics have been simulated in Simulink, whereas the controller has been modeled in the logic language of the Prototype Verification System and simulated with the interpreter for the same language available in the theorem proving environment. With this approach, co-simulation and formal verification corroborate each other, thus strengthening developers’ confidence in their analysis

AB - This paper presents a proof-of-concept application of an approach to system development based on the integration of formal verification and co-simulation. A simple autonomous vehicle has the task of reaching an assigned straight path and then follow it, and it can be controlled by varying its turning speed. The correctness of the proposed control law has been formalized and verified by interactive theorem proving with the Prototype Verification System. Concurrently, the system has been co-simulated using the Prototype Verification System and the MathWorks Simulink tool: The vehicle kinematics have been simulated in Simulink, whereas the controller has been modeled in the logic language of the Prototype Verification System and simulated with the interpreter for the same language available in the theorem proving environment. With this approach, co-simulation and formal verification corroborate each other, thus strengthening developers’ confidence in their analysis

UR - http://hdl.handle.net/10447/286532

M3 - Paper

ER -