Abstract
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 |
Fingerprint
Cite this
}
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/Report › Report › Academic
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 -