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

doi:10.1007/978-3-540-79707-4_14

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

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

4 Citaten (Scopus)

Samenvatting

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.

Originele taal-2	Engels
Titel	Formal Methods for Industrial Critical Systems (12th International Workshop, FMICS 2007, Berlin, Germany, July 1-2, 2007, Revised Selected Papers)
Redacteuren	S. Leue, P. Merino
Plaats van productie	Berlin
Uitgeverij	Springer
Pagina's	182-199
ISBN van geprinte versie	978-3-540-79706-7
DOI's	https://doi.org/10.1007/978-3-540-79707-4_14
Status	Gepubliceerd - 2008

Publicatie series

Naam	Lecture Notes in Computer Science
Volume	4916
ISSN van geprinte versie	0302-9743

Duurzame ontwikkelingsdoelstellingen van de VN

Deze output draagt bij aan de volgende duurzame ontwikkelingsdoelstelling(en)

Toegang tot document

10.1007/978-3-540-79707-4_14

Citeer dit

van Eekelen, M., Hoedt, ten, S., Schreurs, R., & Usenko, Y. S. (2008). Analysis of a session-layer protocol in mCRL2 : verification of a real-life industrial implementation. In S. Leue, & P. Merino (editors), Formal Methods for Industrial Critical Systems (12th International Workshop, FMICS 2007, Berlin, Germany, July 1-2, 2007, Revised Selected Papers) (blz. 182-199). (Lecture Notes in Computer Science; Vol. 4916). Springer. https://doi.org/10.1007/978-3-540-79707-4_14

van Eekelen, Marko ; Hoedt, ten, S. ; Schreurs, R. et al. / Analysis of a session-layer protocol in mCRL2 : verification of a real-life industrial implementation. Formal Methods for Industrial Critical Systems (12th International Workshop, FMICS 2007, Berlin, Germany, July 1-2, 2007, Revised Selected Papers). redacteur / S. Leue ; P. Merino. Berlin : Springer, 2008. blz. 182-199 (Lecture Notes in Computer Science).

@inproceedings{c73fae5de3ca444d8070cc4061128837,

title = "Analysis of a session-layer protocol in mCRL2 : verification of a real-life industrial implementation",

abstract = "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.",

author = "{van Eekelen}, Marko and {Hoedt, ten}, S. and R. Schreurs and Y.S. Usenko",

year = "2008",

doi = "10.1007/978-3-540-79707-4_14",

language = "English",

isbn = "978-3-540-79706-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "182--199",

editor = "S. Leue and P. Merino",

booktitle = "Formal Methods for Industrial Critical Systems (12th International Workshop, FMICS 2007, Berlin, Germany, July 1-2, 2007, Revised Selected Papers)",

address = "Germany",

}

van Eekelen, M, Hoedt, ten, S, Schreurs, R & Usenko, YS 2008, Analysis of a session-layer protocol in mCRL2 : verification of a real-life industrial implementation. in S Leue & P Merino (uitgave), Formal Methods for Industrial Critical Systems (12th International Workshop, FMICS 2007, Berlin, Germany, July 1-2, 2007, Revised Selected Papers). Lecture Notes in Computer Science, vol. 4916, Springer, Berlin, blz. 182-199. https://doi.org/10.1007/978-3-540-79707-4_14

Analysis of a session-layer protocol in mCRL2 : verification of a real-life industrial implementation. / van Eekelen, Marko; Hoedt, ten, S.; Schreurs, R. et al.
Formal Methods for Industrial Critical Systems (12th International Workshop, FMICS 2007, Berlin, Germany, July 1-2, 2007, Revised Selected Papers). uitgave / S. Leue; P. Merino. Berlin: Springer, 2008. blz. 182-199 (Lecture Notes in Computer Science; Vol. 4916).

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

TY - GEN

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

AU - van Eekelen, Marko

AU - Hoedt, ten, S.

AU - Schreurs, R.

AU - Usenko, Y.S.

PY - 2008

Y1 - 2008

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

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

U2 - 10.1007/978-3-540-79707-4_14

DO - 10.1007/978-3-540-79707-4_14

M3 - Conference contribution

SN - 978-3-540-79706-7

T3 - Lecture Notes in Computer Science

SP - 182

EP - 199

BT - Formal Methods for Industrial Critical Systems (12th International Workshop, FMICS 2007, Berlin, Germany, July 1-2, 2007, Revised Selected Papers)

A2 - Leue, S.

A2 - Merino, P.

PB - Springer

CY - Berlin

ER -

van Eekelen M, Hoedt, ten S, Schreurs R, Usenko YS. Analysis of a session-layer protocol in mCRL2 : verification of a real-life industrial implementation. In Leue S, Merino P, redacteurs, Formal Methods for Industrial Critical Systems (12th International Workshop, FMICS 2007, Berlin, Germany, July 1-2, 2007, Revised Selected Papers). Berlin: Springer. 2008. blz. 182-199. (Lecture Notes in Computer Science). doi: 10.1007/978-3-540-79707-4_14

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

Samenvatting

Publicatie series

Duurzame ontwikkelingsdoelstellingen van de VN

Toegang tot document

Vingerafdruk

Citeer dit