Software per il mondo aperto
opportunità e sfide
Carlo Ghezzi
Dipartimento di Elettronica e Informazione
Politecnico di Milano, Italy
[email protected]
Venezia--Novembre 2007
1
Che cos'è il "mondo aperto?
• Le metodologie e tecnologie del software sono passate da
una situazione di
– mondo chiuso
– a evoluzione controllata
Il mondo esterno col quale il
– a mondo aperto
sistema
interagisce
è benesterno
noto e fisso
I
cambiamenti
nel
mondo
• Il progresso nel settore può essere analizzato secondo
LaI cambiamenti
struttura della
soluzione
è fissa
ricdhiedono
riprogettazione
si
manifestano
questa visione prospettica
e centralizzata
Imonolitica,
cambiamenti
nell'implementazione
quando il fissa
sistema
è in esecuzione
sono
localizzati evolve
a parti mentre
ristretta
L'architettura
il sistema è in funzione
Venezia--Novembre 2007
2
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
Venezia--Novembre 2007
3
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"
Venezia--Novembre 2007
4
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"
Venezia--Novembre 2007
5
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
Venezia--Novembre 2007
6
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"!
Venezia--Novembre 2007
7
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"
Venezia--Novembre 2007
8
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
Venezia--Novembre 2007
9
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)
Venezia--Novembre 2007
10
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")
Venezia--Novembre 2007
11
OO design
interface
Fax
Polimorfismo
Fax f
body
Fax with phone
-interface
-body
Binding dinamico
f.sendFax();
Venezia--Novembre 2007
12
Binding che attraversa i confini di rete
server
client
RMI
code base
Venezia--Novembre 2007
13
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
Venezia--Novembre 2007
14
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
Venezia--Novembre 2007
15
Che cosa succede oggi?
• Mondo aperto
– livelli mai prima sperimentati di evoluzione
– "perpetual beta"
Venezia--Novembre 2007
16
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
Venezia--Novembre 2007
17
Organizzazioni in rete
Le applicazioni
appartengono a diversi
domini applicativi
Interazioni via web con
proptocolli standard
FOO
LOO
Funzionalit`a offerte da
diversi fornitori che
variano nel tempo
BOO
Esportazione di
applicazioni interne
Venezia--Novembre 2007
MOO
18
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
Venezia--Novembre 2007
19
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
Venezia--Novembre 2007
20
Mondo chiuso
• Nel mondo chiuso esiste una separazione netta tra preruntime e runtime
progetto
verifica
deployment
execuzione
• I cambiamenti si gestiscono ritornando alla fase di
sviluppo, nella quale si effettuano le attività di verifica
Venezia--Novembre 2007
21
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
Venezia--Novembre 2007
22
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"
Venezia--Novembre 2007
23
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?
Venezia--Novembre 2007
24
Discovery-based binding
Service
Specification
Discovery
Agency
Query
Service
Requestor
Requirements
Publish
Service
Provider
Response
Interact
Request
Venezia--Novembre 2007
Service
Specification
Service
25
Implicit binding (P/S)
C1
C2
notifiche
sottoscrizioni
Event Dispatcher
C3
C4
C5
C6
2 sottoscrizioni a "rosso" (C1, C5)
1 sottoscrizione a blu (C6)
Venezia--Novembre 2007
26
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
Venezia--Novembre 2007
27
Un esempio
Dovuto a Carzaniga e Wolf
want
low air fares
to Europe
subscribe
notification
want
special offers
by United
publish
notify
publication
publish/subscribe
service
subscription
want to fly
December
DEN-MXP
United offers
DEN-MXP
October
Alitalia offers
DEN-MXP
Nov-Feb
subscriber
publisher
Venezia--Novembre 2007
28
E-commerce
• TIBCO, ION-MkView, smartsockets
dispatcher
operatori finanziari
(compravendita di
azioni)
gateway verso
altri mercati
componenti applicativi
Venezia--Novembre 2007
29
Spazi di tuple (Linda-like)
C1
C2
invia tupla
Tuple space
legge tupla
via pattern
matching
C3
C4
C5
C6
rimuove tupla
via pattern
matching
read e remove nondeterministiche e bloccanti
Venezia--Novembre 2007
30
Binding by contract
required interface
provided interface
COMPONENT
interfaccia descritta da una
SPECIFICA
La specifica descrive
signature
comportamento funzionale
comportamento nonfunzionale
Bisogna gestire le violazioni di contratto
Venezia--Novembre 2007
31
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
Venezia--Novembre 2007
32
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
Venezia--Novembre 2007
33
Le sfide del mondo aperto
• Vanno ripensate tutte le attività del ciclo di vita
– requisiti
– specifica
– design&implementazione
– verifica&convalida
Venezia--Novembre 2007
34
Zoom-in #1
Dynamic self-adapting service orchestration via BBC
collaborazioni con L. Baresi, D. Bianculli,E. Di Nitto,
S. Guinea, P. Spoletini
Venezia--Novembre 2007
35
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)
Venezia--Novembre 2007
36
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
Venezia--Novembre 2007
37
2 tipi di convalida
1 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
Venezia--Novembre 2007
38
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
Venezia--Novembre 2007
39
Che succede se il contratto è violato?
• Strategie di re-binding
• Comportamenti autonomici
– qui non ne parliamo
Venezia--Novembre 2007
40
Il processo TeleAssistance
receive
while
pick
invoke
switch
panic
button
invoke invoke
"mild" "high"
Venezia--Novembre 2007
41
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
Venezia--Novembre 2007
42
Specifiche nonfunzionali
performance
response
time
throughtput
dependability
reliability
availability
richiedono tempo esplicito e una metrica
la distanza tra tempi
conteggi (negli intervalli di tempo)
Venezia--Novembre 2007
43
ALBERT
Un linguaggio temporale che predica su eventi e durate
Consente di esprimere statement di QoS
Le proprietà sono espresse come invarianti del processo
Sintassi:
Venezia--Novembre 2007
44
Stati
• Semantica espressa con riferimento a sequenze di stati (con timestamp) del processo BPEL
Venezia--Novembre 2007
45
Esempi
• LabServiceTime:
la risposta del lab arriva entro 1 ora dall'invio dei dati del paziente
onEvent(start_analyzeData) → Within(onEvent(end_analyzeData), 60)
• MDCheckUp:
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))
Venezia--Novembre 2007
50
Esecuzione e monitoring via AOP
Venezia--Novembre 2007
51
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
Venezia--Novembre 2007
52
Zoom-in #2
Design and accurate verification of
Publish-Subscribe architectures
joint work with L. Baresi, L. Mottola, L. Zanolin
Venezia--Novembre 2007
53
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
Venezia--Novembre 2007
54
Variety of approaches (1)
• From enterprise to embedded systems
Enterprise
Systems
Sensor
Networks
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
Dynamic
Topologies
Venezia--Novembre 2007
55
Variety of approaches (2)
Different
guarantees
provided
Guarantee
Choices
Message Reliability
Absent, Present
Message Ordering
Random, Pair-wise FIFO, Systemwide 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
…
…
Venezia--Novembre 2007
56
Existing systems
Guarantee
JMS-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
Venezia--Novembre 2007
57
Message ordering
C1
t1: e1
C1
t1: e1
C2
C3
t1: e1
t1: e1
C2
t2: e2
C3
t2: e2
Venezia--Novembre 2007
58
Ordering of events
Total ordering
C1
Hypothesis:
C1 generates e1 for C2, C3
C2 generates e2 and then e3 for C3
e3 generated by C2 as a
consequence of receipt of e1
C2
Causal ordering
C3
e1
C1
C3
e1
e2
e2
e3
e3
Ordering relative to sender
C1
C2
C2
C3
e1
None
C1
C2
C3
e1
e2
e2
e3
e3
Venezia--Novembre 2007
59
A designer's workbench
GOAL: assess design and detect design flaws
prior to moving to implementation
• 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
Venezia--Novembre 2007
60
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
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
Venezia--Novembre 2007
61
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
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
Venezia--Novembre 2007
62
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
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
Allows one to explore the
interplay between application and
comm infrastructure
Venezia--Novembre 2007
63
PubSub APIs
The 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);
Subscriptions
actiondef publish<'a>(PubSubConnection.type<'a>, 'a);
as boolean
actiondef publishWithPriority<'a>(PubSubConnection.type<'a>, 'a,
functions!
MessagePriority);
expdef boolean waitingMessage<'a>(PubSubConnection.type<'a>);
actiondef getNextMessage<'a>(PubSubConnection.type<'a>,
Venezia--Novembre 2007 lazy 'a);
64
Using PubSub APIs
record MyMessage {int value;}
Publishes
a message
MyMessage receivedEvent := new MyMessage;
active thread Publisher() {
MyMessage publishedEvent = new MyMessage;
PubSubConnection.type<MyMessage> ps;
record MyMessage {int value;}
loc loc0: // Connection setup
fun isGreaterThanZero(MyMessage event)
do { ps := PubSubConnection.register<MyMessage>();}
goto loc1;
returns boolean = event.value
0;
loc >loc1:
// Publishing a message
Defines a
do { publishedEvent.value :=subscription
1;
PubSubConnection.publish<MyMessage>(ps,
publishedEvent);}
active thread Subscriber() {
return;
PubSubConnection.type<MyMessage> ps;
Issues a
}
loc loc0: // Connection setup and subscription
(matching)
do { ps := PubSubConnection.register<MyMessage>();
subscription
PubSubConnection.subscribe<MyMessage>(ps,
isGreaterThanZero);}
Receives a
goto loc1;
message
loc loc1: // Message
receive
Venezia--Novembredo
2007{
65
when PubSubConnection.waitingMessage<MyMessage>(ps)
Representing the system state
• Let the system state be described by a tuple:
SystemState = <T1, T2, …, Tn, DispatcherState>
i-th thread (application
component) state
• In turn, let us also define
DispatcherState = <SubTable, RoutingData, M1, M2, …Mn>
Subscriptions
issued
Bookkeeping data to model
specific guarantees
Venezia--Novembre 2007
Messages in
transit
66
Domain-specific model checker
state 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>
Venezia--Novembre 2007
67
Domain-specific model checker
state abstraction - Example 2
• 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>
Venezia--Novembre 2007
68
Domain-specific model checker
state abstraction - Example 3
• Publish-Subscribe often needs to duplicate messages
• Message duplication does not affect the application state
• All supporting data structures hidden in our Bogor
extension
Venezia--Novembre 2007
69
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
Venezia--Novembre 2007
70
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
Publish
Ops.
Bogor w/ PubSub
Memory
Time
SPIN/Promela
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
Venezia--Novembre 2007
71
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
Venezia--Novembre 2007
72
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
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
Select
reliability
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
R1 fails
Venezia--Novembre 2007
73
Verification - Step 2
•
•
•
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
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
Select
CO
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
R3 fails
Venezia--Novembre 2007
74
Verification - Step 3
• R3 also requires the subscription from the fire
brigade to propagate instantaneously
• Unreasonable to assume in a distributed
environment
• Modify the application
Repeat publish
until ACK
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
R3 fails
Venezia--Novembre 2007
75
Verification - Step 4
• 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
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
Select
repliable
messages
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
R2 fails
Venezia--Novembre 2007
76
Verification - Step 5
• R4 (messages … must be delivered with a
maximum delay of five time units) requires
RT
• DSWare already provides it
QuickTime™ and a
TIFF (LZW) decompressor
are needed to see this picture.
R4 succeeds
Venezia--Novembre 2007
77
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
Venezia--Novembre 2007
78
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
Venezia--Novembre 2007
79
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*
Venezia--Novembre 2007
80
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 2007
81