Modelling and verifying IEEE Std 11073-20601 session setup using mCRL2

J.J.A. Keiren, M.D. Klabbers

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

    Samenvatting

    In this paper we advocate that formal verication should be a part of the development of a communication standard; in a short period of time issues are uncovered that have been in the standard for a number of years, and all subtleties in the correctness of the protocol are understood. We model and verify the session setup protocol that is part of the IEEE 11073-20601:2008 standard for communication between personal health devices. We identify a number of issues present in the standards document. Discussion with a member of the standards committee unveiled that most, but not all, of the identified issues are fixed in the IEEE 11073-20601:2010 version of the standard. In addition, the correctness of the protocol, including the fixes, is assessed. For this, properties of the session setup protocol are formulated, and using the model checker mCRL2 it is veried whether the model satises these properties.We show that the session setup protocol is awed, and propose a straightforward way to fix this issue. Keywords: Veri¿cation, model checking, IEEE 11073-20601, protocol standardisation, interoperability
    Originele taal-2Engels
    Titel12th International Workshop on Automated Verification of Critical Systems (AVoCS, Bamberg, Germany, September 18-20, 2012)
    RedacteurenG. Lüttgen, S. Merz
    UitgeverijECEASST
    Pagina's1-16
    StatusGepubliceerd - 2012
    Evenement12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012) - Bamberg, Duitsland
    Duur: 18 sep 201220 sep 2012
    Congresnummer: 12

    Publicatie series

    NaamElectronic Communications of the EASST
    Volume53
    ISSN van geprinte versie1863-2122

    Congres

    Congres12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012)
    Verkorte titelAVoCS 2012
    LandDuitsland
    StadBamberg
    Periode18/09/1220/09/12
    Ander12th International Workshop on Automated Verification of Critical Systems (AVoCS)

    Vingerafdruk Duik in de onderzoeksthema's van 'Modelling and verifying IEEE Std 11073-20601 session setup using mCRL2'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit