Validation Of A Distributed ‘SmartSpace’ Architecture Through Simulation

  • Ian Oliver
Part of the Understanding Complex Systems book series (UCS)


The use of formal methods in software and systems development has advantages but often suffers from difficulty in applying such methods and the visualisation of the results. We show here that the use of a light-weight formal specification language - Alloy - and the use of simulation traces similar to that of scenario explorations with object-diagrams in UML can be effective in understanding the behaviour of such systems at analysis and design-times.


Simulation Validation Formal Specification Alloy 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abrial, J.-R.: The B-Book - Assigning programs to Meanings. Cambridge University Press, Cambridge (1995)Google Scholar
  2. 2.
    Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: UML2Alloy: A Challenging Model Transformation. In: ACM/IEEE 10th International Conference on Model Driven Engineering Languages and Systems (MoDELS) (2007)Google Scholar
  3. 3.
    Andoni, A., Daniliuc, D., Khurshid, S., Marinov, D.: Evaluating the small scope hypothesis (2002)Google Scholar
  4. 4.
    Berners-Lee, T., Hendler, J., Lassila, O.: The Semantic Web. Scientific American 284(5), 34–43 (2001)CrossRefGoogle Scholar
  5. 5.
    Borgida, A., Mylopoulos, J., Reiter, R.: On the Frame Problem in Procedure Specifications. IEEE Transactions on Software Engineering 21(10), 785–797 (1995)CrossRefGoogle Scholar
  6. 6.
    Bussler, C.: A Minimal Triple Space Computing Architecture. In: Proceedings of the 2nd WSMO Implementation Workshop (WIW 2005), Innsbruck, Austria, June 6-7 (2005)Google Scholar
  7. 7.
    Coleman, J., Jones, C., Oliver, I., Romanovsky, E.T.A.: RODIN (Rigorous Open Development Environment for Complex Systems). In: Fifth European Dependable Computing Conference EDCC-5, Budapest (2005)Google Scholar
  8. 8.
    Craigen, D., Kromodimoeljo, S., Meisels, I., Pase, B., Saaltink, M.: EVES: An Overview. In: Prehn, S., Toetenel, H. (eds.) VDM 1991. LNCS, vol. 551. Springer, Heidelberg (1991)Google Scholar
  9. 9.
    Crane, M., Dingel, J.: Runtime Conformance Checking of Objects Using Alloy. In: Third Workshop on Runtime Verification (RV 2003), Boulder, Colorado (July 2003)Google Scholar
  10. 10.
    D’Souza, D.F., Cameron Wills, A.: Object, Components and Frameworks with UML - The Catalysis Approach. Object Technology Series. Addison-Wesley, Reading (1999)Google Scholar
  11. 11.
    Georg, G., Bieman, J., France, R.: Using Alloy and UML/OCL to specify run-time configuration management: a case study. In: Proc. Workshop on Practical UML-Based Rigorous Development Methods — Countering or Integrating the eXtremists (October 2001)Google Scholar
  12. 12.
    Gogolla, M., Richters, M.: Development of UML Descriptions with USE. In: Shafazand, H., Tjoa, A.M. (eds.) EurAsia-ICT 2002. LNCS, vol. 2510, pp. 228–238. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  13. 13.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)zbMATHGoogle Scholar
  14. 14.
    Hui, K.-Y., Chalmers, S., Gray, P., Preece, A.: Experience in Using RDF. In: Agent-mediated Knowledge Architectures, pp. 177–192. Springer, Germany (2004)Google Scholar
  15. 15.
    Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)Google Scholar
  16. 16.
    Jia, X.: A Tutorial of ZANS - A Z Animation System. DePaul University, Chicago, USA (May 1995),
  17. 17.
    Hinchey, M.G., Bowen, J.P.: Seven more myths of formal methods. Software 12(4), 34–41 (1995)CrossRefGoogle Scholar
  18. 18.
    Khushraj, D., Lassila, O., Finin, T.: sTuples: semantic tuple spaces. In: The First Annual International Conference on Mobile and Ubiquitous Systems: Networking and Services, 2004. MOBIQUITOUS 2004, August 22-26, pp. 268–277 (2004)Google Scholar
  19. 19.
    Lassila, O., Adler, M.: Semantic Gadgets: Ubiquitous Computing Meets the Semantic Web. In: Fensel, D., Hendler, J.A., Lieberman, H., Wahlster, W. (eds.) Spinning the Semantic Web: Bringing the World Wide Web to Its Full Potential, pp. 363–376. MIT Press, Cambridge (2003)Google Scholar
  20. 20.
    Leuschel, M., Butler, M.: ProB: A Model Checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)Google Scholar
  21. 21.
    Oliver, I.: Simulation of Software Behaviour using Animation. In: Amborski, K., Meuth, H. (eds.) Proceedings of European Simulation Multiconference, SCS Europe, vol. 4, pp. 278–283 (2002) ISBN 90-77039-07-4Google Scholar
  22. 22.
    Oliver, I.: Experiences in Using B and UML in Industrial Development. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 248–251. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  23. 23.
    Oliver, I.: Experiences of Formal Methods in Conveniontal Software and Systems Design. In: BCS FACS Xmas Workshop: Formal Methods in Industry (December 2007)Google Scholar
  24. 24.
    Oliver, I., Honkola, J.: Sedvice: A Triple Space Computing Exploration Environment. In: Tripcom Workshop, Galway, Ireland, April 28-29 (2008)Google Scholar
  25. 25.
    Wade, S.: An Investigation into the use of the Tuple Space Paradigm in Mobile Computing Environments. Ph.D. thesis, Lancaster University, UK (1999)Google Scholar
  26. 26.
    Christopher Westland, J.: The cost of errors in software development: evidence from industry. The Journal of Systems and Software 62(1), 1–10 (2002)CrossRefGoogle Scholar
  27. 27.
    Zaremba, M., Moran, M.: Enabling Execution of Semantic Web Services: WSMX Core Platform. In: Proceedings of the 1st WSMO Implementation Workshop (WIW 2004) Frankfurt, Germany (2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Ian Oliver
    • 1
  1. 1.Nokia Research CenterHelsinkiFinland

Personalised recommendations