Specifications used in the following papers:

• Bracciali A., Hillston J., Latella D., Massink M. Reconciling Population and Agent Models for Crowd Dynamics. In Proceedings of Third International Workshop on Logics, Agents, and Mobility. 15 July 2010; Edinburgh, UK. To appear. See also http://web.me.com/farwer/LAM10/LAM10.html and http://www.floc-conference.org/LAM-home.html.
• Massink M., Bracciali A., Latella D., Harrison M., A Scalable Fluid Flow Process Algebraic Approach to Emergency Egress Analysis. In Proceedings of the 8th IEEE International Conference on Software Engineering And Formal Methods (SEFM2010). pp. 169-180. IEEE, 2010.
• Massink M., Latella D., Bracciali A., Harrison M. D., Hillston J., Scalable Context-dependent Analysis of Emergency Egress Models. Formal Aspects of Computing, 2011. To Appear.

The analysis of the case studies discussed in the above papers have been based on the following specifications:

• Full PEPA specification of the three storey building
• Full PEPA specification of the same building with smoke in the landing of the western staircase
• Full PEPA specification of the large building
  

Both specifications have been analysed with the PEPA plugin tool (version 0.10 of 2008) of the University of Edinburgh, for Eclipse Europa on a MAC OS X.

• Full Bio-PEPA specification of floor 3 of the building
• Full Bio-PEPA specification of floor 3 with dynamic routing information provided to evacuees

These specifications have been analysed with the Bio-PEPA plugin tool from the University of Edinburgh, 2010.

Last update: May, 2011