Laboratory of Formal Methods (2016/2017)
The material is made available after each lesson.
Disclaimer: last year's slides will be subject to some changes, thus refer to the updated content.
All packages can be opened with the command
~$ tar -xvf package_name.tar.gz
Part I - spin
The
spin model checker can be downloaded from this
link.
Its documentation is provided
here.
-
Spin: Introduction -
March 03, 2017
Spin: Introduction (slides)
Lab examples (download)
-
Spin: Overview of PROMELA -
March 10, 2017
Spin: Overview of PROMELA (slides)
Code examples (download)
Exercises solutions (download)
-
Spin: Exercises on Message Channels -
March 17, 2017
Spin: Exercises on Message Channels (slides)
Code examples (download)
Exercises solutions (download)
-
Spin: LTL Model Checking -
March 24, 2017
SPIN: LTL Model Checking (slides)
Code examples (download)
Exercises solutions (download)
Optional Exercise solution (download)
-
Spin: Exercises -
March 31, 2017
Spin: Exercises (slides)
Exercises solutions (download)
Part II - nuXmv
The
nuXmv model checker can be downloaded from this
link.
Its documentation is provided
here.
-
nuXmv: Introduction -
April 07, 2017
nuXmv: Introduction (slides)
Code examples (download)
Exercises solutions (download)
-
nuXmv: Model Checking -
April 21, 2017
nuXmv: Model Checking (slides)
Code examples (download)
Exercises solutions (download)
-
nuXmv: Planning -
May 05, 2017
nuXmv: Planning (slides)
Code examples (download)
Exercises solutions (download)
-
nuXmv: Bounded Model Checking -
May 12, 2017
nuXmv: Bounded Model Checking (slides)
Code examples (download)
Exercises solutions (download)
Optional Exercise solution (download)
-
nuXmv: Exercises -
May 19, 2017
Code examples (download)
nuXmv: Exercises (slides)
Exercises solutions (download)
Part III - Wrapping Up
-
Exam: Group Simulation -
May 26, 2017
Exam: Assignment (download)
Exam: Solution (download)
Available documentation during the exam (download) - found in '/usr/local/docs'