Risorse

Aree/Progetti collegati

Coordinatore/i

Membri

Sottoaree

Ricerca: dettaglio

  • Home
  • > Ricerca
  • > Ricerca: dettaglio: Specifica e verifica di protocolli di interazione fra agenti

Specifica e verifica di protocolli di interazione fra agenti

Coordinatore/i: Alberto Martelli  

Membri:
Matteo Baldoni  
Cristina Baroglio  
Valentina Gliozzi  
Viviana Patti  
Gian Luca Pozzato  

Attivit?

I servizi forniti in molti domini applicativi sempre pi? possono essere descritti e realizzati come espressione di un insieme di agenti cooperanti. Rispetto all'approccio pi? tradizionale della programmazione a componenti, il paradigma ad agenti esplicita aspetti sociali, connessi alla caratteristica degli agenti di essere autonomi e proattivi: le componenti comunicano e si coordinano in maniera dinamica, utilizzando linguaggi ad alto livello, per perseguire scopi comuni (o propri). Tra gli aspetti sociali ? particolarmente importante definire "regole comportamentali", espresse mediante protocolli di comunicazione (interazione), finalizzate a controllare l'organizzazione del sistema. I protocolli di comunicazione possono essere utilizzati per regolare l'interazione fra gli agenti specificando un insieme di conversazioni accettabili, ossia sequenze di operazioni (in particolare scambi di messaggi) che si possono svolgere fra agenti diversi. Con la rapida espansione di internet, gli agenti si trovano sempre pi? ad operare in ambienti fortemente dinamici. Diventa quindi essenziale che gli agenti soddisfino propriet? che ne garantiscano l'interoperabilit?, come ad esempio che un agente sia conforme a un protocollo di interazione, che un agente stia rispettando i suoi vincoli sociali o che un protocollo ottenuto per composizione conservi le propriet? dei protocolli che lo compongono. Per dimostrare se un protocollo garantisce o meno determinate propriet? ? necessario specificarlo in un linguaggio formale. Infatti l'utilizzo di linguaggi formali di specifica consente di sviluppare tecniche di verifica formale di propriet?.

L'obiettivo di questo progetto ? quello di sviluppare strumenti e tecniche per la specifica e la verifica di propriet? riguardanti l'interazione fra agenti in un sistema multiagente. Pi? precisamente i principali obiettivi del progetto sono i seguenti:
Definizione di formalismi per la specifica e la verifica di protocolli di interazione
Verranno analizzate le principali propriet? dei protocolli di interazione che si intendono verificare, e verranno individuati i formalismi pi? adeguati per esprimere queste propriet?. I formalismi utilizzati per specificare protocolli di comunicazione e per descriverne le propriet? saranno prevalentemente basati sulla logica (temporale e computazionale), ma si prenderanno in considerazione anche formalismi a vincoli, linguaggi formali ed automi.

Verifica automatica delle propriet?
Verranno messe a punto tecniche di verifica per i formalismi sviluppati nel punto precedente. In particolare, per le logiche temporali, saranno sviluppate tecniche di model checking. In altri casi, si applicheranno tecniche basate su procedure di dimostrazione e si indagheranno tecniche basate su risoluzione estesa. Verranno anche sviluppate tecniche di prototipazione rapida per la validazione di protocolli di interazione.

Linguaggi di modellazione e loro traduzione nei linguaggi formali definiti nel progetto
Per lo sviluppo dei sistemi multiagente sono stati proposti numerosi linguaggi di modellazione. Questi linguaggi mancano di semantica formale e quindi non sono utilizzabili direttamente per la dimostrazione automatica di propriet? delle componenti del sistema. Un obiettivo ? quello di analizzare i linguaggi di modellazione pi? diffusi, in particolare formalismi grafici, e di definire tecniche di traduzione nei formalismi sviluppati nel progetto.

I linguaggi, le tecniche e gli strumenti sviluppati verranno valutati in diversi ambiti applicativi, fra cui principalmente: linee guida cliniche, servizi web, commercio elettronico e sicurezza, presentazioni multimediali.

Aree/Progetti collegati:
Knowledge Representation and Reasoning

Appartiene a:
PROGETTI PRECEDENTI