Download User Manual: Model Checking - Software and Systems Engineering

Validas Model Checking for AutoFOCUS
Contents:
1
Introduction .............................................................................................................3
2
Installation ...............................................................................................................4
2.1
2.2
3
Models and Properties ..........................................................................................6
3.1
3.2
3.3
3.4
4
Supported Models................................................................................................ 6
Supported Properties ......................................................................................... 7
Property Tags ........................................................................................................ 9
Bounded Model Checking ............................................................................... 10
Using MCUI ............................................................................................................. 12
4.1
5
NuSMV ................................................................................. 4
Cadence SMV ........................................................................ 5
Example................................................................................................................. 13
Available Settings ................................................................................................ 16
5.1
5.2
5.3
5.4
5.5
Model ................................................................................. 16
Properties ........................................................................... 17
Options .............................................................................. 19
Encoding ............................................................................ 20
MSC ................................................................................... 22
6
Known Bugs............................................................................................................ 25
7
Literature ................................................................................................................ 26
page 2