Transcript Validating Distributed Object & Component Designs

Validating Distributed Object &
Component Designs
Wolfgang Emmerich and Nima Kaveh
London Software Systems
University College London
http://www.cs.ucl.ac.uk/lss
{n.kaveh|w.emmerich}@cs.ucl.ac.uk
© 2003 Wolfgang Emmerich
1
Outline
 Distributed Systems
 Middleware
 Advanced Communication in Object and
Component Middleware
 Design Issues for Distributed Objects and
Components
 Design Validation using Model Checking
 Conclusions
© 2003 Wolfgang Emmerich
2
Distributed System Example
© 2003 Wolfgang Emmerich
3
What is a Distributed System?
Component1
Componentn
Middleware
Network Operating System
Hardware
Component1
Componentn
Middleware
Network Operating System
Hardware
Hostn-1
Host2
Component1
Componentn
Middleware
Network Operating System
Hardware
Host1
© 2003 Wolfgang Emmerich
Network
Component1
Componentn
Middleware
Network Operating System
Hardware
Hostn
4
What is a Distributed System?
 A distributed system is a collection of
autonomous hosts that that are connected
through a computer network. Each host
executes components and operates a
distribution middleware, which enables the
components to coordinate their activities in such
a way that users perceive the system as a
single, integrated computing facility.
© 2003 Wolfgang Emmerich
5
Abstraction from network protocols
Network protocols do not provide right
abstractions for building distributed systems:
 Packet forwarding vs. procedure call
 Mapping of request parameters to byte streams
 Resolution of data heterogeneity
 Identification of components
 Implementation of component activation
 Type safety
 Synchronization of interaction between distributed
components
 Quality of service guarantees
© 2003 Wolfgang Emmerich
6
Outline
 Distributed Systems
 Middleware
 Advanced Communication in Object and
Component Middleware
 Design Issues for Distributed Objects and
Components
 Design Validation using Model Checking
 Conclusions
© 2003 Wolfgang Emmerich
7
Middleware
 Layered between Application and OS/Network
 Makes distribution transparent
 Resolves heterogeneity of
 Hardware
 Operating Systems
 Networks
 Programming Languages
 Provides development and run-time
environment for distributed systems.
© 2003 Wolfgang Emmerich
ISO/OSI Reference Model
Application
Presentation
Session
Middleware
Transport
Network
Network Operating System
Data link
Physical
© 2003 Wolfgang Emmerich
9
Forms of Middleware
 Transaction-Oriented
 IBM CICS
 BEA Tuxedo
 Encina
 Message-Oriented
 IBM MQSeries
 DEC Message Queue
 NCR TopEnd
 RPC Systems
 Object-Oriented
 OMG/CORBA
 DCOM
 Java/RMI
 Distributed-Components
 J2EE
 .NET
 CCM
 ANSA
 Sun ONC
 OSF/DCE
© 2003 Wolfgang Emmerich
10
Remote Procedure Calls
 Enable procedure calls across host boundaries
 Call interfaces are defined using an Interface
Definition Language (IDL)
 RPC compiler generates presentation and
session layer implementation from IDL
© 2003 Wolfgang Emmerich
11
Local vs. Remote Procedure Call
Caller
Caller
Caller
Called
Stub
Called
Stub
Transport Layer (e.g. TCP or UDP)
© 2003 Wolfgang Emmerich
IDL Example (Unix RPCs)
const NL=64;
struct Customer {
struct DoB {int day; int month; int year;}
string name<NL>;
};
program TRADERPROG {
version TRADERVERSION {
void PRINT(Customer)=0;
int STORE(Customer)=1;
Customer LOAD(int)=2;
}= 0;
} = 105040;
© 2003 Wolfgang Emmerich
13
Presentation Layer
 Resolve data heterogeneity
 Common data representation
 Transmission of data declaration
 Map complex data structures to network
transport
 Static marshalling/unmarshalling
 Dynamic marshalling/unmarshalling
