Modelling and analysing software in mCRL2

J.F. Groote; Jeroen J.A. Keiren; Bas Luttik; Erik P. de Vink; Tim A.C. Willemse

Modelling and analysing software in mCRL2

J.F. Groote, Jeroen J.A. Keiren, Bas Luttik, Erik P. de Vink, Tim A.C. Willemse

Formal System Analysis

Research output: Book/Report › Report › Academic

128 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 language	English
Place of Publication	Eindhoven
Publisher	Technische Universiteit Eindhoven
Number of pages	24
Publication status	Published - Dec 2019

Publication series

Name	Computer Science Reports
Volume	19-05
ISSN (Print)	0926-4515

Access to Document

CSR-19-05Final published version, 482 KB

Fingerprint Dive into the research topics of 'Modelling and analysing software in mCRL2'. Together they form a unique fingerprint.

Cite this

@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 = dec,

language = "English",

series = "Computer Science Reports",

publisher = "Technische Universiteit Eindhoven",

}

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 -