Analysis of a session-layer protocol in mCRL2 : verification of a real-life industrial implementation

Marko van Eekelen, S. Hoedt, ten, R. Schreurs, Y.S. Usenko

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    4 Citations (Scopus)


    This paper reports the analysis of an industrial implementation of the session-layer of a load-balancing software system. This software comprises 7.5 thousand lines of C code. It is used for distribution of the print jobs among several document processors (workers). A large part of this commercially used software system has been modeled closely and analyzed using process-algebraic techniques. Several critical issues were discovered. Since the model was close to the code, all problems that were found in the model, could be traced back to the actual code resulting in concrete suggestions for improvement of the code. All in all, the analysis significantly improved the quality of this real-life system. This research was supported by SenterNovem Innovation Voucher Inv053967. The fourth author has also been supported by NWO Hefboom project 641.000.407.
    Original languageEnglish
    Title of host publicationFormal Methods for Industrial Critical Systems (12th International Workshop, FMICS 2007, Berlin, Germany, July 1-2, 2007, Revised Selected Papers)
    EditorsS. Leue, P. Merino
    Place of PublicationBerlin
    ISBN (Print)978-3-540-79706-7
    Publication statusPublished - 2008

    Publication series

    NameLecture Notes in Computer Science
    ISSN (Print)0302-9743


    Dive into the research topics of 'Analysis of a session-layer protocol in mCRL2 : verification of a real-life industrial implementation'. Together they form a unique fingerprint.

    Cite this