Venezia--Novembre 20071 Software per il mondo aperto opportunit à e sfide Carlo Ghezzi Dipartimento...

Venezia--Novembre 2007 1

Software per il mondo apertoopportunità e sfide

Carlo GhezziDipartimento di Elettronica e InformazionePolitecnico di Milano, [email protected]


Che cos'è il "mondo aperto?

• Le metodologie e tecnologie del software sono passate da una situazione di– mondo chiuso– a evoluzione controllata– a mondo aperto

• Il progresso nel settore può essere analizzato secondo questa visione prospettica

Il mondo esterno col quale ilsistema interagisce è ben noto e fissoLa struttura della soluzione è fissamonolitica, fissa e centralizzata

I cambiamenti nel mondo esternoricdhiedono riprogettazioneI cambiamenti nell'implementazionesono localizzati a parti ristretta

I cambiamenti si manifestanoquando il sistema è in esecuzioneL'architettura evolve mentreil sistema è in funzione


Traccia del seminario

• Breve rassegna dell'evoluzione del software dal punto di vista dei concetti di mondo aperto/chiuso

• Analisi delle sfide e opportunità• Zoom su due linee di ricerca• Un'agenda per la ricerca


Postulati

• Il mondo aperto richiede di comporre il software dinamicamente….

• …. in quanto la struttura del software deve poter cambiare dinamicamente, anche in modo imprevisto

• Ciò comporta un cambiamento radicale in come si progetta e convalida il software– in particolare, da una convalida off-lie a una convalida

"perpetua"


Il punto di vista

• Mi focalizzo su composizione/struttura– come viene costruito un sistema da sue parti?

• come/quando si stabiliscono i "binding" tra parti?– quale struttura/architettura?

anche a livello di processo– come è strutturata vita di un'applicazione?– quale organizzazione in fasi/attività/ruoli/attori?

con un occhio al mondo del "business"


Archeologia

• Nascita nel 1968 dell'ingegneria del software, come risposta a – crescente importanza del software nella società– bassa qualità e costi elevati– assenza di metodi standard

• iterazione continua codifica/rimozione di errori


Fatti e ipotesi implicite• Organizzazioni monolitiche

– soluzioni centralizzate• L'ipotesi di mondo chiuso

– i confini tra il mondo reale e la "macchina" sono chiari e fissi

– i requisisti esistono e sono stabili, basta scovarli elicit them right!

– le modifiche sono pericolose• vanno evitate, sono la causa dei problemi di costo e

"schedule"!


Le soluzioni proposte

• A livello di processo– il modello sequenziale a fasi (waterfall)

• raffinamenti dai requisiti al codice• sviluppi top-down via deduzioni formali

• A livello di prodotto– linguaggi e metodi per architetture software statiche,

centralizzate, verificabili• composizioni statiche, congelate a "design time"


Lezioni apprese

• Impossibile stabilire all'inizio i requisiti• I requisiti non possono essere congelati• I requisiti sono intrinsecamente decentrati, illusori il loro

controllo completo e la pre-pianificazione• Quando cambiano, impattano spesso su ogni parte del

prodotto/processo• L'evoluzione è intrinseca al software

– non è un fatto accidentale che capita inatteso dopo il rilascio


Evoluzione controllata• Si deve poter prevedere e controllare l'evoluzione

– con ciò ci si allontana progressivamente dall'ipotesi di mondo chiuso

• A livello di processo – modelli evolutivi

• incrementali, prototipali, a spirale • A livello di prodotto

– Metodi• design for change (Parnas)

– information hiding– specification/interface vs. implementation/body

– Tecnologia e linguaggi• da strutture monolitiche, a modulari e distribuite (client/server)


Evoluzione controllata: linguaggi e metodi OO

• Consentono alcuni tipi di cambiamenti dinamici • Nuove (sotto)classi e oggetti possono essere creati

mentre il sistema è in esecuzione– le operazioni chiamate vengono scelte durante

l'esecuzione• Mondo parzialmente aperto + "type safety"

– se si possono prevedere i cambiamenti e li si possono gestire mediante il meccanismo di ereditarietà, l'evoluzione dinamica può coesistere con la verifica statica ("type safety")


body

interfacePolimorfismo

Fax f

Binding dinamicof.sendFax();

OO designFax

-body

-interface

Fax with phone


Binding che attraversa i confini di rete

clientclient

serverserver

RMIRMI

code basecode base


Componenti: il processo nel mondo aperto

• Sistemi sviluppati a partire da componenti• Mondo aperto per il processo

– sviluppi decentrati– multipli "stakeholder"

• controllo limitato sul processo– integrazione "bottom up" via middleware


Facciamo il punto

• La necessità di adattamento ai cambiamenti esterni– nel mondo del "business"– nel mondo fisico

impone cambiamenti al software• Siamo stati ragionevolmente capaci di rispondere a

questa sfida senza compromettere l'affidabilità delle soluzioni


Che cosa succede oggi?

• Mondo aperto – livelli mai prima sperimentati di evoluzione– "perpetual beta"


Dove sono i motivi del cambiamento? (1)

• Nel mondo del business– organizzazioni agili in rete

• federazioni dinamiche, opportunistiche, goal-oriented• reazioni rapide ai rapidi cambiamenti della domanda• reazioni rapide interne all'organizzazione e nella rete

dei rapporti


Organizzazioni in reteLe applicazioni appartengono a diversi domini applicativi

Interazioni via web conproptocolli standard

BOOBOO BOOBOO

LOOLOO LOOLOO

MOOMOO MOOMOO

FOOFOO FOOFOO

Funzionalit`a offerte da diversi fornitori che variano nel tempo

Esportazione diapplicazioni interne


Dove sono i motivi del cambiamento? (2)

• Mobilità fisica e ubiquitous/ pervasive computing– richiedono binding dinamici e context-aware

• invocazione di un servizio di stampa che si lega alla stampante più vicina

• richiesta di illuminazione che si lega a un attuatore che apre le imposte o all'interruttore della luce elettrica a seconda dellle condizioni di luce esterna


Mondo aperto• I requisiti cambiano in continuazione e in modo imprevedibile• I confini tra il sistema e il mondo esterno non possono essere

congelati– possono cambiare mentre il sistema è in esecuzione

• non possiamo "spegnere il sistema" e riprogettare/ reinstallare/rieseguire

• occorre fornire un servizio senza interruzione

• Le composizioni evolvono perchè possono cambiare sia i components che la loro struttura

• Non esiste una singola "autorità" che ha l'intero sistema a carico


Mondo chiuso

• Nel mondo chiuso esiste una separazione netta tra pre-runtime e runtime

• I cambiamenti si gestiscono ritornando alla fase di sviluppo, nella quale si effettuano le attività di verifica

progettoverificadeploymentexecuzione


Da componenti a servizi

• Entrambi sono sviluppati da "altri"• I componenti sono eseguiti nel dominio dell'applicazione, e ne

diventano parte• I servizi sono eseguiti nei rispettivi domini• Di norma, i componenti vengono scelti e collegati al tempo di

progettazione• Servizi scelti e collegati a run-time• I servizi supportano contratti espliciti per consentire l'uso da parte

di terzi– richiedono un SLA che riguarda non solo gli aspetti funzionali

• I servizi possono essere composti per formare nuovi servizi


Ownership

• Tradizionalmente le applicazioni sono possedute dalle organizzazioni che lo "eseguono"

• Componenti e software di supporto non sono posseduti, ma sono amministrati da chi li esegue– che dipende dal proprietario per le evoluzioni

• I servizi non sono posseduti nè amministrati, ma solo "attivati"


Meccanismi di binding per il mondo aperto

• Esplicito in due fasi– discovery-based

• fase 1: pubblicazione delle proprietà funzionali e non• fase 2: ricerca, scoperta, selezione, con eventuale

ottimizzazione/negoziazione• Implicito

– via uno spazio logico glocale di coordinamento• eventi: publish/subscribe• dati persistenti: tuple space• by contract?


Discovery Agency

Discovery Agency

ServiceProvider

ServiceProvider

ServiceRequest

or

ServiceRequest

orRequirements

ServiceSpecification

Publish

Discovery-based binding



ServiceInteract

Query

RequirementsRequest Response


C3 C4 C5 C6

C1 C2

Event Dispatcher

sottoscrizionisottoscrizioni notifichenotifiche

Implicit binding (P/S)

2 sottoscrizioni a "rosso" (C1, C5)1 sottoscrizione a blu (C6)


Architetture Publish-Subscribe• Comunicazione asincrona mediata da un dispatcher

– anonima – multipoint – implicit addressing

• subject vs. contents-based• I componenti applicativi

– si sottoscrivono a pattern di messaggi a cui sono interessati– pubblicano messaggi

• Il dispatcher esegue un match tra messaggi pubblicati e sottoscrizioni ed esegue il multicast

• Supporto all'aggiunta/rimozione/sostituzione dinamica di componenti


Un esempio

publish/subscribeservice

publish/subscribeservice

wantlow air faresto Europe

wantlow air faresto Europe

want to flyDecemberDEN-MXP

want to flyDecemberDEN-MXP

wantspecial offers

by United

wantspecial offers

by United

subscribe

notify

United offersDEN-MXPOctober

United offersDEN-MXPOctober

Alitalia offersDEN-MXPNov-Feb

Alitalia offersDEN-MXPNov-Feb

publish

subscriber

publisher

subscription

publication

notification

Dovuto a Carzaniga e Wolf


E-commerce• TIBCO, ION-MkView, smartsockets

operatori finanziari (compravendita diazioni)

gateway verso altri mercati

dispatcher

componenti applicativi


Spazi di tuple (Linda-like)

C3 C4 C5 C6

C1 C2

Tuple space

invia tupla

rimuove tupla via pattern matching

legge tupla via pattern matching

read e remove nondeterministiche e bloccanti


Binding by contract

COMPONENTrequired interface provided interface

interfaccia descritta da unaSPECIFICA

La specifica descrive signaturecomportamento funzionale comportamento nonfunzionale

Bisogna gestire le violazioni di contratto


Potenziali benefici

• Chiara separazione tra "what", "how" e "when"– possibili diverse politiche

• early/late• context-aware• ottimizzazione di figure di merito

– legame al "current best"

– "self-organization"– necessaria descrizione semanticamente ricca delle interfacce

• deve descrivere la QoS


BBC per composizione di servizi• La composizione può essere descritta da un workflow, che

specifica una orchestrazione astratta– il workflow viene eseguito dal direttore ch fa da

coordinatore– i servizi esterni sono definiti tramite specifica che

consente BBC– binding a servzi concreti viene fatto dinamicamente


Le sfide del mondo aperto

• Vanno ripensate tutte le attività del ciclo di vita

– requisiti– specifica– design&implementazione– verifica&convalida


Zoom-in #1

Dynamic self-adapting service orchestration via BBCcollaborazioni con L. Baresi, D. Bianculli,E. Di Nitto,

S. Guinea, P. Spoletini


Web service orchestrations

• L'orchestrazione di Web services con BPEL consente di sviluppare servizi complessi per composizione

• BPEL viene esteso per consentire di denotare servizi partner astratti

• Binding a servizi concreti realizzato a run-time, a causa del mondo aperto, poichè– i servizi possono cambiare nel tempo (in meglio o in

peggio)– nuovi servizi si rendono disponibili (e si vuol sfruttare

la loro disponibilità, che può dipendere dal contesto)


Verifica&convalida

+ BBC fornisce flessibilità e dinamismo- BBC richiede perpetua V&V

– late binding+composizione dinamica danno flessibilità al costo di ridotta affidabilità

– l'intero spettro possibile di regimi di binding uno spettro completo di attività di V&V


2 tipi di convalida1 linguaggio

• ALBERT: un linguaggio in logica temporale per processi BPEL– può esprimere proprietà funzionale e non-funzionali– utilizzabile per due tipi di convalida

• design-time (model checking)– si assume che il mondo esterno soddisfi certe proprietà e sulla base

di ciò– si garantisce che valgano certe proprietà del servizio composto

• run-time (monitoring)– si verifica il mantenimento delle proprietà

• Un unico e coerente framework per la convalida


Assume-guarantee

• Un approccio potente alla progettazione e verifica– definire ciò che il mondo esterno deve garantire

• si assume che valga e ci si fida che sia così

– a ciò che a nostra volta dobbiamo garantire• abbiamo naturalmente l'onere della prova che sia davvero

così

• Naturalmente esiste l'onere di prova/check che ciò che si assume riguardo a X sia davvero garantito da X


Che succede se il contratto è violato?

• Strategie di re-binding• Comportamenti autonomici

– qui non ne parliamo


Il processo TeleAssistance

receivewhile

pick

invokeswitch

invoke"mild"

panicbutton invoke"high"


Qualche proprietà

• LabServiceTime: la risposta del lab arriva entro 1 ora dall'invio dei dati del paziente

• FASConfirmHospitalization: se il FAS viene chiamato 3 volte in 1 settimana con severità “High” per un certo paziente, si deve notificare il TA, entro 1 giorno, che il paziente è stato ricoverato

• FASInvokeMildAlarm: dopo la ricezione di un messaggio dal LAB che indica che deve essere mandato un allarme al FAS, TA dve invocare il servizio FAS entro 4 ore, con una severità “Mild” dell'allarme

• MDCheckUp: se un paziente preme pButtonMsg 3 volte in una settimana, il FAS ospedalizza il paziente entro 1 giorno


Specifiche nonfunzionali

performance dependability

responsetime

throughtput reliability availability

richiedono tempo esplicito e una metricala distanza tra tempiconteggi (negli intervalli di tempo)


ALBERTUn linguaggio temporale che predica su eventi e durateConsente di esprimere statement di QoSLe proprietà sono espresse come invarianti del processo

Sintassi:


Stati

• Semantica espressa con riferimento a sequenze di stati (con time-stamp) del processo BPEL


Esempi

• LabServiceTime:

• MDCheckUp:

la risposta del lab arriva entro 1 ora dall'invio dei dati del paziente

se un paziente preme pButtonMsg 3 volte in una settimana, il FAS ospedalizza il paziente entro 1 giorno

x(Becomes(count($alarmNotif/level=`high’ ∧