© 2003 Wolfgang Emmerich
14
Marshalling and Unmarshalling
char * marshal() {
char * msg;
msg=new char[4*(sizeof(int)+1) +
 Marshalling: Disassemble
strlen(name)+1];
sprintf(msg,"%d %d %d %d %s",
data structures into
dob.day,dob.month,dob.year,
transmittable form
strlen(name),name);
return(msg);
};
void unmarshal(char * msg) {
int name_len;
sscanf(msg,"%d %d %d %d ",
 Unmarshalling:
&dob.day,&dob.month,
&dob.year,&name_len);
Reassemble the
= new char[name_len+1];
complex data structure. name
sscanf(msg,"%d %d %d %d %s",
&dob.day,&dob.month,
&dob.year,&name_len,name);
© 2003 Wolfgang Emmerich
15
};
Stubs
 Creating code for marshalling and unmarshalling
is tedious and error-prone.
 Code can be generated fully automatically from
interface definition.
 Code is embedded in stubs for client and server.
 Client stub represents server for client, Server
stub represents client for serve.
 Stubs achieve type safety.
 Stubs also perform synchronization.
© 2003 Wolfgang Emmerich
16
Type Safety
 How can we make sure that
 servers are able to perform operations requested by
clients?
 actual parameters provided by clients match the
expected parameters of the server?
 results provided by the server match the
expectations of client?
 Middleware acts as mediator between client and
server to ensure type safety.
 Achieved by interface definition in an agreed
language.
© 2003 Wolfgang Emmerich
17
Facilitating Type Safety
Request
Client
Server
Reply
Interface
Definition
© 2003 Wolfgang Emmerich
18
Synchronization
 What should client do while server executes
 Wait?
 Not care?
 Proceed concurrently and re-synchronise later?
 What should server do if clients request
operations concurrently
 Process them sequentially?
 Process them concurrently?
 Each of these reasonable
 Most supported by middleware primitives
© 2003 Wolfgang Emmerich
19
Outline
 Distributed Systems
 Middleware
 Advanced Communication in Object and
Component Middleware
 Design Issues for Distributed Objects and
Components
 Design Validation using Model Checking
 Related Work
 Conclusions
© 2003 Wolfgang Emmerich
20
Policies & Primitives
 Mainstream object middleware provides few
primitives and policies
 Threading Policies (Server-side):
 Single Threaded
 Multi Threaded
 Synchronization Primitives (Client-side):
 Synchronous Requests
 Deferred Synchronous Requests
 One-way Requests
 Asynchronous Requests
© 2003 Wolfgang Emmerich
21
Server-side threading policies
 Multiple client objects can request operations from
servers concurrently
 What to do?
 Options:
 Queue requests and process them sequentially
 Start new concurrent threads for every request
 Use a thread-pool and assign a thread to each new request
 To relieve programmer of server object:
 Server-side threading implemented in object adapters
 POA in CORBA
 SCM in COM
 EJB Container in J2EE
© 2003 Wolfgang Emmerich
22
CORBA Architecture
Object Implementation
Client
Dynamic
Invocation
Client
Stubs
ORB
Interface
Implementation
Skeletons
POA
ORB Core
One standardised interface
One interface per object operation
One interface per object adapter
ORB-dependent interface
© 2003 Wolfgang Emmerich
POA Threading Policies
 Single-threaded:
 Use when object implementations are not thread safe
 Default threading policy in CORBA
 ORB-controlled:
 Threads to execute object implementations are
started, managed and stopped by the ORB
 Programmer has to be aware that implementations
will be called concurrently and make them thread
safe (e.g. for stateful objects)
 Unspecified how ORB implements thread
management.
© 2003 Wolfgang Emmerich
24
Client-side Synchronisation
Primitives Overview
 Synchronous (Rendevous): Client-blocked until
server finished execution of requested operation
 Oneway: Client continues after request taken by
middleware, no synchronisation happens at all
 Deferred synchronous: Client continues after
request taken by middleware, client polls for
result
 Asynchronous: Client continues after request
taken by middleware and server informs about
the result
© 2003 Wolfgang Emmerich
25
Request Synchronization
 OO-Middleware default: synchronous requests.
:Client
Op()
:Server
 Synchronous requests might block clients
unnecessarily. Examples:
 User Interface Components
 Concurrent Requests from different servers
© 2003 Wolfgang Emmerich
26
Oneway Requests
 Return control to client as soon as request has
