About | Contact Us | Register | Login
ProceedingsSeriesJournalsSearchEAI
Context-Aware Systems and Applications. Second International Conference, ICCASA 2013, Phu Quoc Island, Vietnam, November 25-26, 2013, Revised Selected Papers

Research Article

Formal Modeling and Verification of Context-Aware Systems Using Event-B

Download(Requires a free EAI acccount)
528 downloads
Cite
BibTeX Plain Text
  • @INPROCEEDINGS{10.1007/978-3-319-05939-6_25,
        author={Hong Le and Ninh Truong},
        title={Formal Modeling and Verification of Context-Aware Systems Using Event-B},
        proceedings={Context-Aware Systems and Applications. Second International Conference, ICCASA 2013, Phu Quoc Island, Vietnam, November 25-26, 2013, Revised Selected Papers},
        proceedings_a={ICCASA},
        year={2014},
        month={6},
        keywords={Context awareness Modeling Verification Event-B},
        doi={10.1007/978-3-319-05939-6_25}
    }
    
  • Hong Le
    Ninh Truong
    Year: 2014
    Formal Modeling and Verification of Context-Aware Systems Using Event-B
    ICCASA
    Springer
    DOI: 10.1007/978-3-319-05939-6_25
Hong Le1,*, Ninh Truong2,*
  • 1: University of Mining and Geology
  • 2: VNU - University of Engineering and Technology
*Contact email: anhlh.di10@vnu.edu.vn, thuantn@vnu.edu.vn

Abstract

Context awareness is a computing paradigm that makes applications responsive and adaptive with their environment. Formal modeling and verification of context-aware systems are challenging issues in the development as they are complex and uncertain. In this paper, we propose an approach to use a formal method Event-B to model and verify such systems. First, we specify a context aware system’s components such as context data entities, context rules, context relations by Event-B notions. In the next step, we use the Rodin platform to verify the system’s desired properties such as safety properties. It aims to benefit from natural representation of context awareness concepts in Event-B and proof obligations generated by refinement mechanism to ensure the correctness of systems. We illustrate the use of our approach on a simple example.

Keywords
Context awareness Modeling Verification Event-B
Published
2014-06-19
http://dx.doi.org/10.1007/978-3-319-05939-6_25
Copyright © 2013–2025 ICST
EBSCOProQuestDBLPDOAJPortico
EAI Logo

About EAI

  • Who We Are
  • Leadership
  • Research Areas
  • Partners
  • Media Center

Community

  • Membership
  • Conference
  • Recognition
  • Sponsor Us

Publish with EAI

  • Publishing
  • Journals
  • Proceedings
  • Books
  • EUDL