x = $alarmNotif/pID, onEvent(pButtonMsg), 10080) = 3)

→ Within(onEvent(patHospitalizedMsg) ∧ $patHospitalized/pId=x, 1440))

onEvent(start_analyzeData) → Within(onEvent(end_analyzeData), 60)


Esecuzione e monitoring via AOP


Valutazione di ALBERT a run time

• Per le proprietà che fanno riferimento solo allo stato presente o alla storia passata– la storia è bounded

• Per le proprietà che fanno riferimento al futuro– si genera un nuovo task parallelo, ma ancora si ha

memoria bounded


Zoom-in #2

Design and accurate verification of Publish-Subscribe architectures

joint work with L. Baresi, L. Mottola, L. Zanolin


Premise

• Modern distributed applications for dynamic environments ask for a flexible and reconfigurable software infrastructure

• Publish-Subscribe provides an answer to these needs– fostering an anonymous, implicit, multi-point

communication paradigm• Hard to design and verify "global behavior" of composite

applications– component interactions change dynamically– focus on each reactive component, "global picture" is missing– real-world Publish-Subscribe systems differ along several

dimensions


QuickTime™ and aTIFF (LZW) decompressor

are needed to see this picture.

Enterprise Systems

Dynamic Topologies

Sensor Networks

Variety of approaches (1)

• From enterprise to embedded systems


Variety of approaches (2)

Different guarantees provided

Guarantee Choices

Message Reliability Absent, Present

Message OrderingRandom, Pair-wise FIFO, System-wide FIFO, Causal Order, Total Order

