Modellazione, Programmazione, Analisi,

Simulazione e Verifica di Sistemi Complessi

La nascita del Dipartimento IBRIDS,

Workshop, 23 febbraio 2012

Chi siamo

member(lpgroup, martelli, maurizio).member(lpgroup, delzanno, giorgio).member(lpgroup, mascardi, viviana).

member(lpgroup, locoro, angela).member(lpgroup, briola, daniela).

member(lpgroup, traverso, riccardo).

Maurizio Martelli, PO

Maurizio Martelli, PO

Giorgio Delzanno, PA

Maurizio Martelli, PO

Giorgio Delzanno, PA

Viviana Mascardi, Ric

Angela Locoro, Post Doc

Angela Locoro, Post Doc

Daniela Briola, Post Doc

Angela Locoro, Post Doc

Daniela Briola, Post Doc

Riccardo Traverso, dottorando

La nascitamortal(X) :- chick(X).chick(piopio).

?- mortal(piopio).?- yes

/* ...mo' me lo segno... */

Nasciamo come “Gruppo di Programmazione Logica” nel 1992

Negli ultimi anni del millennio individuiamo nella modellazione, prototipazione e verifica di sistemi complessi un dominio promettente in cui applicare la Logica Computazionale

Attualmente lavoriamo sulle tematiche originali alle quali abbiamo aggiunto tematiche più applicative e di ampio respiro anche collegate all'ingegneria del software

Ci piacciono

... la logica computazionale

Tutti gli esseri umani sono mortali. Socrate è umano. Quindi, Socrate è mortale.

mortal(X) :- human(X).human(socrates).

?- mortal(socrates).?- yes

?- mortal(Y).?- Y = socrates ? ;no

...i sistemi multi-agente

...le ontologie

...la verifica e il model checking

Diciamo qualcosa di utile su...

...la logica computazionale

Strumento flessibile per specificare sistemi che ragionano, ottenendo gratuitamente un prototipo eseguibile.

Consente di realizzare facilmente metaprogrammi: programmi che ragionano su altri programmi. Molto comodo per analizzare staticamente il comportamento di un agente e per implementare agenti con capacità metacognitive.

...i sistemi multiagente

La stragrande maggioranza degli scenari che impiegano sistemi distribuiti moderni sono intrinsecamente inclini ad essere sviluppati in termini di sistemi multi-agente, [...] i sistemi distribuiti moderni sono già di fatto dei sistemi multi-agente, essendo costituiti da componenti autonome, collocate in un ambiente e sociali

F.Zambonelli ed A. Omicini, JAAMAS, 9(3), 2004

...le ontologie

Servono a realizzare l'interoperabilità semantica tra sistemi eterogenei.

Nel giro di pochi anni praticamente ogni società, università, agenzia governativa o qualsiasi gruppo che condivida un interesse vorrà collegare le proprie risorse web ai contenuti di un'ontologia - a causa dei molti e potenti mezzi che saranno disponibili per sfruttarle. Su questa infrastruttura, la computazione ad agenti sarà la tipologia principale del futuro prossimo

J. A. Hendler. Agents and the semantic web. IEEE Intelligent Systems, 16(2):30-37, 2001

...la verifica e il model checking

Verificare formalmente alcune proprietà dei sistemi serve a essere certi del loro comportamento

Usiamo verifica e model checking per modellare, analizzare e verificare sistemi concorrenti e distribuiti, ad esempio sistemi parametrici nel numero delle componenti come una rete ad hoc

Le nostre gratificazioni

“FYPA - Find Your Path, Agent!” sviluppato da D. Briola in collaborazione con Ansaldo STS, è risultato finalista nel “2011 Ansaldo STS Innovation Award”

“SimulRisk - Simulatore in tecnologia SW agent per la valutazione del rischio di siti fisici” sviluppato da R. Traverso in collaborazione con ElsagDatamat ha vinto il premio innovazione e sicurezza TechFOr 2010

Le nostre cene sociali

10th International Workshop on Declarative Agent Languages and Technologies, DALT@AAMAS 2012, Valencia, 2012

5th International Workshop on Reachability, RP 2011, Genoa, Italy, 2011

2nd International Multi-Agent Logics, Languages, and Organisations Federated Workshops, MALLOW’009, Lyon, 2009

1st International Workshop on Agents, Web Services and Ontologies, Integrated Methodologies, MALLOW-AWESOME’007, Torino, 2007

Workshop dagli Oggetti agli Agenti, WOA 2007, Genova, 2007

I nostri $$$

Titolo e Anno

Nome partecipante e Ruolo Fonte Finanziamento UO

Indiana MAS2012-2015

V. Mascardi, coordinatore nazionale. D. Briola, A. Locoro, M. Martelli, partecipanti

MIUR-FIRB 331.100 €

DISCO2010-2012

G. Delzanno, partecipante MIUR-PRIN 20.000 €

Iniziativa SW CINI-FinMeccanica 2010-2012

V. Mascardi, coordinatore locale; A. Locoro, M. Martelli, partecipanti

Industria 75.000 €

I nostri $$$

Titolo e Anno

Nome partecipante e Ruolo Fonte Finanziamento UO

Assegno per verifica di reti Ad Hoc2010

G. Delzanno, coordinatore locale

Fondazione 12.000 €

Sintesis (progetto SIIT) 2009-2010

G. Delzanno, partecipante Industria 144.100 €

TecDoc (progetto SIIT) 2007-2009

Maurizio Martelli, Viviana Mascardi, partecipanti

Industria 104.400 €

Oggi no, ma domani...

Definiremo la semantica dell'ambiente in cui gli agenti sono collocati e miglioreremo la comunicazione tra agenti utilizzando ontologie

Applicheremo gli agenti e ontologie al dominio dei beni culturali

Modelleremo protocolli in ambiente wireless e distribuito (es: assenza di loop nelle tabelle di routing)

Combineremo tecniche globali e locali per l'analisi di sistemi distribuiti (es: dimostrare mutua esclusione usando proprietà locali dei singoli processi)

Analizzeremo sistemi temporizzati (es: clock, reset, time-out)

Analizzeremo e verificheremo software multithreaded (es: model checking di Concurrent Java)

(grazie per l'attenzione)