Modelling and analysing software in mCRL2

Research output: Book/ReportReportAcademic

8 Downloads (Pure)

Abstract

Model checking is an effective way to design correct software.
Making behavioural models of software, formulating correctness properties using modal formulas, and verifying these using finite state analysis techniques, is a very efficient way to obtain the required insight in the software. We illustrate this on four common but tricky examples.
Original languageEnglish
Place of PublicationEindhoven
PublisherTechnische Universiteit Eindhoven
Number of pages24
Publication statusPublished - Dec 2019

Publication series

NameComputer Science Reports
Volume19-05
ISSN (Print)0926-4515

Fingerprint

Model checking
Software design

Cite this

Groote, J. F., Keiren, J. J. A., Luttik, B., de Vink, E. P., & Willemse, T. A. C. (2019). Modelling and analysing software in mCRL2. (Computer Science Reports; Vol. 19-05). Eindhoven: Technische Universiteit Eindhoven.
Groote, J.F. ; Keiren, Jeroen J.A. ; Luttik, Bas ; de Vink, Erik P. ; Willemse, Tim A.C. / Modelling and analysing software in mCRL2. Eindhoven : Technische Universiteit Eindhoven, 2019. 24 p. (Computer Science Reports).
@book{d763906b895740ed987dd256c787f126,
title = "Modelling and analysing software in mCRL2",
abstract = "Model checking is an effective way to design correct software.Making behavioural models of software, formulating correctness properties using modal formulas, and verifying these using finite state analysis techniques, is a very efficient way to obtain the required insight in the software. We illustrate this on four common but tricky examples.",
author = "J.F. Groote and Keiren, {Jeroen J.A.} and Bas Luttik and {de Vink}, {Erik P.} and Willemse, {Tim A.C.}",
year = "2019",
month = "12",
language = "English",
series = "Computer Science Reports",
publisher = "Technische Universiteit Eindhoven",

}

Groote, JF, Keiren, JJA, Luttik, B, de Vink, EP & Willemse, TAC 2019, Modelling and analysing software in mCRL2. Computer Science Reports, vol. 19-05, Technische Universiteit Eindhoven, Eindhoven.

Modelling and analysing software in mCRL2. / Groote, J.F.; Keiren, Jeroen J.A.; Luttik, Bas; de Vink, Erik P.; Willemse, Tim A.C.

Eindhoven : Technische Universiteit Eindhoven, 2019. 24 p. (Computer Science Reports; Vol. 19-05).

Research output: Book/ReportReportAcademic

TY - BOOK

T1 - Modelling and analysing software in mCRL2

AU - Groote, J.F.

AU - Keiren, Jeroen J.A.

AU - Luttik, Bas

AU - de Vink, Erik P.

AU - Willemse, Tim A.C.

PY - 2019/12

Y1 - 2019/12

N2 - Model checking is an effective way to design correct software.Making behavioural models of software, formulating correctness properties using modal formulas, and verifying these using finite state analysis techniques, is a very efficient way to obtain the required insight in the software. We illustrate this on four common but tricky examples.

AB - Model checking is an effective way to design correct software.Making behavioural models of software, formulating correctness properties using modal formulas, and verifying these using finite state analysis techniques, is a very efficient way to obtain the required insight in the software. We illustrate this on four common but tricky examples.

M3 - Report

T3 - Computer Science Reports

BT - Modelling and analysing software in mCRL2

PB - Technische Universiteit Eindhoven

CY - Eindhoven

ER -

Groote JF, Keiren JJA, Luttik B, de Vink EP, Willemse TAC. Modelling and analysing software in mCRL2. Eindhoven: Technische Universiteit Eindhoven, 2019. 24 p. (Computer Science Reports).