Filtering Precise, Approximate

Real-time Guarantees Absent, Present

Subscription Propagation Delay

Absent, Present

Repliable Messages Absent, Present

Message Priorities Absent, Present

Queue Drop Policy None, Tail Drop, Priority Drop

… …


Existing systems

GuaranteeJMS-compliant[jmsSpec]

REDS [cugola07reds]

DSWare [li04event]

Message Reliability Present Present Absent

Message Ordering Pair-wise FIFO Random Random

Filtering Precise Precise, Approximate Precise

Real-time Guarantees Absent Absent Present

Subscription Propagation Delay Absent Present Present

Repliable Messages Present Present Absent

Message Priorities Present Absent Absent

Queue Drop Policy Priority Drop Tail Drop Tail Drop


Message ordering

C2

C1

C3

t1: e1 t1: e1

t2: e2

C2

C1

C3

t1: e1 t1: e1

t2: e2


Ordering of events

Hypothesis:C1 generates e1 for C2, C3C2 generates e2 and then e3 for C3e3 generated by C2 as a consequence of receipt of e1

C1 C2 C3

Total ordering

e1e2

e3

C1 C2 C3

Causal ordering

e1e2

e3

C1 C2 C3

Ordering relative to sender

e1e2

e3

C1 C2 C3

None

e1e2

e3


A designer's workbench

• Provide a model of the architecture• The model embodies the amount of detail that the

designer wishes to express• The model is verified against certain properties• The model is changed or details are added as needed

GOAL: assess design and detect design flaws prior to moving to implementation


State of the art

• Model checking proposed to address the verification issue – standard tools (e.g., SPIN) used to model both the application and the PubSub

infrastructure (e.g., [garlan03], [baresi ghezzi zanolin03])– fine-grained models unfeasible due to state space explosion– parametric models difficult due to little support for parameterization in the modeling

language

A change of perspective: embed the PubSub communication paradigm within the model-checker






Our solution

• Fine grained parametric models implemented in the model checker– PubSub APIs as primitive constructs of the modeling language

• easier to specify the application model• Domain-specific knowledge can achieve

application- specific state abstraction– addresses the state space explosion problem






Performing the verification





• Specify the application model using the PubSub API• Specify the properties to be checker (LTL)• Select combination of PubSub guarantees the application

relies on• Instantiate the parametric dispatcher within Bogor• Depending on the verification outcome:

– modify the application model– change the guarantees selected

Allows one to explore the interplay between application

and comm infrastructure


PubSub APIsThe PubSub infrastructure is offered as a generic abstract data type

– each instance represents a connection to the PubSub dispatcher– customized w.r.t. the type of messages used by the application– operations are used to issue subscriptions, publish messages, …

typealias MessagePriority int (0,9);

enum DropPolicy {TAIL_DROP, PRIORITY_DROP }extension PubSubConnection for polimi.bogor.bogorps.PubSubModule { typedef type<'a>; expdef PubSubConnection.type<'a> register<'a>(); expdef PubSubConnection.type<'a> registerWithDropping<'a>(int, DropPolicy); actiondef subscribe<'a>(PubSubConnection.type<'a>, 'a -> boolean); actiondef publish<'a>(PubSubConnection.type<'a>, 'a); actiondef publishWithPriority<'a>(PubSubConnection.type<'a>, 'a, MessagePriority); expdef boolean waitingMessage<'a>(PubSubConnection.type<'a>); actiondef getNextMessage<'a>(PubSubConnection.type<'a>, lazy 'a); }

Subscriptions as boolean functions!


Using PubSub APIs

record MyMessage {int value;}

