Specifica e verifica di protocolli nel progetto Massive

Marco Alberti, Fedrico Chesani, Anna Ciampolini, Paola Mello, Marco Montali, Sergio Storari, Paolo Torroni

DEIS, Universita` di BolognaENDIF, Universita` di Ferrara

Specifica e verifica di protocolli nel progetto Massive

Marco Alberti, Fedrico Chesani, Anna Ciampolini, Paola Mello, Marco Montali, Sergio Storari, Paolo Torroni

DEIS, Universita` di BolognaENDIF, Universita` di Ferrara

ProtocolloProtocolloProtocolloProtocollo

Def. Insieme delle regole che governano un'attività di scambio di informazioni fra due o piu` entità.

– protocolli per la trasmissione di dati tra computer

– protocolli di interazione tra agenti

– protocolli di negoziazione nel commercio eletrronico

– protocolli medici (linee guida)

– ...

concetto generale applicabile a sistemi complessi e distribuiti: necessita` di strumenti per:

– specificare i protocolli

– verificare i protocolli

Def. Insieme delle regole che governano un'attività di scambio di informazioni fra due o piu` entità.

– protocolli per la trasmissione di dati tra computer

– protocolli di interazione tra agenti

– protocolli di negoziazione nel commercio eletrronico

– protocolli medici (linee guida)

– ...

concetto generale applicabile a sistemi complessi e distribuiti: necessita` di strumenti per:

– specificare i protocolli

– verificare i protocolli

Obiettivi Obiettivi Obiettivi Obiettivi

Individuare formalismi basati su logica per la descrizione di protocolli di interazione per agenti in società aperte:– specifica formale

– verifica di proprietà

– implementazione

Sperimentazione in casi reali:– linee guida cliniche

– e-commerce (protocolli per aste e transazioni commerciali)

– e-learning (by doing)

– protocolli internet (TCP/IP)

– ...

Sinergia con il progetto europeo

Individuare formalismi basati su logica per la descrizione di protocolli di interazione per agenti in società aperte:– specifica formale

– verifica di proprietà

– implementazione

Sperimentazione in casi reali:– linee guida cliniche

– e-commerce (protocolli per aste e transazioni commerciali)

– e-learning (by doing)

– protocolli internet (TCP/IP)

– ...

Sinergia con il progetto europeo

SOCS: societa` aperte di agenti basate su logica SOCS: societa` aperte di agenti basate su logica computazionalecomputazionale

SOCS: societa` aperte di agenti basate su logica SOCS: societa` aperte di agenti basate su logica computazionalecomputazionale

agenti eterogenei: non e` possibile fare assunzioni sulla struttura interna degli agenti, ma e` possibile osservare il comportamento sociale degli agenti (interazioni)

Gli agenti e la societa` hanno conoscenza incompleta dell'ambiente in cui operano.

Applicazione di forme di ragionamento abduttivo per modellare sia le interazioni tra agenti logici, che il comportamento del singolo agente.

Definizione di un linguaggio di programmazione logica (opportunamento esteso) per descrivere le societa`

Definizione di procedure di dimostrazione come supporto operazionale:

– verifica automatica delle interazioni

– verifica di proprieta` del protocollo

agenti eterogenei: non e` possibile fare assunzioni sulla struttura interna degli agenti, ma e` possibile osservare il comportamento sociale degli agenti (interazioni)

Gli agenti e la societa` hanno conoscenza incompleta dell'ambiente in cui operano.

Applicazione di forme di ragionamento abduttivo per modellare sia le interazioni tra agenti logici, che il comportamento del singolo agente.

Definizione di un linguaggio di programmazione logica (opportunamento esteso) per descrivere le societa`

Definizione di procedure di dimostrazione come supporto operazionale:

– verifica automatica delle interazioni

