DEGAS: Dancers in violet tutues

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

  1. Describe Choreographer real estate, explorer, editor, menus, and output tab.
    1. 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.
    2. Show off the editor by editing the model, and the syntax highlighting. Maybe delete a period in a prefix, and re-insert?
  2. Show the Mobility part of the model in Poseidon. Show the Activity graph only.
    1. 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.
    2. 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.
  3. Show the Performance model in Poseidon. Show the two state machines and the collaboration diagram. Explain the Tomcat state machine in more detail.
    1. Run the extractor-solver-reflector combo on the performance model. "Extract PEPA", "Check Syntax", "Derive Uncompressed", "Solve LNBCG", "Reflect".
    2. Save as TomcatAndPDA.performance.zuml
    3. 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.
    4. Add the extra association in the Tomcat state machine. Make it between the states "ProcessRequest" and "SendHTTPResponse". Action is "locateServlet" at rate(ls).
    5. Re-run the extractor-solver-reflector combo on the model. As above.
    6. Save as TomcatAndPDA.performanceWithServlet.zuml (Note! New file name!)
    7. 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.
    8. (Moral: modellers are able to easily keep their UML presentation consistent with the formal process algebra code view.)
  4. (At this point, Stephen hands over to Carlo for the security aspect of the model.)
    1. Discuss the Support model, as a framework for protocol modelling for authentication analysis in LySa.
    2. 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!
    3. Derive in real time a new model (Support1), by relaxing the requirements, and show that no errors remain, and no reflection is offered.
    4. 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.
    5. SessionKeyExchange, Table6, and maybe WMF stay there in case of questions.
    6. 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.