• DocumentCode
    258443
  • Title

    Verifying the Precedence Property Pattern Using the B Method

  • Author

    Mammar, Amel ; Frappier, M.

  • Author_Institution
    Inst. Mines-Telecom, Telecom SudParis, Paris, France
  • fYear
    2014
  • fDate
    9-11 Jan. 2014
  • Firstpage
    229
  • Lastpage
    233
  • Abstract
    This paper presents an approach to proving a temporal property pattern of the form Prec(P1, P2) that expresses that if a state, presented by predicate P2, is reached then there should exist a state, in the past, that verifies P1. Such a property pattern is very useful in the specification of various systems such as Information Systems (IS) and security policies. To this aim, we define sufficient and necessary proof obligations that allow to establish such a property.
  • Keywords
    formal verification; security of data; B method; information systems; precedence property pattern verification; security policies; temporal property pattern; Conferences; Educational institutions; Electronic mail; Information systems; Unified modeling language; B Method; Precedence properties; Proofs; Temporal properties; Verification;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    High-Assurance Systems Engineering (HASE), 2014 IEEE 15th International Symposium on
  • Conference_Location
    Miami Beach, FL
  • Print_ISBN
    978-1-4799-3465-2
  • Type

    conf

  • DOI
    10.1109/HASE.2014.40
  • Filename
    6754611
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=258443