Deliberazione dinamica verificabile e adattiva consapevole del contesto

Abstract

Questa tesi mira a migliorare le capacità dei robot di eseguire com- compiti complessi in modo robusto e sicuro all'interno di ambienti non strutturati, ad esempio basandosi su un adattamento autonomo e non supervisionato al variare del funzionamento contesti nazionali. Nello specifico, la ricerca si propone di verificare formalmente i de- capacità di liberazione dei robot, garantendo un funzionamento sicuro e prolungato senza intervento umano. Integrando queste capacità in a toolchain software basata su modello, l'approccio consente agli sviluppatori di farlo costruire sistemi di deliberazione specifici dell'applicazione in grado di determinare comportamenti appropriati per il completamento dell'attività tenendo conto del contesto operativo del robot ed esperienze passate. La metodologia facilita l'implementazione e la configurazione di re- componenti necessari per eseguire questi comportamenti, automatizzando al contempo il analisi dei comportamenti per garantire la sicurezza e la protezione. Questo è stato ottenuto attraverso l’uso di modelli e strumenti formali sia in fase di progettazione che in fase di progettazione verifica in fase di esecuzione. La tesi si concentra su una nave robot umanoide entrare in un ambiente, dove deve adattare il suo comportamento alla dinamica cambiamenti ambientali, come la presenza umana o la connessione di rete problemi di attività e modificare il tour di conseguenza. La ricerca introduce inoltre un linguaggio formale di specificazione delle proprietà misura per codificare i requisiti e costruire monitoraggi di runtime, includere migliorare l’affidabilità delle operazioni robotiche. Il sistema è convalidato attraverso esperimenti condotti in simulazioni, dimostrandone le funzionalità capacità nel garantire sicurezza e flessibilità operativa in ambienti dinamici ambienti. Inoltre, è presente un ambiente di virtualizzazione a livello di sistema operativo forniti per riprodurre esperimenti simulati. I risultati contribuiscono prezio

This thesis aims to advance the capabilities of robots to perform com- plex tasks robustly and safely within unstructured environments, fo- cusing on autonomous and unsupervised adaptation to varying oper- ational contexts. Specifically, the research seeks to formally verify the cognitive de- liberation capabilities of robots, ensuring safe, prolonged operation without human intervention. By integrating these capabilities into a model-driven software toolchain, the approach enables developers to build application-specific deliberation systems capable of determining appropriate behaviors for task completion while accounting for the robot’s operational context and past experiences. The methodology facilitates the deployment and configuration of re- quired components to execute these behaviors, while automating the analysis of behaviors to ensure safety and security. This is achieved through the use of formal models and tools for both design-time and runtime verification. The thesis focuses on a humanoid robot navi- gating in a environment, where it must adapt its behavior to dynamic environmental changes, such as human presence or network connec- tivity issues, and modify its tour accordingly. The research further introduces a formal property specification lan- guage to encode requirements and construct runtime monitors, en- hancing the reliability of robotic operations. The system is validated through experiments conducted in simulations, demonstrating its fea- sibility in ensuring safety and operational flexibility in dynamic en- vironments. Additionally, an OS-level virtualization environment is provided to reproduce simulated experiments. The results contribute valuable insights into the design and deployment of autonomous sys- tems, offering a scalable, formally grounded methodology that inte- grates synchronous and asynchronous message-passing models.