End-to-end integrated security and performance analysis on the DEGAS Choreographer platform
This page contains the source code and compiled versions of the End-to-end integrated security and performance analysis on the DEGAS Choreographer platform paper.
Status
The paper is to appear in the proceedings of Formal Methods 2005. The deadline for the submitted version of the paper is 2nd May 2005 and the page limit is 16 pages. Please cite this paper as shown in this BibTeX entry for the Choreographer implementation.
Compiled version
Compiled versions of the paper are available as PDF.
| Compiled versions of the paper | ||
| main.pdf | PDF file of the paper generated by pdflatex |
Archive
The files from this Web site are available as a single download in two compressed formats.
| Archive of this Web site | ||
| CHOREOGRAPHER.tar.gz | Gzipped TAR file suitable for Linux | |
| CHOREOGRAPHER.zip | Zip archive suitable for Windows |
Sources
Individual files from the site are listed below in case it is more convenient just to get one of the files instead of all of them.
| LaTeX sources | ||
| main.tex | Root LaTeX document | |
| abstract.tex | Abstract | |
| introduction.tex | Introduction | |
| performance.tex | Describes the performance analysis process using the PEPA language and the PEPA Workbench | |
| protocols.tex | Describes the security analysis process using the LySa language and the LySatool | |
| er.tex | Short description of Extractors and Reflectors | |
| wmf.tex | The demonstration is the wide-mouthed frog example | |
| analysis.tex | Describes the use of Choreographer on the WMF example | |
| softwareengineering.tex | Describes the software engineering issues impacting the development of the DEGAS Choreographer platform | |
| industrialexperience.tex | Describes the experiences as we understand them of the users in Motorola and Omnys | |
| conclusions.tex | Conclusions | |
| acknowledgements.tex | Acknowledgements | |
| BibTeX databases | ||
| main.bib | Bibliography file for the paper | |
| degas.bib | DEGAS bibliography | |
| pepa.bib | PEPA bibliography | |
| security.bib | Security bibliography | |
Screenshots
A repository of screenshots in PNG format of Choreographer and Poseidon is here. This includes screenshots used in the paper as well as others which could be used in slides or overhead foils or elsewhere.
Page maintained by Stephen Gilmore.Last modified: Fri Apr 15 12:48:54 BST 2005
Validate this page.