MyMessage receivedEvent := new MyMessage;active thread Publisher() { MyMessage publishedEvent = new MyMessage; PubSubConnection.type<MyMessage> ps; loc loc0: // Connection setup do { ps := PubSubConnection.register<MyMessage>();} goto loc1; loc loc1: // Publishing a message do { publishedEvent.value := 1; PubSubConnection.publish<MyMessage>(ps, publishedEvent);} return;}

Publishes a message

record MyMessage {int value;}

fun isGreaterThanZero(MyMessage event) returns boolean = event.value > 0;

active thread Subscriber() { PubSubConnection.type<MyMessage> ps; loc loc0: // Connection setup and subscription do { ps := PubSubConnection.register<MyMessage>(); PubSubConnection.subscribe<MyMessage>(ps, isGreaterThanZero);} goto loc1; loc loc1: // Message receive when PubSubConnection.waitingMessage<MyMessage>(ps) do { PubSubConnection.getNextMessage<MyMessage>(ps, receivedEvent);} return;}

Issues a (matching)

subscription

Defines a subscription

Receives a message


Representing the system state

• Let the system state be described by a tuple:

• In turn, let us also define

SystemState = <T1, T2, …, Tn, DispatcherState>i-th thread (application

component) state

DispatcherState = <SubTable, RoutingData, M1, M2, …Mn>Subscriptions

issued

Bookkeeping data to model specific guarantees Messages in

transit


Domain-specific model checkerstate abstraction - Example 1

• A message is delivered to an application component if at least one of its subscriptions matches– the order in which subscriptions are examined is immaterial

• We model the subscription table as a set

DispatcherState = <SubTable, RoutingData, M1, M2, …Mn>


• As messages are delivered, bookkeeping information must be stored at the dispatcher to enforce a specific message ordering– from the dispatcher perspective, they change every time a message is

published• From the application perspective, the state of the incoming

queue may be viewed as unchanged even though some messages directed to it have been issued

DispatcherState = <SubTable, RoutingData, M1, M2, …Mn>




• Publish-Subscribe often needs to duplicate messages• Message duplication does not affect the application state• All supporting data structures hidden in our Bogor

extension


More on "why Bogor"

• Multi-point communication feasible also with other tools (e.g., using Promela channels)– cannot model dynamic sender-receiver pairs– cannot be detached to serve a different pair of processes– cannot model fine-grained guarantees


Evaluation

• A set of synthetic scenarios stressing sample PubSub guarantees– 5 threads subscribing to messages coming from another thread

• Comparing against SPIN/Promela [zanolin03approach]

Scenario PublishOps.

Bogor w/ PubSub SPIN/Promela

Memory Time Memory Time

Causal1 2 32.8 Mb 103 sec 298.3 Mb > 15 min

Causal2 5 45.6 Mb 132 sec 589.6 Mb > 1 hour

Causal3 7 52.3 Mb 158 sec OutOfMem NotCompleted

Causal4 10 61.1 Mb 189 sec OutOfMem NotCompleted

Priorities1 2 18.3 Mb 47 sec 192 Mb > 10 min

Priorities2 5 26.9 Mb 103 sec 471.2 Mb > 30 min

Priorities3 7 37.9 Mb 134 sec OutOfMem NotCompleted

Priorities4 10 49.1 Mb 163 sec OutOfMem NotCompleted


Case study

• An application for fire monitoring in a tunnel• Communication patterns expressed as subscriptions• A set of requirements

– R1 - when a truck enters the tunnel, ventilation must increase– R2 - when temperature increases, smoke sensors must be queried– R3 - when temperature increases, notify cs and contact fb to inspect the environment. It

reports to cs which checks that control occurred– R4 - messages from the control station to

command the traffic lights must be delivered with a maximum delay of five time units

• Requirements expressed in LTL• PubSub guarantees initially

set to DSWare


Verification - Step 1





• The initial application model took message reliability for granted

– R1 (ventilation must increase when a truck enters the tunnel) fails immediately

• Message reliability currently investigated in embedded networked systems

– assume it is provided by the communication infrastructure

R1 fails

Select reliability







• R3 (… contact the fire brigade to inspect the environment and report to the control station) fails without causal ordering

• CO is key in safety applications• Push CO in the PubSub infrastructure

R3 fails

Select CO





• R3 also requires the subscription from the fire brigade to propagate instantaneously

• Unreasonable to assume in a distributed environment

• Modify the application

R3 fails

Repeat publish until ACK







• R2 (when temperature increases, smoke sensors must be queried) requires a query reply interaction

• R2 fails because of subscription propagation delays

• Query-reply provided by embedded system middleware

R2 fails

Select repliable

messages







• R4 (messages … must be delivered with a maximum delay of five time units) requires RT

• DSWare already provides it

R4 succeeds


Conclusions• A tool supporting exploration of the design space• Enables exploring the interplay between application and

communication infrastructure • Proposed a change of perspective in the use of model checking

– embed domain specific mechanisms and export them as primitive constructs of the modeling language

• Make fine-grained, parametric models feasible


The end

• Fundamental problems continue to exist in a new and more difficult form– Process level

• combine process agility and product quality– harder for distributed and inter-organization developments

– Product level• requirements and specification• architecture/implementation• verification


Acknowledgements

• Projects SeCSE, Cascadas, Plastic, ArtDeco• People

– L. Baresi, E. Di Nitto, G.P. Picco, G. Cugola, S. Guinea, D. Bianculli, P. Spoletini, L. Mottola … student*


Some papers C. Ghezzi, L. Baresi, E Di Nitto "Towards Open-World Software". Computer, IEEE, Volume 39, Number 10: 36-43, October 2006 L. Baresi, C. Ghezzi, and S. Guinea, "Smart Monitors for Composed Services", 2nd Int.l Conf. on Service Oriented Computing. Nov. 2004 L. Baresi, C. Ghezzi, and S. Guinea "Towards Self-healing Compositions of Services" In Bernd J. Kraemer and Wolfgang A. Halang (eds.)

Contributions to Ubiquitous Computing. Volume 42 of Studies in Computational Intellligence, Springer, 2006 L. Baresi, E. Di Nitto, C. Ghezzi, S. Guinea "A Flexible Framework for the Deployment of Service-Centric Systems", Service Oriented

Computing and Applications, 1, 1, 2007 L. Baresi, D. Bianculli, C. Ghezzi, P. Spoletini. Monitoring Web Service Orchestrations Using Timed WSCoL Proc. of Int.l Conference on

Web Services (ICWS), 2007 D. Bianculli, C. Ghezzi, Monitoring Conversational Web Services, SOSWE 2007. L. Baresi, D. Bianculli, C. Ghezzi, S. Guinea, P. Spoletini. Validation of Web service compositions. To appear on IEE Proceedings Software,

2007 L. Baresi, C. Ghezzi, and L. Mottola "On Accurate Automatic Verification of Publish-Subscribe Architectures", ICSE 2007 D. Bianculli, R. Jurca, W. Binder, C. Ghezzi, B.Faltings. Automated Dynamic Maintenance of Composite Services based on Service

Reputation. In Proc. of Int.l Conf. on Service Oriented Computing (ICSOC), 2007 L. Zanolin, C. Ghezzi, and L. Baresi. "An Approach to Model and Validate Publish/Subscribe Architectures". In Proc. of the SAVCBS03

Workshop, 2003 L. Baresi, C. Ghezzi, and L. Mottola. "Towards Fine-Grained Automated Verification of Publish-Subscribe Architectures". In Proc. of the 26th

Int. Conf. on Formal Methods for Networked and Distributed Systems (FORTE06), 2006 L. Baresi, C. Ghezzi, and L. Mottola. "On Accurate Automatic Verification of Publish-Subscribe Architectures". Proc. of the 29th Int. Conf. on

Software Engineering (ICSE07), 2007 L. Baresi, G. Gerosa, C. Ghezzi, and L. Mottola. "Playing with Time in PublishSubscribe using a DomainSpecific Model Checker". In Proc. of

the SAVCBS03 Workshop, 2007

Venezia--Novembre 20071 Software per il mondo aperto opportunit à e sfide Carlo Ghezzi Dipartimento...

Documents

Transcript of Venezia--Novembre 20071 Software per il mondo aperto opportunit à e sfide Carlo Ghezzi Dipartimento...