Towards Checking Bigraphical Context-Aware Models

Abstract:

Context-aware computing is an important aspect of Pervasive Computing, Cyber-physical Systems (CPS), Cloud computing, etc. Recently, few works have been reported on formal approaches for this area. Bigraph was proposed as a mathematical structure that is consist of two graphs, a place graph and a link graph, intended for modeling distributed, mobile systems, etc. Bigraphs and its corresponding Bigraphical Reactive Systems (BRSs) present a modern, graphical structure, algebra calculus for the description of the syntax and semantics of systems in accordance with the orthogonal notions of connectivity and locality. Bigraphs and BRSs have been applied in various areas. Bigraph is used to formalize context-aware models in this paper. Then, we present an approach to check the formal context-aware models. The formalisms and checking are explicitly depicted through a simple but non-trivial example.

• Periodical: Applied Mechanics and Materials (Volumes 411-414)
• Pages: 545-548
• DOI: https://doi.org/10.4028/www.scientific.net/AMM.411-414.545
• Online since: September 2013
• Authors: Dong Xu, Gang Zhu, De Zhen Xu
• Keywords: Bigraph, Context-Aware, Model Checking

References

[1] R. Milner. The Space and Motion of Communicating Agents. Cambridge University Press, (2009).

[2] Milner, R. Bigraphs and their algebra. Electr. Notes Theor. Comput. Sci. Vol. 209, 24 April 2008, Pages 5-19.

[3] L. Birkedal, S. Debois, E. Elsborg, T. Hildebrandt, and H. Niss. Bigraphical Models of Context-Aware Systems, In: Proc. 9th International Conference on Foundations of Software Science and Computation Structure, Lecture Notes in Computer Science 3921, 187-33201.

DOI: 10.1007/11690634_13

[4] Birkedal, L., Bundgaard, M., Damgaard, T., Debois, S., Elsborg, E., Glenstrup, A., Hildebrandt, T., Milner, R. and Niss, H., Bigraphical programming languages for pervasive computing. In: Proc. International Workshop on Combining Theory and Systems Building in Pervasive Computing , 653-658.

[5] Bundgaard, M. and Hildebrandt, T., Bigraphical semantics of higher-order mobile embedded resources with local names. In: Proc. Workshop on Graph Transformation for Verification and Concurrency, Electronic Notes in Theoretical Computer Science 154, Elsevier, 7-29.

DOI: 10.1016/j.entcs.2005.03.029

[6] Bundgaard, M., Glenstrup, A., Hildebrandt, T., Hojsgaard, E. and Niss, H., Formalising higher-order mobile embedded business processes with binding bigraphs. In: Proc. 10th International Conference on Coordination Languages, Lecture Notes in Computer Science 5052, 83–99.

DOI: 10.1007/978-3-540-68265-3_6

[7] Zhang, M., Shi, L., Zhu, L., Wang, Y., Feng, L. and Pu, F., A bigraphical model of WSBPEL. In: 2nd Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering , IEEE Computer Society, 117-120.

DOI: 10.1109/tase.2008.47

[8] Birkedal, L. and Hildebrandt, T., Bigraphical programming languages. Laboratory for Context-Dependent Mobile Communication, IT University, Denmark. http: /www. itu. dk/research/bpl.

[9] G. Perrone, S. Debois, and T.T. Hildebrandt. A Model Checker for Bigraphs. In ACM Symposium on Applied Computing 2012 – Software Verification and Testing Track. ACM, (2012).

DOI: 10.1145/2245276.2231985

[10] http: /bigraph. org/papers/gcm2012.

[11] M. Weiser, The computer for the 21st Century, Pervasive Computing, IEEE, vol. 99, pp.19-25, (2002).

[12] M. Satyanarayanan, Pervasive computing: vision and challenges, Personal Communications, IEEE, vol. 8, pp.10-17, (2001).

[13] Milner, R., Bigraphical reactive systems. In: Proc. 12th International Con-ference on Concurrency Theory, Lecture Notes in Computer Science 2154, Springer-Verlag, 16C35.

[14] Francois Siewe, Antonio Cau and Hussein Zedan, The Calculus of Context-aware Ambients, Journal of Computer and System Sciences, Volume 77, Issue 4, July 2011, Pages 597-620, JCSS IEEE AINA 2009. Alexander Faithfull, Gian Perrone, and Thomas T. Hildebrandt.

DOI: 10.1016/j.jcss.2010.02.003

[15] Gian Perrone, Soren Debois and Thomas T. Hildebrandt. A verification environment for bigraphs. Innova tions Syst Softw Eng, DOI 10. 1007/s11334-013-0210-2.