– verifica di proprieta` del protocollo

Verifica delle interazioni Verifica delle interazioni Verifica delle interazioni Verifica delle interazioni

Protocolli?

Agenti

SocialBehaviour

Infrastruttura Sociale

Fulfillment

Violation

Reasoning and verification

module

Protocols

Modello della Societa`:Modello della Societa`:<<SOKB, SEKBSOKB, SEKB, , ICICss, , GoalsGoals>>

Modello della Societa`:Modello della Societa`:<<SOKB, SEKBSOKB, SEKB, , ICICss, , GoalsGoals>>

SEKB: conoscenza dinamica associata alla societa`:– History (HAP): insieme di eventi sociali accaduti nella societa`, ognuno

rappresentato da fatti ground del tipo: H(Event [,Time] ).

– EXP: aspettative (positive o negative) sul comportamento (sociale) dei membri, ognuna modellata mediante un abducibile:

[¬ ] E( Event [, Time ] ) / [¬ ] EN( Event [, Time ] )

ICs: descrizione dei protocolli mediante vincoli sociali di integrita` SOKB: conoscenza statica associata alla societa` (roles and rules)

– LP clauses with expectations Goals: la societa` puo` essere goal-directed (LP Goals)

SEKB: conoscenza dinamica associata alla societa`:– History (HAP): insieme di eventi sociali accaduti nella societa`, ognuno

rappresentato da fatti ground del tipo: H(Event [,Time] ).

– EXP: aspettative (positive o negative) sul comportamento (sociale) dei membri, ognuna modellata mediante un abducibile:

[¬ ] E( Event [, Time ] ) / [¬ ] EN( Event [, Time ] )

ICs: descrizione dei protocolli mediante vincoli sociali di integrita` SOKB: conoscenza statica associata alla societa` (roles and rules)

– LP clauses with expectations Goals: la societa` puo` essere goal-directed (LP Goals)

Eventi e AspettativeEventi e AspettativeEventi e AspettativeEventi e Aspettative

ICs formalizzano i protocolli in termini di:

– Eventi accaduti (H(..))

– Aspettative relative al comportamento degli agenti al fine di seguire I protocolli (E(..), EN(..))

ICs formalizzano i protocolli in termini di:

– Eventi accaduti (H(..))

– Aspettative relative al comportamento degli agenti al fine di seguire I protocolli (E(..), EN(..))

Happened event H(event,T) Event happened at time T

Expectation E(event,T) Society expects event to happen (at time T)

Negative Expectation NE(event,T) Society expects that event doesn’t

happen

Social infrastructureSocial infrastructureSocial infrastructureSocial infrastructure

Eventi

Fulfillment

Violation

Reasoning VerifyCompliance

YES

NO

Aspettative

(1)verifica on-the fly della conformita` ai protocolli

(1)verifica on-the fly della conformita` ai protocolli

Social Integrity Constraints Social Integrity Constraints (ICs)(ICs)

Social Integrity Constraints Social Integrity Constraints (ICs)(ICs)

permettono la descrizione dei protocolli mediante una sintassi logica basata su regole forward, che possono contenere vincoli CLP sulle variabili.

Esempio: negoziazione di beniSe io ti faccio un'offerta, mi aspetto che tu mi risponda accettando o

rifiutando l'offerta, entro il tempo massimo d

H(tell(Me,You,offer(Item,Price),T) E(tell(You,Me,accept(Item,Price),T’) ^ T’<=T+d ∨E(tell(You,Me,refuse(Item,Price), T’) ^ T’<=T+d’

Se tu accetti la mia offerta, mi aspetto che tu, successivamente, non la rifiuti

H(tell(You,Me,accept(Item,Price), T)

EN(tell(You,Me,refuse(Item,Price), Tr) ^ Tr>=T

permettono la descrizione dei protocolli mediante una sintassi logica basata su regole forward, che possono contenere vincoli CLP sulle variabili.

Esempio: negoziazione di beniSe io ti faccio un'offerta, mi aspetto che tu mi risponda accettando o

rifiutando l'offerta, entro il tempo massimo d

H(tell(Me,You,offer(Item,Price),T) E(tell(You,Me,accept(Item,Price),T’) ^ T’<=T+d ∨E(tell(You,Me,refuse(Item,Price), T’) ^ T’<=T+d’

Se tu accetti la mia offerta, mi aspetto che tu, successivamente, non la rifiuti

H(tell(You,Me,accept(Item,Price), T)

EN(tell(You,Me,refuse(Item,Price), Tr) ^ Tr>=T

Example (fulfillment)Example (fulfillment)Example (fulfillment)Example (fulfillment)

H(tell(yves,thomas,offer(scooter,10$),1) H(tell(yves,thomas,offer(scooter,10$),1)

thomasthomasyvesyves

E(tell(thomas,yves,accept(scooter,10$),T’), T’ < 7

∨ E(tell(thomas,yves,refuse(scooter,10$),T’), T’ < 7

E(tell(thomas,yves,accept(scooter,10$),T’), T’ < 7

∨ E(tell(thomas,yves,refuse(scooter,10$),T’), T’ < 7

H(tell(thomas,yves,accept(scooter,10$),5) H(tell(thomas,yves,accept(scooter,10$),5)

fulfillment!fulfillment!

Esempio di violazioneEsempio di violazioneEsempio di violazioneEsempio di violazione

H(tell(yves,thomas,offer(scooter,10$),1) H(tell(yves,thomas,offer(scooter,10$),1)

thomasthomasyvesyves

H(tell(thomas,yves,accept(Item,Price), T) v

EN(tell(thomas,yves,refuse(Item,Price), Tr), Tr>=T

H(tell(thomas,yves,accept(Item,Price), T) v

EN(tell(thomas,yves,refuse(Item,Price), Tr), Tr>=T

H(tell(thomas,yves,accept(scooter,10$),5) H(tell(thomas,yves,accept(scooter,10$),5)

H(tell(thomas,yves,refuse(scooter,10$),8) H(tell(thomas,yves,refuse(scooter,10$),8)

violazione!violazione!

Istanza di Societa` = Abductive Logic Istanza di Societa` = Abductive Logic ProgramProgram

Istanza di Societa` = Abductive Logic Istanza di Societa` = Abductive Logic ProgramProgram

L'istanza di una Societa` (SHAP) e` modellata mediante un programma logico abduttivo <P,Ab,IC>:– P = SOKB HAP– Ab = {E, EN, ¬ E, ¬ EN}– IC = ICS

Consistenza:– ICS-Consistency– E-Consistency– ¬-Consistency– Fulfillment

L'istanza di una Societa` (SHAP) e` modellata mediante un programma logico abduttivo <P,Ab,IC>:– P = SOKB HAP– Ab = {E, EN, ¬ E, ¬ EN}– IC = ICS

Consistenza:– ICS-Consistency– E-Consistency– ¬-Consistency– Fulfillment

Def: Consistenza, fulfillment e Def: Consistenza, fulfillment e violazioneviolazione

Def: Consistenza, fulfillment e Def: Consistenza, fulfillment e violazioneviolazione

Data una societa` ed un set HAP di eventi:

