Laboratory of Formal Methods (2014/2015)
The material is made available after each lesson.
Disclaimer: some slides of the previous years contain outdated information.
Please, refer only to the (revised) material that I provide you on this web page.
Part I - spin
The
spin model checker can be downloaded from this
link.
Its documentation is provided
here.
- Introduction to SPIN - Feb 24, 2015
Introduction to SPIN (slides)
Lab examples (download)
- An overview of PROMELA - Mar 03, 2015
An overview of PROMELA (slides)
Code examples (download)
Exercises solutions (download)
- Exercises - Mar 10, 2015
Exercises (slides)
Code examples (download)
Exercises solutions (download)
- SPIN: verifying LTL properties - Mar 17, 2015
SPIN: verifying LTL properties (slides)
Code examples (download)
Exercises solutions (download)
Optional exercise solution (download)
Part II - nuXmv
The
nuXmv model checker can be downloaded from this
link.
Its documentation is provided
here.
- nuXmv: introduction and examples - Mar 24, 2015
nuXmv: introduction and examples (slides)
Lab examples (download)
Exercises solutions (download)
- nuXmv: property specification - Mar 31, 2015
nuXmv: property specification (slides)
Lab examples (download)
- nuXmv: Planning as Model Checking - Apr 21, 2015
nuXmv: Planning as Model Checking (slides)
Lab examples (download)
Exercises solutions (download)
- nuXmv: Bounded Model Checking - Apr 28, 2015
nuXmv: Bounded Model Checking (slides)
Lab examples (download)
Exercises solutions (download)
Optional exercise solution (download)
Part III - exercises
Last part of course devoted to some exercises.
- nuXmv: Exercises - May 05, 2015
nuXmv: Exercises (slides)
Lab examples (download)
Exercises solutions (download)
(note: philosophers solution moved to next week)
- Exercises (continued) - May 12, 2015
Exercises (slides)
Exercises solutions (download)
- Exam Examples - May 19, 2015
Exam Examples (slides)
Examples (download)