Scalable analysis of collective behaviour in smart service systems

ABSTRACT

The long term vision of smart service systems in which electronic environments are made sensitive and responsive to the presence of, possibly many, people is gradually taking shape through a number of pilot projects. The purposes of such systems vary from intelligent homes that assist their inhabitants to make their lives more independent and comfortable to much larger environments such as airports in which people are provided with context aware, personalised, adaptive and anticipatory services that are most relevant for them given their location and their current activities. This paper is concerned with the exploration of scalable formal models that can address the collective behaviour of a large number of people moving through a smart environment.

References

1. R. Bird. Introduction to Functional Programming using Haskell. Prentice Hall Press, 1998.
2. P. Cairns, M. Jones, and H. Thimbleby. Reusable usability analysis with Markov models. ACM Trans. on Human-Computer Interaction (TOCHI), 8(2): 99--132, 2001.
3. G. Doherty, M. Massink, and G. Faconti. Reasoning about Interactive Systems with Stochastic Models. Interactive Systems: Design, Specification, and Verification (DSVIS01), LNCS 2220, Springer, 2001.
4. D. T. Gillespie. Exact stochastic simulation of coupled chemical reactions. The Journal of Physical Chemistry, 81(25):2340--2361, 1977.
5. S. Gilmore and J. Hillston. The PEPA workbench: A tool to support a process algebra-based approach to performance modelling. In Proc. of the Seventh Int. Conf. on Modelling Techniques and Tools for Computer Performance Evaluation, LNCS 794, pp. 353--368. Springer-Verlag, 1994.
6. M. Harrison, M. Massink, and D. Latella. Engineering crowd interaction within smart environments. In G. Calvary, T. N. Graham, and P. Gray, (Eds.), Proc. of ACM SIGCHI EICS Symp, pp. 117--122. ACM 2009.
7. J. Hillston. A compositional approach to performance modelling. Cambridge University Press, 1996.
8. J. Hillston. Fluid flow approximation of PEPA models. In Proc. of QEST'05, pp. 33--43. IEEE Comp. Soc., 2005.
9. T. M. Kisko, R. L. Francis, and C. R. Nobel. Evacnet4 user's guide, 1998. http://www.ise.ufl.edu/kisko/-files/evacnet/EVAC4UG.HTM.
10. C. Kray, G. Kortuem, and A. Krüger. Adaptive navigation support with public displays. In R. S. Amant, J. Riedl, and A. Jameson (Eds.), Proc. of IUI 2005, pp. 326--328, New York, 2005. ACM Press.
11. M. H. ter Beek, G. P. Faconti, M. Massink, P. Palanque, and M. Winckler. Resilience of Interaction Techniques to Interrupts: A Formal Model-based Approach. In: T. Gross et al. (Eds.), Proc. of INTERACT 2009, Part I, LNCS 5726, pp. 494--509, 2009.
12. G. Santos and B. E. Aguirre. A critical review of emergency evacuation simulation models. In Proc. of the NIST Workshop on Building Occupant Movement during Fire Emergencies, June 10--11, 2004, pp. 27--52. NIST/BFRL Publications Online, Gaithersburg, MD, USA, 2005.
13. A. D. Swain and H. E. Guttmann. Handbook of human reliability analysis with emphasis on nuclear power plant applications - final report. Technical Report NRC FIN A 1188 NUREG/CR-1278 SAND80-0200, Prepared for Division of Facility Operations; Office of Nuclear Regulatory Research; US Nuclear Regulatory Commission; Washington, D.C. 20555, August 1983.
14. M. Tribastone. The PEPA plug-in project. In M. Harchol-Balter, M. Kwiatowska, and M. Telek (Eds.) Proc. of QEST'07, pp. 53--54. IEEE Computer Society Press, 2007.
15. M. Weiser, R. Gold, and J. S. Brown. The origins of ubiquitous computing research at PARC in the late 1980s. IBM Systems Journal, 38(4):693--696, 1999.
16. C. D. Wickens. Engineering Psychology and Human Performance. Charles E. Merrill Publ. Comp., 1984.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Human-centered computing

  • Human computer interaction (HCI)

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification