|
DEGAS Edinburgh Review April 2005
General setup
- Have both Choreographer, and Poseidon loaded. Have all files we need
already generated, have no other major programs running.
- At the beginning, Choreographer's Explorer should show a directory
which is completely empty except for the original models
(TomcatAndPDA.zuml and the LySa example ZUML).
- During the demo allow the speaker to point to things using the
laser pointer (rather than the laptop cursor) to avoid e.g. Poseidon's
constant highlighting of boxes and arrows.
- Use the Bird's eye view in Poseidon to zoom in to the diagram
which is being displayed. This will automatically switch to larger
fonts and increase readability. A zoom of 136% seemed good for the
TomcatAndPDA activity diagram. For other things it might be good to
try to position over the yellow box and zoom so that that fills the
pane (reduce the size of the Poseidon explorer if need be).
- For Choreographer use larger fonts in the editors for PEPA, PEPA
nets and LySa and use darker colours in preference to lighter ones.
In particular, avoid light green because this is very hard to read.
Outline of Choreographer demonstration
- Describe Choreographer real estate, explorer, editor, menus, and output
tab.
- Show off the explorer by expanding a file, like PEPA, to show the other
files associated with this one. Show the state, and steadystate files,
perhaps.
- Show off the editor by editing the model, and the syntax highlighting.
Maybe delete a period in a prefix, and re-insert?
- Show the Mobility part of the model in Poseidon.
Show the Activity graph only.
- Run the extractor-solver-reflector combo for mobility.
"Extract PEPA Net", "Generate XML Output", "Load Matrix" , "SolveMatrix",
"Reflect". Pointing out the progress messages displayed in the output tab as
they appear.
- Show the results in Poseidon.
Show the value in the activity graph, and the steady state information which
is hdden in one of the "properties" tabs.
- Show the Performance model in Poseidon.
Show the two state machines and the collaboration diagram. Explain the
Tomcat state machine in more detail.
- Run the extractor-solver-reflector combo on the performance model.
"Extract PEPA", "Check Syntax", "Derive Uncompressed", "Solve
LNBCG", "Reflect".
- Save as TomcatAndPDA.performance.zuml
- Show results in Poseidon.
Show the steady state results in the state machines.
Should see that the Client is waiting about 2.869%
of the time.
- Add the extra association in the Tomcat state machine.
Make it between the states "ProcessRequest" and "SendHTTPResponse". Action
is "locateServlet" at rate(ls).
- Re-run the extractor-solver-reflector combo on the model.
As above.
- Save as TomcatAndPDA.performanceWithServlet.zuml (Note! New
file name!)
- Show the new results in Poseidon.
This time the average response time of Tomcat should decrease, and the amount
of time of the client spent waiting should decrease.
Should see that the Client is now waiting only about 0.499%
of the time.
Show the performace
impact of the modification to the model. Thereby demonstrating that the tool
is can process quickly changes to a UML model and that UML models are
easy to change.
- (Moral: modellers are able to
easily keep their UML presentation consistent with the
formal process algebra code view.)
- (At this point, Stephen hands over to Carlo for the security aspect
of the model.)
- Discuss the Support model, as a framework for protocol modelling for authentication analysis in LySa.
- Discuss the requirements put on the exchange in the Support model, run the tool, and discuss the reported error. Give credits to the piecies, while using them (extractor DIPISA, lysatool IMM, and reflector UEDIN): real integration!
- Derive in real time a new model (Support1), by relaxing the requirements, and show that no errors remain, and no reflection is offered.
- To finish, discuss briefly the protocol used in the case studies, (establish a secure communication between dynamic partners, by exchanging secure certificates) as a useful one also in the Tomcat scenario, and show that the tool is able to capture the errors in the naive exchange (CertificateExchange08) while the sophisticated version with a shared secret (CertificateExchange06) has no errors.
- SessionKeyExchange, Table6, and maybe WMF stay there in case of questions.
- Using Mikael's words the moral is: You can model a protocol; you add some annotation about a security property; you check the property using the tool; sometimes the tool says that the protocol is okay and other times it says that it isn't.
Page maintained by Stephen Gilmore.
Last modified: Fri Apr 1 14:26:46 BST 2005
Validate this page.
|