1. un insieme EXP di aspettative e` ICs-consistent iffSOKB HAP EXP ⊨ ICs

2. un insieme EXP di aspettative e` E-consistent iff{ E(p), EN(p) } ⊈ EXP

3. un insieme EXP di aspettative e` ¬-consistent iff{ E(p), E(p) } ⊈ EXP

{ EN(p), EN(p) } ⊈ EXP

4. un insieme EXP di aspettative (ICs,E,¬) consistent e` fulfilled iffHAP EXP {E(p) → H(p)} {EN(p) → H(p)} ╞

5. se non esiste un insieme di aspettative fulfilled, HAP produce una violazione nella societa`.

Data una societa` ed un set HAP di eventi:

1. un insieme EXP di aspettative e` ICs-consistent iffSOKB HAP EXP ⊨ ICs

2. un insieme EXP di aspettative e` E-consistent iff{ E(p), EN(p) } ⊈ EXP

3. un insieme EXP di aspettative e` ¬-consistent iff{ E(p), E(p) } ⊈ EXP

{ EN(p), EN(p) } ⊈ EXP

4. un insieme EXP di aspettative (ICs,E,¬) consistent e` fulfilled iffHAP EXP {E(p) → H(p)} {EN(p) → H(p)} ╞

5. se non esiste un insieme di aspettative fulfilled, HAP produce una violazione nella societa`.

Society Constraint Proof Procedure Society Constraint Proof Procedure (wrt IFF)(wrt IFF)

Society Constraint Proof Procedure Society Constraint Proof Procedure (wrt IFF)(wrt IFF)

Dato l'insieme HAP di una societa` (history), la proof procedure abduttiva SCIFF (Society Constraint IFF) genera le aspettative corrispondenti agli eventi, ne verifica la consistenza, identificando situazioni di fulfillment o di violazione.

La SCIFF estende la IFF [Fung, Kowalski, 97]

Estensioni (rispetto a IFF): Meccanismo incrementale: accetta nuovi eventi man mano che accadono Genera le aspettative E, not E, EN, not EN in base al comportamento osservato

degli agenti e agli ICs. Verifica la corrispondenza tra gli eventi accaduti e le aspettative (fulfillment) Identifica situazioni di violazione e/o inconsistenza Vincoli CLP Gli atomi abdotti possono avere variabili quantificate esistenzialmente e

universalmente

Dato l'insieme HAP di una societa` (history), la proof procedure abduttiva SCIFF (Society Constraint IFF) genera le aspettative corrispondenti agli eventi, ne verifica la consistenza, identificando situazioni di fulfillment o di violazione.

La SCIFF estende la IFF [Fung, Kowalski, 97]

Estensioni (rispetto a IFF): Meccanismo incrementale: accetta nuovi eventi man mano che accadono Genera le aspettative E, not E, EN, not EN in base al comportamento osservato