been taken by middleware
 Client and server are not synchronized
 Use if
 Server does not produce a result
 Failures of operation can be ignored by client
:Client
:Server
oneway()
© 2003 Wolfgang Emmerich
27
Oneway using Java Threads
class PrintSquad {
static void main(String[] args) {
Team team;
Date date;
// initializations of team and date omitted ...
OnewayReqPrintSquad a=new OnewayReqPrintSquad(team,date);
a.start();
// continue to do work while request thread is blocked...
}
}
// thread that invokes remote method
class OnewayReqPrintSquad extends Thread {
Team team;
Date date;
OnewayReqPrintSquad(Team t, Date d) {
team=t; date=d;
}
public void run() {
team.print(date); // call remote method and then die
}
}
© 2003 Wolfgang Emmerich
28
Oneway requests in CORBA
 Declared statically in the interface definition of
the server object
 IDL compiler validates that
 operation has a void return type
 does not have any out or inout parameters
 does not raise type specific exceptions
 Example:
interface Team {
oneway void mail_timetable(in string tt);
};
© 2003 Wolfgang Emmerich
29
Oneway requests in CORBA
 If oneway declarations cannot be used: Use
dynamic invocation interface
:Client
:Server
r=create_request()
r:Request
send()
Op()
delete()
© 2003 Wolfgang Emmerich
30
Deferred Synchronous Requests
 Return control to client as soon as request has
been taken by middleware
 Client initiates synchronization
 Use if
 Requests take long time
 Client should not be blocked
 Clients can bear overhead of synchronization
:Client
send()
:Request
op()
:Server
get_result()
© 2003 Wolfgang Emmerich
31
Deferred Synchronous Requests with
Threads
class PrintSquad {
public void print(Team t, Date d) {
DefSyncReqPrintSquad a=new DefSyncReqPrintSquad(t,d);
// do something else here.
a.join(this); // wait for request thread to die.
System.out.println(a.getResult()); //get result and print
}
}
// thread that invokes remote method
class DefSyncReqPrintSquad extends Thread {
String s;
Team team;
Date date;
DefSyncReqPrintSquad(Team t, Date d) {team=t; date=d;}
public String getResult() {return s;}
public void run() {
String s;
s=team.asString(date);// call remote method and die
}
}
© 2003 Wolfgang Emmerich
32
CORBA Deferred Synchronous
Requests
 Determined at run-time with using DII
 By invoking send() from a Request object
 And using get_response() to obtain result
:Client
r=create_request(“op”)
send()
:Server
r:Request
op()
get_response()
© 2003 Wolfgang Emmerich
33
Asynchronous Requests
 Return control to client as soon as request has
been taken by middleware
 Server initiates synchronization
 Use if
 Requests take long time
 Client should not be blocked
 Server can bear overhead of synchronization
:Client
op()
© 2003 Wolfgang Emmerich
:Server
34
Asynchronous Requests with
Threads
 Client has interface for callback
 Perform request in a newly created thread
 Client continues in main thread
 New thread is blocked
 Requested operation invokes callback to pass
result
 New thread dies when request is complete
© 2003 Wolfgang Emmerich
35
Asynchronous Requests with
Threads
interface Callback {
public void result(String s);
}
class PrintSquad implements Callback {
public void Print(Team team, Date date){
A=new AsyncReqPrintSquad(team,date,this);
A.start(); // and then do something else
}
public void result(String s){
System.out.print(s);
}
}
class AsyncReqPrintSquad extends Thread {
Team team; Date date; Callback call;
AsyncReqPrintSquad(Team t, Date d, Callback c) {
team=t;date=d;call=c;
}
public void run() {
String s=team.AsString(date);
call.result(s);
}
}
© 2003 Wolfgang Emmerich
36
Asynchronous Requests using
Message Passing
 Message passing is starting to be provided by
object- and component-oriented middleware
 Microsoft Message Queue
 CORBA Notification Service
 Java Messaging Service
 Request and reply explicitly as messages
 Asynchronous requests can be achieved using
two message queues
© 2003 Wolfgang Emmerich
37
Asynchronous Requests using Message
Queues
enter
remove
Request Queue
Client
Server
remove
enter
Reply Queue
© 2003 Wolfgang Emmerich
38
Difference between
Threading and MQs
Threads
 Communication is
