2010
Journal article
Open Access
Modelling interactive experience, function and performance in ubiquitous systems
Harrison M., Massink M.
Computer Science(all) stochastic modelling General Computer Science Ubiquitous computing ubiquitous computing Human computer interaction model checking Interactive systems Theoretical Computer Science Model checking interactive systems human computer interaction Stochastic modelling
The cost of deploying a ubiquitous system to enhance a physical environment is likely to be considerable. The success of its deployment is highly dependent on its context: the physical environment and the activities that are to be carried out within it. This paper provides an initial exploration of whether stochastic process algebras (in particular PEPA with a Fluid Flow semantics) might be used to explore consequences before deployment. The focus of the exploration is to aid understanding of how a proposed system supports users within the environment. The challenge is to provide notations and techniques that will enable the analysis of potentially complex systems.
Source: Electronic notes in theoretical computer science 261 (2010): 23–42. doi:10.1016/j.entcs.2010.01.004
Publisher: Elsevier, Amsterdam , Paesi Bassi
[1] M. Buchenau and J.F. Suri. Experience prototyping. In Proceedings Designing Interactive Systems (DIS'00), pages 424-433, Brooklyn, New York, 2000. ACM Press.
[2] J.C. Campos and M.D. Harrison. Engineering, 8:275-310, 2001.
[3] J.C. Campos and M.D. Harrison. Systematic analysis of control panel interfaces using formal tools. In N. Graham and P. Palanque, editors, Interactive systems: Design, Specification and Verification, DSVIS'08, volume 5136 of Springer Lecture Notes in Computer Science, pages 72-85. Springer-Verlag, 2008.
[4] L. Cardelli and A.D. Gordon. Mobile ambients. In M. Nivat, editor, Foundations of Software Science and Computation Structures, number 1378 in Springer Lecture Notes in Computer Science, pages 140- 155. Springer-Verlag, 1998.
[5] R. De, Nicola, G. L. Ferrari, and R. Pugliese. KLAIM: a kernel language for agents interaction and mobility. IEEE Transactions on Software Engineering, 24(5):315-330, 1998.
[6] A. Degani. Taming HAL: designing interfaces beyond 2001. Palgrave, Macmillan, 2003.
[7] A. Dix, J. Finlay, G. Abowd, and R. Beale. Human Computer Interaction. Pearson Education Ltd., 3 edition, 2004.
[8] D. Garlan, S. Khersonsky, and J.S. Kim. Model checking publish-subscribe systems. In Proceedings of the 10th International SPIN Workshop on Model Checking of Software (SPIN03), Portland, Oregon, 2003.
[9] J. Gow and H.W. Thimbleby. MAUI: An interface design tool based on matrix algebra. In R. J. K. Jacob, Q. Limbourg, and J. Vanderdonckt, editors, Computer Aided Design of User Interfaces IV, CADUI' 2004, pages 81-94, 2004.
[10] M.D. Harrison, M. Massink, and D. Latella. Engineering human flows in smart environments using formal techniques - full version. Technical Report 2009-TR-014, CNR-ISTI, 2009. http://puma.isti.cnr.it/ metadata.php?idcode=2009-TR-014&idcol=1&idauth=1&langver=it.
[11] J. Hillston. Fluid flow approximation of PEPA models. In Proceedings of QEST'05, pages 33-43. IEEE Computer Society, 2005.
[12] J.A. Hillston. A compositional approach to performance modelling. Cambridge University Press, 1996.
[13] G.J. Holzmann. The SPIN Model Checker, Primer and Reference Manual. Addison Wesley, 2003.
[14] C. Kray, G. Kortuem, and A. Kru¨ger. Adaptive navigation support with public displays. In R. St. Amant, J. Riedl, and A. Jameson, editors, Proceedings of IUI 2005, pages 326-328, New York, 2005. ACM Press.
[15] M. Kwiatkowska, G. Norman, and D. Parker. PRISM: Probabilistic symbolic model checker. In T. Field, P.G. Harrison, J. Bradley, and U. Harder, editors, Computer Performance Evaluation: Modelling Techniques and Tools Proceedings 12th International Conference, TOOLS 2002, number 2324 in Springer Lecture Notes in Computer Science, page 200. Springer-Verlag, 2002.
[16] M. Kwiatkowska, G. Norman, and D. Parker. Analysis of a gossip protocol in PRISM. SIGMETRICS Performance Evaluation Review, 36(3):17-22, 2008.
[17] T. McBryan and P. Gray. A model-based approach to supporting configuration in ubiquitous systems. In N. Graham and P. Palanque, editors, Interactive systems: Design, Specification and Verification, DSVIS'08, volume 5136 of Springer Lecture Notes in Computer Science, pages 167-180. SpringerVerlag, 2008.
[18] J McCarthy and P.C. Wright. Technology as Experience. MIT Press, 2004.
[19] R. Milner. Communicating and mobile systems: the pi-calculus. Cambridge University Press, 1999.
[20] Y. Rogers. Moving on from Weiser's vision of calm computing: Engaging UbiComp experiences. In Paul Dourish and Adrian Friday, editors, Proceedings of Ubicomp 2006, pages 404-421, Heidelberg, Berlin, New York, 2006. Springer.
[21] M.B. Rosson and J.M. Carroll. Usability Engineering: scenario-based development of human computer interaction. Morgan Kaufman, 2002.
[22] R. Ruksenas, J. Back, P. Curzon, and A. Blandford. Verification-guided modelling of salience and cognitive load. Formal Aspects of Computing, 2009. DOI: 10.1007/s00165-008-0102-7.
[23] J. Rushby. Using model checking to help discover mode confusions and other automation surprises. Reliability Engineering and System Safety, 75(2):167-177, February 2002.
[24] H.W. Thimbleby. Interaction walkthrough: evaluation of safety critical interactive systems. In G. Doherty and A. Blandford, editors, Interactive Systems: Design, Specification and Verification, number 4323 in Springer Lecture Notes in Computer Science, pages 52-66. Springer-Verlag, 2007.
[25] M. Tribastone. The PEPA plug-in project. In M. Harchol-Balter, M. Kwiatowska, and M. Telek, editors, Proceedings of QEST'07, pages 53-54. IEEE Computer Society Press, 2007.
[2] J.C. Campos and M.D. Harrison. Engineering, 8:275-310, 2001.
[3] J.C. Campos and M.D. Harrison. Systematic analysis of control panel interfaces using formal tools. In N. Graham and P. Palanque, editors, Interactive systems: Design, Specification and Verification, DSVIS'08, volume 5136 of Springer Lecture Notes in Computer Science, pages 72-85. Springer-Verlag, 2008.
[4] L. Cardelli and A.D. Gordon. Mobile ambients. In M. Nivat, editor, Foundations of Software Science and Computation Structures, number 1378 in Springer Lecture Notes in Computer Science, pages 140- 155. Springer-Verlag, 1998.
[5] R. De, Nicola, G. L. Ferrari, and R. Pugliese. KLAIM: a kernel language for agents interaction and mobility. IEEE Transactions on Software Engineering, 24(5):315-330, 1998.
[6] A. Degani. Taming HAL: designing interfaces beyond 2001. Palgrave, Macmillan, 2003.
[7] A. Dix, J. Finlay, G. Abowd, and R. Beale. Human Computer Interaction. Pearson Education Ltd., 3 edition, 2004.
[8] D. Garlan, S. Khersonsky, and J.S. Kim. Model checking publish-subscribe systems. In Proceedings of the 10th International SPIN Workshop on Model Checking of Software (SPIN03), Portland, Oregon, 2003.
[9] J. Gow and H.W. Thimbleby. MAUI: An interface design tool based on matrix algebra. In R. J. K. Jacob, Q. Limbourg, and J. Vanderdonckt, editors, Computer Aided Design of User Interfaces IV, CADUI' 2004, pages 81-94, 2004.
[10] M.D. Harrison, M. Massink, and D. Latella. Engineering human flows in smart environments using formal techniques - full version. Technical Report 2009-TR-014, CNR-ISTI, 2009. http://puma.isti.cnr.it/ metadata.php?idcode=2009-TR-014&idcol=1&idauth=1&langver=it.
[11] J. Hillston. Fluid flow approximation of PEPA models. In Proceedings of QEST'05, pages 33-43. IEEE Computer Society, 2005.
[12] J.A. Hillston. A compositional approach to performance modelling. Cambridge University Press, 1996.
[13] G.J. Holzmann. The SPIN Model Checker, Primer and Reference Manual. Addison Wesley, 2003.
[14] C. Kray, G. Kortuem, and A. Kru¨ger. Adaptive navigation support with public displays. In R. St. Amant, J. Riedl, and A. Jameson, editors, Proceedings of IUI 2005, pages 326-328, New York, 2005. ACM Press.
[15] M. Kwiatkowska, G. Norman, and D. Parker. PRISM: Probabilistic symbolic model checker. In T. Field, P.G. Harrison, J. Bradley, and U. Harder, editors, Computer Performance Evaluation: Modelling Techniques and Tools Proceedings 12th International Conference, TOOLS 2002, number 2324 in Springer Lecture Notes in Computer Science, page 200. Springer-Verlag, 2002.
[16] M. Kwiatkowska, G. Norman, and D. Parker. Analysis of a gossip protocol in PRISM. SIGMETRICS Performance Evaluation Review, 36(3):17-22, 2008.
[17] T. McBryan and P. Gray. A model-based approach to supporting configuration in ubiquitous systems. In N. Graham and P. Palanque, editors, Interactive systems: Design, Specification and Verification, DSVIS'08, volume 5136 of Springer Lecture Notes in Computer Science, pages 167-180. SpringerVerlag, 2008.
[18] J McCarthy and P.C. Wright. Technology as Experience. MIT Press, 2004.
[19] R. Milner. Communicating and mobile systems: the pi-calculus. Cambridge University Press, 1999.
[20] Y. Rogers. Moving on from Weiser's vision of calm computing: Engaging UbiComp experiences. In Paul Dourish and Adrian Friday, editors, Proceedings of Ubicomp 2006, pages 404-421, Heidelberg, Berlin, New York, 2006. Springer.
[21] M.B. Rosson and J.M. Carroll. Usability Engineering: scenario-based development of human computer interaction. Morgan Kaufman, 2002.
[22] R. Ruksenas, J. Back, P. Curzon, and A. Blandford. Verification-guided modelling of salience and cognitive load. Formal Aspects of Computing, 2009. DOI: 10.1007/s00165-008-0102-7.
[23] J. Rushby. Using model checking to help discover mode confusions and other automation surprises. Reliability Engineering and System Safety, 75(2):167-177, February 2002.
[24] H.W. Thimbleby. Interaction walkthrough: evaluation of safety critical interactive systems. In G. Doherty and A. Blandford, editors, Interactive Systems: Design, Specification and Verification, number 4323 in Springer Lecture Notes in Computer Science, pages 52-66. Springer-Verlag, 2007.
[25] M. Tribastone. The PEPA plug-in project. In M. Harchol-Balter, M. Kwiatowska, and M. Telek, editors, Proceedings of QEST'07, pages 53-54. IEEE Computer Society Press, 2007.
Metrics
Back to previous page
BibTeX entry
@article{oai:it.cnr:prodotti:68508,
title = {Modelling interactive experience, function and performance in ubiquitous systems},
author = {Harrison M. and Massink M.},
publisher = {Elsevier, Amsterdam , Paesi Bassi},
doi = {10.1016/j.entcs.2010.01.004},
journal = {Electronic notes in theoretical computer science},
volume = {261},
pages = {23–42},
year = {2010}
}CNR authorsLaboratories
0000-0001-5089-002XCNR ExploRA
DOIAlso available from
DOIAlso available from
