SWE 619 Assignment 9
Fall 2023


Goal: Temporal Logic / Specification Patterns.

Note: You might find the Huth and Ryan text useful for some of these exercises:

M.R.A. Huth and M.D. Ryan. Logic in Computer Science. Second Edition. Cambridge University Press, 2004, ISBN 978-0-521-54310-1.
Although this text is no longer available through the university libarary services, enterprising students may be able to locate this document. Relevant material begins on page 183.

The non-bonus part of this assignment is a paper/pencil exercise only. Use the KSU slides covered in the lecture as a resource to help you formulate the following in CTL. You should use the variables listed in typewriter font as your primitive propositions. Start by drawing an appropriate computational tree, and only then capturing that tree with CTL. The computational tree will count as part of the grading.

  1. It is possible to get to a state where started holds, but ready does not hold.
  2. If a request (of some resource) occurs, then it will eventually be acknowledged.
  3. A certain process will eventually be permanently deadlocked.
  4. No matter what state the computation is in, the reset process will eventually be enabled.
  5. It is always possible to get to a restart state.
  6. The elevator can remain on the third floor with its doors closed indefinitely.
    Use predicates such as doors == closed, floor == 3,
  7. After switchClosed becomes true, valveOpen is never true.
  8. Variable toggle alternates between true and false on successive states.

For those interested in bonus points, consider the traffic light specification. Expand the SMV to model a more complex intersection. For example, you could consider an intersection with a left-turn arrow. Write SPEC clauses to capture the following property:

Finally, verify these properties with SMV. You can download SMV in various forms from Carnegie Mellon (finding a place to run this binary may be an adventure...) or NuSMV (this runs ok for me).

As an additional example, you might look at a mutual exclusion example or the example from the class slides

Note: NuSMV has deprecated processes; I'd be happy to have someone figure out the appropriate replacement.

Bonus credit (up to 3 points) only available if you demonstrate that you had SMV running.