DEGAS Choreographer paper
This page contains the source code and compiled versions of the DEGAS Choreographer paper. The paper is to appear in the 2nd International Workshop on Web Services and Formal Methods (http://www.cs.unibo.it/~lucchi/ws-fm05/). Deadline for camera-ready copy: June 20, 2005. (Format: 15 pages in LNCS style.)
The Choreographer software is available for download from http://groups.inf.ed.ac.uk/choreographer/
Status
The paper is a draft which has been submitted for publication. Comments are welcome. Please cite this paper as shown in this BibTeX entry for Choreographer.
Compiled version
Two versions of the paper are available: a short version for publication and a long version with more details and motivation. Compiled versions of the paper are available as PDF files.
| Compiled versions of the paper | ||
| main.pdf | PDF file of the paper generated by pdflatex | |
| long.pdf | PDF file of the long version of the paper |
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 with the author (or authors) primarily responsible named beside.
| LaTeX sources | ||
| main.tex | Root LaTeX document | |
| abstract.tex (Stephen) | Abstract | |
| introduction.tex (Stephen) | Introduction | |
| methodology.tex (Stephen) | Describes the DEGAS methodology | |
| choreographer.tex (Stephen and Val) | Overview of Choreographer (with screenshots) | |
| design.tex (Stephen and Val) | The design of Choreographer | |
| implementation.tex (Val and Stephen) | The implementation of Choreographer | |
| casestudy.tex (Leila) | Describes the Motorola case study | |
| uml.tex (Stephen) | Describes the UML model of the Motorola case study and extraction | |
| pepa.tex (Stephen or Leila) | Describes the PEPA language | |
| performance.tex (Leila) | Describes the PEPA model of the Motorola case study | |
| lysa.tex (Monika) | Describes LySa and the LySatool | |
| security.tex (Monika) | Describes the LySa model of the Motorola case study | |
| relatedwork.tex (Stephen) | Related work, mostly integrated security and performance | |
| moreRelatedWork.tex (Monika) | More related work, mostly security | |
| evenMoreRelatedWork.tex (Stephen) | More related work, mostly performance | |
| conclusions.tex | Conclusions | |
| acknowledgements.tex | Acknowledgements | |
| metadata.tex | Describes the specification of the paper | |
| BibTeX databases | ||
| main.bib | Bibliography file for the paper | |
| pepa.bib | PEPA bibliography | |
| security.bib | Security bibliography | |
Last modified: Thu Jun 16 16:17:56 BST 2005
Validate this page.