immediate
 Do not achieve
guaranteed delivery of
request
 Can be achieved using
language/OS primitives
© 2003 Wolfgang Emmerich
Message Queues
 Buffer Request and Reply
messages
 Persistent storage may
achieve guaranteed
delivery
 Imply additional licensing
costs for Messaging
39
Outline
 Distributed Systems
 Middleware
 Advanced Communication in Object and
Component Middleware
 Design Problems for Distributed Objects and
Components
 Design Validation using Model Checking
 Related Work
 Conclusions
© 2003 Wolfgang Emmerich
40
Design Problems
 Client and server objects execute concurrently
(or even in parallel when residing on different
machines)
 This concurrency gives raise to the usual
problems:
 Deadlocks
 Safety Property violations
 Liveness
© 2003 Wolfgang Emmerich
41
Deadlock Example
© 2003 Wolfgang Emmerich
42
Safety Properties
 Notifications of new price
are sent only in response
to trade update
 Only traders that have
subscribed for
notifications will receive
them
 Equity server cannot
accept new trade unless
notification of previous
trade is complete
© 2003 Wolfgang Emmerich
43
Liveness Properties
 It is always the case that
the EquityServer will
eventually be able to
accept a trade
 Traders will always be
able to eventually enter a
new trade
© 2003 Wolfgang Emmerich
44
Outline
 Distributed Systems
 Middleware
 Advanced Communication in Object and
Component Middleware
 Design Issues for Distributed Objects and
Components
 Design Validation using Model Checking
 Related Work
 Conclusions
© 2003 Wolfgang Emmerich
45
Motivations & Challenges
 Confront complexities by offering developers
design aid
 Complement existing Software Engineering
validation and verification techniques
 Only expose designers to the UML notation they
are likely to be familiar with
 Solution not dependent on any specific semantic
notation
 Build on existing tools and notations
© 2003 Wolfgang Emmerich
46
Approach
 Exploit the fact that object and component
middleware provide only few primitives for
synchronization of distributed objects
 Representation of these primitives as
stereotypes in UML models
 Formal specification of stereotype semantics
 Model checking of UML models against given
safety and liveness properties
© 2003 Wolfgang Emmerich
47
Approach Overview
Stereotype UML
Class & Statechart
diagrams + props.
Process Algebra
Generation
Results – UML
Sequence diagrams
Model Checking
Design Domain
© 2003 Wolfgang Emmerich
Verification Domain
48
Policies & Primitives
 Mainstream object middleware provides few
primitives and policies
 Synchronization Primitives (Client-side):
 Synchronous Requests
 Deferred Synchronous Requests
 One-way Requests
 Asynchronous Requests
 Threading Policies (Server-side):
 Single Threaded
 Multi Threaded
© 2003 Wolfgang Emmerich
49
Approach Overview
Stereotype UML
Class & Statechart
diagrams + props
Process Algebra
Generation
Results – UML
Sequence diagrams
Model Checking
Developer Domain
© 2003 Wolfgang Emmerich
Verification Domain
50
Trading Class Diagram
<<singleThreaded>>
NotificationServer
receiveEquityData()
addTrader()
removeTrader()
myUpdateServer
traders
<<singleThreaded>>
Trader
receiveServerUpdates()
myEquityServer
controller
notifier
<<singleThreaded>>
EquityServer
traders
receiveTraderUpdate()
© 2003 Wolfgang Emmerich
51
Notification Server Statechart
addTrader
removeTrader
idle
receiveEquityData
finishedsendout
preparing
data
reply
sending
© 2003 Wolfgang Emmerich
<<synchronous>>
traders.receiveServerUpdates()
52
Equity Server Statechart
idle
receiveTraderUpdate
reply
update
<<synchronous>>
notifier.receiveEquityData()
updates
completed
© 2003 Wolfgang Emmerich
53
Object Diagram
trader3:Trader
trader2:Trader
trader1:Trader
equityServer1:EquityServer
notifier1:NotificationServer
Used to depict run-time configuration of the system
© 2003 Wolfgang Emmerich
54
User-defined properties
 Designers must specify properties that the
modelled system must adhere to
 Enforce restriction on parallel execution of
state diagram models
 Safety
 Nothing bad happens during execution
 Deadlock, event ordering
 Liveness
 Something good eventually happens
 Eventual termination
© 2003 Wolfgang Emmerich
55
Safety Property
0
EquityServer.receiveTraderUpdate
Trader.receiveServerUpdates
1
NotificationServer.receiveEquityData
2
Specifies action ordering across the three state diagrams
© 2003 Wolfgang Emmerich
56
Liveness Property
<<singleThreaded>>
NotificationServer
myUpdateServer
<<progress>> receiveEquityData()
addTrader()
traders
removeTrader()
<<singleThreaded>>
Trader
<<progress>> receiveServerUpdates()
myEquityServer
controller
notifier
<<singleThreaded>>
EquityServer
traders
<<progress>> receiveTraderUpdate()
Progress evaluates to the temporal logic property of “always eventually”
© 2003 Wolfgang Emmerich
58
Approach Overview
Stereotype UML
Class & Statechart
diagrams + props
Process Algebra
Generation
Results – UML
Sequence diagrams
Model Checking
Developer Domain
© 2003 Wolfgang Emmerich
Verification Domain
59
Process Algebra Generation
 Use Finite State Process algebra (Magee &
Kramer 99) to model object synchronisation
 Finite number of synchronization primitives and
activation policies  Define FSP fragments for all
primitive/policy combinations
 Compose FSP fragments along the combination
of client/server primitives and the object diagram
 Define fragments and composition in OCL.
© 2003 Wolfgang Emmerich
60
Process Algebra Generation
Trading Class Diagram
Equity Server Statechart
<<singleThreaded>>
NotificationServer
idle
controller
receiveTraderUpdate
reply
notifier
<<singleThreaded>>
EquityServer
update
<<synchronous>>
notifier.receiveEquityData()
updates
completed
Combination of single threaded server and synchronous invocation detected
© 2003 Wolfgang Emmerich
61
Application FSP Specification
EQUITYSERVER=(startserver->Idle),
Idle=(receivetraderupdate->Update),
Update=(notifier.receiveequitydata->receiveInvocationReply ->Updatescompleted),
Updatescompleted=(reply->Idle).
NOTIFICATIONSERVER=(startnotificationserver->Idle),
Idle=(receiveequitydata->Preparingdata | addtrader->Idle | removetrader->Idle),
Preparingdata=(reply->Sending),
Sending=(traders.receiveserverupdates->receiveInvocationReply ->Sending |
finishedsendout->Idle).
NOTIFIER_OA =(receiveRequest->relayRequest->receiveReply->relayReply->NOTIFIER_OA).
||TRADING_SYSTEM = (notifier1:NOTIFICATIONSERVER || equityserver1:EQUITYSERVER
|| notificationserverOA:NOTIFIER_OA ) /{
equityserver1.notifier.receiveequitydata / notificationserverOA.receiveRequest,
equityserver1.receiveInvocationReply / notificationserverOA.relayReply,
notifier1.receiveequitydata / notificationserverOA.relayRequest,
© 2003 Wolfgang Emmerich
notifier1.reply
/ notificationserverOA.receiveReply }.
62
User-defined Property FSP
Specification
Safety:
property SFY_1= ({trader1,trader2}.equityServer1.receivetraderupdate->S1),
S1= ({equityServer1}.notifier1.receiveequitydata->S2),
S2= ( {notifier1}.trader1.receiveserverupdates->SFY_1
| {notifier1}.trader2.receiveserverupdates->SFY_1).
Liveness:
progress EQUITYSERVER_PRG={ trader1.equityServer1.receivetraderupdate,
trader2.equityServer1.receivetraderupdate}
progress NOTIFICSERVER_PRG ={equityServer1.notifier1.receiveequitydata }
progress TRADER_PRG = {notifier1.trader1.receiveserverupdates,
notifier1.trader2.receiveserverupdates }
© 2003 Wolfgang Emmerich
63
Approach Overview
Stereotype UML
Class & Statechart
diagrams + props
Process Algebra
Generation
Generate UML
Sequence diagrams
for results
Model Checking
Developer Domain
© 2003 Wolfgang Emmerich
Verification Domain
64
Model Checking
 Generate a Labelled Transition System from
