Remember Me
Or use your Academic/Social account:


Or use your Academic/Social account:


You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.


Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message


Verify Password:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Sama, Michele; Raimondi, Franco; Rosenblum, David; Emmerich, Wolfgang (2008)
Publisher: Institute of Electrical and Electronics Engineers
Languages: English
Types: Part of book or chapter of book
Context-aware and adaptive applications running on mobile devices pose new challenges for the verification community. Current verification techniques are tailored for different domains (mostly hardware) and the kind of faults that are typical of applications running on mobile devices are difficult (or impossible) to encode using the patterns of ldquotraditionalrdquo verification domains. In this paper we present how techniques similar to the ones used in symbolic model checking can be applied to the verification of context-aware and adaptive applications. More in detail, we show how a model of a context-aware application can be encoded by means of ordered binary decision diagrams and we introduce symbolic algorithms for the verification of a number of properties.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • [1] R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183-235, April 1994.
    • [2] R. Alur, T. A. Henzinger, and O. Kupferman. Alternatingtime temporal logic. Journal of the ACM, 49(5):672-713, 2002.
    • [3] V. Barr. Applications of rule-base coverage measures to expert system evaluation. In Proc. National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, pages 411 - 416, July 1997.
    • [4] R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transaction on Computers, 35(8):677- 691, 1986.
    • [5] L. Capra, W. Emmerich, and C. Mascolo. Carisma: Contextaware reflective middleware system for mobile applications. IEEE Transactions on Software Engineering, 29(10):29- 945, October 2003.
    • [6] A. Cimatti, E. M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NUSMV2: An open-source tool for symbolic model checking. In Proceedings of the 14th International Conference on Computer Aided Verification (CAV'02), volume 2404 of LNCS, pages 359-364. Springer-Verlag, 2002.
    • [7] E. Clarke, O. Grumberg, K. McMillan, and X. Zhao. Efficient generation of counterexamples and witnesses in symbolic model checking. Technical report, Pittsburgh, PA, USA, 1994.
    • [8] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999.
    • [9] M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. Property specification patterns for finite-state verification. In M. Ardis, editor, Proceedings of the 2nd Workshop on Formal Methods in Software Practice (FMSP'98), pages 7-15, New York, 1998. ACM Press.
    • [10] P. Fahy and S. Clarke. CASS-Middleware for mobile context-aware applications. In Proc. MobiSys Workshop on Context Awareness, pages 304-308, June 2004.
    • [11] J. Floch. Theory of adaptation. Deliverable D2.2, MADAM Project, available from http://www.ist-music.eu/MUSIC/madam-project/madamdeliverables/techreportreference.2007-04-13.0451108510, 2006. Last accessed 7 March 2008.
    • [12] T. Gu, H. K. Pung, and D. Q. Zhang. A middleware for building context-aware mobile services. In Proc. IEEE Vehicular Technology Conference, pages 2656- 2660, May 2004.
    • [13] U. G. Gupta. Automatic tools for testing expert systems. Communications of the ACM, 5:179-184, May 1998.
    • [14] M. P. Heimdahl and N. G. Leveson. Completeness and consistency in hierarchical state-based requirements. IEEE Transactions on Software Engineering, 22(6):363-377, June 1996.
    • [15] C. L. Heitmeyer, R. D. Jeffords, and B. G. Labaw. Automated consistency checking of requirements specifications. ACM Transactions on Software Engineering and Methodology, 5(3):231-261, 1996.
    • [16] G. J. Holzmann. The model checker SPIN. IEEE Trans. on Software Eng., 23(5):279-295, 1997.
    • [17] iscid. http://www.iscid.org/encyclopedia/adaptive system.
    • [18] M. Z. Kwiatkowska, G. Norman, and D. Parker. PRISM: Probabilistic symbolic model checker. In Computer Performance Evaluation / TOOLS, pages 200-204, 2002.
    • [19] A. Lomuscio and F. Raimondi. Model checking knowledge, strategies, and games in multi-agent systems. In Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems (AAMAS'06), pages 161-168, Hakodake, Japan, 2006. ACM Press.
    • [20] H. Lu, W. K. Chan, and T. H. Tse. Testing context-aware middleware-centric programs: A data flow approach and an RFID-based experimentation. In Proc. International Symposium on Foundations of Software Engineering, pages 242- 252, November 2006.
    • [21] K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
    • [22] A. Ranganathan and R. H. Campbell. A middleware for context-aware agents in ubiquitous computing environments. In Proc. ACM/IFIP/USENIX International Middleware Conference, pages 143-161, June 2003.
    • [23] G.-C. Roman, P. J. McCann, and J. Y. Plun. Mobile UNITY: Reasoning and specification in mobile computing. ACM Transactions on Software Engineering and Methodology, 6(3):250 - 282, July 1997.
    • [24] M. Sama and D. Rosenblum. ContextNotifier. http://code.google.com/p/contextnotifier/.
    • [25] M. Sama, D. S. Rosenblum, Z. Wang, and S. Elbaum. Multilayer faults in the architectures of mobile, context-aware adaptive applications: A position paper (Short Paper). In Proc. ICSE 2008 International Workshop on Software Architectures and Mobility, May 2008. Short Paper, to appear.
    • [26] B. Schilit, N. Adams, and R. Want. Context-aware computing applications. In IEEE Workshop on Mobile Computing Systems and Applications, Santa Cruz, CA, US, 1994.
    • [27] F. Somenzi. CUDD: CU decision diagram package - release 2.4.1. http://vlsi.colorado.edu/∼fabio/ CUDD/cuddIntro.html, 2005.
    • [28] T. Tse, S. Yau, W. Chan, H. Lu, and T. Chen. Testing context-sensitive middleware-based software applications. In Proc. International Computer Software and Applications Conference, pages 458-465, September 2004.
    • [29] Z. Wang, S. Elbaum, and D. S. Rosenblum. Automated generation of context-aware tests. In Proc. International Conference on Software Engineering, pages 406-415, May 2007.
  • No related research data.
  • No similar publications.
  • BioEntity Site Name
    Google Code

Share - Bookmark

Funded by projects

  • RCUK | UbiVal: Fundamental Approa...

Cite this article