Weryfikacja wspomagana komputerowo
2016-2017
Lab 7 – NuXmv and CTL

Vincent Penelle

Topics of this Lab



Exercise 1: (CTL)

In addition to LTL, NuXmv is also able to check CTL formula (actually, it is its main use). CTL is a logic which deals with paths rather than a single execution. To write a CTL formula to your model, you simply write SPEC formula (e.g., SPEC AG (i=0 -> EX i!=0)), and you can check it with the command check_ctlspec. You can find the syntax of CTL formulæ on the manual page.

  1. Add to this file the following properties in CTL. Then check them. (this code should not be dissimilar to last time).


Exercise 2: (A microwave)

This code models the behaviour of a microwave.

  1. Draw (on a paper) the automaton described by this model (and give relevant names to transition – after all this is a microwave, that should be doable).
  2. Express in CTL and check the following properties:


Exercise 3: (Modelling an elevator)

The goal of this exercise is to model an elevator in smv, and to check its behaviour in CTL. Your elevator can navigate between floors 1 to N (with a fixed value of N which I let you choose – but don’t take it too big). It has a set of buttons, 1 for each floor, which can be on or off. When a button is on, that means the elevator has been called to that floor (and should go there). At each step, the elevator can go up or down by one step, and can be called to some floors. When it is at a given floor, the corresponding button is switched off.

  1. Make a model of such an elevator. The following properties will have to be expressed in CTL, included to your model, and true. You may need some more information in your model than what I’ve discribed to have a correct model.
  2. In addition, check on it the following properties (in CTL). Some may be false.


Exercise 4: (Mutual exclusion (le retour de la vengeance))

Even if processes are not recommended in smv (see next exercise), it is still possible to model a mutual exclusion algorithm in smv. Here is a code of it.

  1. Draw the described system.
  2. Write and check in CTL the following properties:
  3. Would it be easy to extend that modelisation to more than two processes?


Exercise 5: (Processes (deprecated))

If we have time, we will quickly discuss of a feature which should disappear in a next version (announced since some years now though): processes. In nuXmv, it is not possible to have cycling dependency as it was the case in Spin. With processes, it used to be the case. Here is an example of that behaviour, which should not be unfamiliar. Understand it and check it, but do not put to much time in this: this feature is not supposed to be used.


This document was translated from LATEX by HEVEA.