Modelling and Analysis of an Interventional X-Ray System
Goal
A requirements document written by Jozef Hooman lists a number of requirements for an
interventional X-ray system of Philips Healthcare.
These requirements are also illustrated via a number of
movies and slides.
The goal of this assignment is:
-
To formalize the requirements in temporal logic.
-
To construct a NUSMV2 (or Uppaal) model of the (relevant part of the) interventional X-ray system.
-
To verify that your model satisfies the requirements (or establish that the requirements are problematic/inconsistent).
Do not hesitate to contact Jozef Hooman and/or the instructor with questions!
Note: Given that the total time required for making the full assignment is hard to predict
and no extension of the deadline is possible, you are strongly advised to focus first on a
simplified version of the system without switch (pedals only) and without errors, and to deal
with formalization of the requirements, model building and analysis for this subcase.
Once this has been completed and there is time left, you may work on adding the switch or the errors
(or both).
Reflection
Did you find your efforts to formally model and reason about this system useful?
Did it help you to gain additional insight in the temporal logic and model checking?
If so, what did you learn?
What was the most difficult part of this assignment?
What was your experience with NuSMV2 (or Uppaal)?
Products
Your report + NuSMV2 models should be sent in by July 3, 2013.