degli agenti e agli ICs. Verifica la corrispondenza tra gli eventi accaduti e le aspettative (fulfillment) Identifica situazioni di violazione e/o inconsistenza Vincoli CLP Gli atomi abdotti possono avere variabili quantificate esistenzialmente e

universalmente

Implementazione dell'infrastruttura sociale: Implementazione dell'infrastruttura sociale:

SOCS-SISOCS-SIImplementazione dell'infrastruttura sociale: Implementazione dell'infrastruttura sociale:

SOCS-SISOCS-SI Implementa la SCIFF proof procedure Interfaccia utente Gestione/visualizzazione della societa`: membri,

protocolli, history, aspettative Monitor degli eventi sociali verifica di conformita`

Implementa la SCIFF proof procedure Interfaccia utente Gestione/visualizzazione della societa`: membri,

protocolli, history, aspettative Monitor degli eventi sociali verifica di conformita`

Medium Layer File System Prompt >

User DefinedProtocols

Society Infrastructure

Society ModuleSociet

yGUI

Module

User

Un caso applicativo: Un caso applicativo: specifica e verifica di linee guida in specifica e verifica di linee guida in

campo medicocampo medico

Un caso applicativo: Un caso applicativo: specifica e verifica di linee guida in specifica e verifica di linee guida in

campo medicocampo medico Linee guida: raccomandazioni di comportamento clinico prodotte allo

scopo di assistere medici e pazienti nella decisione delle modalità assistenziali più appropriate in determinate situazioni cliniche.

Distribuzione e Complessita`: molti attori, eterogeneita`, concorrenza, necessita` di sincronizzazione

Importanza di specifica e verifica Specifica mediante ICs:

H(misura_temp(Med,Paz,T)) ^ T>=38

E(somministra(Inf,Paz,paracetamolo)) ^ E(registra(Inf2,Paz,T)).

Necessita` di formalismi piu` intuitivi GOSPEL

Linee guida: raccomandazioni di comportamento clinico prodotte allo scopo di assistere medici e pazienti nella decisione delle modalità assistenziali più appropriate in determinate situazioni cliniche.

Distribuzione e Complessita`: molti attori, eterogeneita`, concorrenza, necessita` di sincronizzazione

Importanza di specifica e verifica Specifica mediante ICs:

H(misura_temp(Med,Paz,T)) ^ T>=38

E(somministra(Inf,Paz,paracetamolo)) ^ E(registra(Inf2,Paz,T)).

Necessita` di formalismi piu` intuitivi GOSPEL

GOSPELGOSPELGOSPELGOSPEL

Guideline prOcess SPEcification Language Linguaggio grafico, basato sul paradigma dei flow-chart,

per– Specificare un processo

– Verificare se i partecipanti si comportano secondo specifica

La verifica è possibile grazie alla traduzione di un diagramma GOSPEL in un insieme di vincoli sociali di integrità

Guideline prOcess SPEcification Language Linguaggio grafico, basato sul paradigma dei flow-chart,

per– Specificare un processo

– Verificare se i partecipanti si comportano secondo specifica

La verifica è possibile grazie alla traduzione di un diagramma GOSPEL in un insieme di vincoli sociali di integrità

Livello epistemologicoLivello epistemologicoLivello epistemologicoLivello epistemologico

Graficamente, GOSPEL permette di esprimere i concetti fondamentali per la modellazione di un processo

Elementi:– Attività atomiche e complesse– Punti di decisione– Sezioni di concorrenza

Relazioni binarie fra elementi:– D’ordine (eventualmente associate a guardie logiche)– Temporali (vincoli sulle attività)

Graficamente, GOSPEL permette di esprimere i concetti fondamentali per la modellazione di un processo

Elementi:– Attività atomiche e complesse– Punti di decisione– Sezioni di concorrenza

Relazioni binarie fra elementi:– D’ordine (eventualmente associate a guardie logiche)– Temporali (vincoli sulle attività)

Attività complesseAttività complesseAttività complesseAttività complesse

Tipico approccio top-down utilizzando i macroblocchi– Visti al livello in cui vengono inseriti come attività atomiche– Incapsulano la definizione di un nuovo (sotto)processo

I macroblocchi dicono anche quali sono le modalità di esecuzione del sottoprocesso

– Azione complessaesecuzione lineare– Iterationesecuzione ciclica tipo for– Whileesecuzione ciclica tipo do…while

GOSPEL pone particolare attenzione alla riusabilità dei macroblocchi

