Algorithms for efficient symbolic detection of faults in context-aware applications.

Part of book or chapter of book English OPEN
Sama, Michele ; Raimondi, Franco ; Rosenblum, David ; Emmerich, Wolfgang (2008)

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.
  • References (29)
    29 references, page 1 of 3

    [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.

  • Software (1)
  • Metrics
    views in OpenAIRE
    views in local repository
    downloads in local repository

    The information is available from the following content providers:

    From Number Of Views Number Of Downloads
    Middlesex University Research Repository - IRUS-UK 0 14
Share - Bookmark