A DSL for formally verified interactive robotic applications in service settings

Nowadays, we hear more and more of the rapid spread of robots and their application. Furthermore, creating robotic applications is a hard work that requires a heterogeneous team. Domain Specific Languages (DSLs) represent an interesting tool to support the development of robotic applications. The objective of the thesis is to present a DSL for formally verified interactive robotic applications in service settings and present the implementation of this language in the form of a plugin. Considering a specific framework for robotic applications developed by Politecnico di Milano, the purpose of the language and its implementation is to provide the necessary tools to make the aforementioned framework more accessible and easier to use. In fact, the developed DSL is a high-level language that allows the user to write and read the scenarios in a simple and intuitive way and the plugin offers a powerful and simple interface for using the framework itself. This document first describes the defined DSL. Then, it provides a description of the implementation of the developed language. Finally, to evaluate the correct functioning of the language implementation and its integration with the framework, some integration tests were conducted. Thanks to these tests it has been verified that the plugin actually offers the user the desired services.

Al giorno d'oggi, sentiamo sempre di più della rapida diffusione dei robot e delle loro applicazioni. Inoltre, la creazione di applicazioni robotiche è un duro lavoro che richiede un team eterogeneo. I linguaggi specifici di dominio (Domain Specific Languages, DSLs) rappresentano uno strumento interessante per supportare lo sviluppo di applicazioni robotiche. L'obiettivo della tesi è presentare un DSL per applicazioni robotiche interattive formalmente verificate in impostazioni di servizio e presentare l'implementazione di questo linguaggio sotto forma di plugin. Considerando un framework specifico per applicazioni robotiche sviluppato dal Politecnico di Milano, lo scopo del linguaggio e la sua implementazione è quello di fornire gli strumenti necessari per rendere il framework suddetto più accessibile e più facile da usare. Infatti il DSL sviluppato è un linguaggio di alto livello che permette all'utente di scrivere e leggere gli scenari in modo semplice ed intuitivo e il plugin offre un'interfaccia potente e semplice per l'utilizzo del framework stesso. Questo documento descrive innanzitutto il DSL definito. Quindi, fornisce una descrizione dell'implementazione del linguaggio sviluppato. Infine, per valutare il corretto funzionamento dell'implementazione del linguaggio e la sua integrazione con il framework, sono stati condotti alcuni test di integrazione. Grazie a questi test è stato verificato che il plugin offre effettivamente all'utente i servizi desiderati.