SWE 619 Assignment 9
Spring 2013


Goal: Temporal Logic / Specification Patterns.

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.

  1. It is possible to get to a state where started holds, but ready does not hold.
  2. For any state, if a request (of some resource) occurs, then it will eventually be acknowledged.
  3. A certain process is enabled infinitely often on every computation path.
  4. Whatever happens, a certain process will eventually be permanently deadlocked.
  5. From any state, it is possible to get to a restart state.
  6. An upwards travelling elevator at the second floor does not change its direction when it has passengers wishing to go to the fifth floor.
    Use predicates such as direction == up, floor == 2, and Button5Pressed.
  7. The elevator can remain idle on the third floor with its doors closed.