– I processi modellati possono essere riutilizzati per costruirne di nuovi

Tipico approccio top-down utilizzando i macroblocchi– Visti al livello in cui vengono inseriti come attività atomiche– Incapsulano la definizione di un nuovo (sotto)processo

I macroblocchi dicono anche quali sono le modalità di esecuzione del sottoprocesso

– Azione complessaesecuzione lineare– Iterationesecuzione ciclica tipo for– Whileesecuzione ciclica tipo do…while

GOSPEL pone particolare attenzione alla riusabilità dei macroblocchi

– I processi modellati possono essere riutilizzati per costruirne di nuovi

Livello ontologicoLivello ontologicoLivello ontologicoLivello ontologico

Tramite un’ontologia di dominio specifichiamo l’interpretazione di un diagramma GOSPEL nel dominio di interesse

GOSPEL non definisce un’ontologia a priori:– Linguaggio general purpose

– L’ontologia diventa un parametro del modello

– Di volta in volta ci si può calare su differenti domini applicativi

Due grandi tassonomie: attività e entità (partecipanti)

Tramite un’ontologia di dominio specifichiamo l’interpretazione di un diagramma GOSPEL nel dominio di interesse

GOSPEL non definisce un’ontologia a priori:– Linguaggio general purpose

– L’ontologia diventa un parametro del modello

– Di volta in volta ci si può calare su differenti domini applicativi

Due grandi tassonomie: attività e entità (partecipanti)

Un esempioUn esempioUn esempioUn esempio

il medico misura la temperatura del

paziente

il paziente va trattenuto

il paziente va rilasciato

un’infermieraregistra il valore

un’infermiera somministra

paracetamolo

STOPSTOP

se la temperatura è superiore a 38 gradi

altrimenti

il medico decideche...

Action

misura_temp

Entity

Temperatura

PazienteMedico

GOSPELGOSPEL

Integrity Constraints (ICs)Integrity Constraints (ICs)

procedura di traduzione

Procedura di traduzioneProcedura di traduzioneProcedura di traduzioneProcedura di traduzione

visita il diagramma visita il diagramma individuando la individuando la

prossima finestraprossima finestra

estrai un estrai un elemento dalla elemento dalla

frontierafrontiera

metti lo start del metti lo start del processo nella processo nella

frontierafrontiera

genera le genera le regole per regole per la finestrala finestra

aggiorna la aggiorna la frontierafrontiera

FinestreFinestreFinestreFinestre

blocco di start evento di start

blocco di azione evento “ontologico”

blocco di end evento di end

Traduzione di una finestraTraduzione di una finestraTraduzione di una finestraTraduzione di una finestra

H(e1)H(e1)

E(e2)E(e2)

E(e3)E(e3) E(e4)E(e4)

E(e5)E(e5) E(e6)E(e6)

/\/\

\/\/

\/\/

H(e1)H(e1)--->--->E(e2)E(e2)\/E(e3)\/E(e3)\/E(e4)\/E(e4)\/E(e5)/\E(e6)\/E(e5)/\E(e6)

Un esempioUn esempioUn esempioUn esempio

T38

T<38H(misura_temp(Med,Paz,T))H(misura_temp(Med,Paz,T))/\T<38/\T<38--->--->E(trattieni(Med,Paz))E(trattieni(Med,Paz))\/ E(rilascia(Med,Paz))\/ E(rilascia(Med,Paz))

H(misura_temp(Med,Paz,T))H(misura_temp(Med,Paz,T))/\T>=38/\T>=38--->--->E(somministra(Inf,Paz,paracetamolo))E(somministra(Inf,Paz,paracetamolo))/\ E(registra(Inf2,Paz,T))./\ E(registra(Inf2,Paz,T)).

Work in progressWork in progressWork in progressWork in progress

Lato specifica: editor (in via di sviluppo)– Progettazione grafica– Controlli di consistenza– Integrazione con Protégé per le ontologie

Lato verifica:– Verifica statica di proprietà (esiste una history conforme al

modello?)– Verifica di conformità in tempo reale

• Traduzione• Esecuzione…

Lato specifica: editor (in via di sviluppo)– Progettazione grafica– Controlli di consistenza– Integrazione con Protégé per le ontologie

Lato verifica:– Verifica statica di proprietà (esiste una history conforme al

modello?)– Verifica di conformità in tempo reale

• Traduzione• Esecuzione…

ComplianceVerificationlayer

IntegrazioneIntegrazioneIntegrazioneIntegrazione

triggerstriggers

GOSPEL model

configuration

translation

DatabaseLayer

LegacyApplications