the input process algebra
 Carry out an exhaustive search in state
space of the underlying LTS for action traces
leading to property violations
 In case of violation, produce an action trace
 Trace is used to construct a UML sequence
diagram to show scenario leading to the
property violation
 For liveness violations the sequence diagram
depicts the trace to the terminal set
© 2003 Wolfgang Emmerich
65
Context aware minimization
 Model checking suffers from the state explosion
problem
 Optimisation is achieved by:
 Only modelling the synchronization behaviour of a
middleware application
 Building a state space of transitions in state diagrams
that only correspond to remote requests
Trader
© 2003 Wolfgang Emmerich
TraderOA
66
Approach Overview
Stereotyped UML
Class & Statechart
diagrams + props
Process Algebra
Generation
Results – UML
Sequence diagrams
Model Checking
Developer Domain
© 2003 Wolfgang Emmerich
Verification Domain
67
Relating Results
 Model Checker produces trace in LTS, e.g.:
Trace to DEADLOCK:
trader1.equityServer1.receivetraderupdate
equityServer1.receivetraderupdate
equityServer1.notifier1.receiveequitydata
notifier1.receiveequitydata
notifier1.trader1.receiveserverupdate
trader1.receiveserverupdate
trader1.receiveserverupdates_reply
notifier1.receiveequitydata_reply
equityServer1.receivetraderupdate_reply
trader1.equityServer1.receivetraderupdate
equityServer1.receivetraderupdate
notifier1.trader1.receiveserverupdate
equityServer1.notifier1.receiveequitydata
trader2.equityServer1.receivetraderupdate
© 2003 Wolfgang Emmerich
68
Relating Results
More meaningful in UML notation
trader1:
Trader
equityServer1:
EquityServer
notifier1 :
NotificationServer
receiveTraderUpdate
receiveEquityData
receiveServerUpdates
receiveTraderUpdate
receiveServerUpdates
receiveEquityData
© 2003 Wolfgang Emmerich
69
Tool Support: Architecture
© 2003 Wolfgang Emmerich
70
Tool Support: Design
© 2003 Wolfgang Emmerich
71
Evaluation: Experiment
 How many concurrent objects can we support
 Vary number of traders in architecture below
tradern:Trader
…
trader2:Trader
trader1:Trader
equityServer1:EquityServer
© 2003 Wolfgang Emmerich
notifier1:NotificationServer
72
Evaluation: State Space
© 2003 Wolfgang Emmerich
73
Outline
 Distributed Systems
 Middleware
 Advanced Communication in Object and
Component Middleware
 Design Issues for Distributed Objects and
Components
 Design Validation using Model Checking
 Related Work
 Conclusions
© 2003 Wolfgang Emmerich
74
Some Related Work
 Cheung & Kramer, 1999. Checking Safety
Properties using Compositional Reachability
Analysis, TOSEM 8(1)
 Inverardi et al. 2001. Automated Checking of
Architectural Models using SPIN, ASE 2001.
 McUmber & Cheung, 2001. A general
Framework for formalizing UML with Formal
Languages. ICSE 2001.
© 2003 Wolfgang Emmerich
75
Outline
 Distributed Systems
 Middleware
 Advanced Communication in Object and
Component Middleware
 Design Issues for Distributed Objects and
Components
 Design Validation using Model Checking
 Related Work
 Conclusions
© 2003 Wolfgang Emmerich
76
Conclusions
 Detect synchronisation problems in oomiddleware systems at design
 Define semantics for client/server
communication primitives
 Use model checking to detect potential
execution traces that leading to property
violations
 Confine designers to a pure UML interaction
only
 Introduce no new notations
© 2003 Wolfgang Emmerich
77
Future Work
 Investigate heuristic approaches such as pattern
detection in the UML design diagrams
 Carry out an industrial case study to analyse the
scalability and feasibility of our approach
 Provide semantic mapping to the Promela
(SPIN), to demonstrate the general applicability
of our concepts
© 2003 Wolfgang Emmerich
78