**This is an old revision of the document!**


Final Review

The final is in the testing center and is closed book and closed notes. It consists of one multiple-guess problem and 5 essay problems. Here is a comprehensive list of topics:

  • Create minimum labeled traces such that they satisfy a given temporal logic formula
  • Create BDDs from code showing the unique and compute tables as a final answer (IDs must follow the order of creation from ITE)
  • Create a Boolean expression for a transition relation from a simple program like the dining philosophers in the homework
  • Write a Boolean function describing the initial state of a problem and perform reachability analysis using that function and a transition relation
  • Perform CTL model checking using Boolean functions and fix-point computations

I expect the test to take 2 hours of student time.

Midterm Review

One page of notes is allowed for the exam. You are responsible for knowing the testing center hours: double check the schedule for Saturday! Below is a comprehensive list of topics on the exam. Please note that some of the topics were not covered directly by the homework, so you will want to perhaps work a few problems on your own to prepare.

  • Translate if-statements and while-statements into PROMELA
  • Create a PROMELA verification model to solve a problem that uses shared memory for coordinating processes
  • Create a PROMELA verification model to solve a problem that uses message passing for coordinating processes. Be familiar with all the different forms of interacting with a channel including the ability to poll, insert sorted, pattern match (including the eval() function), and copy values from the channel.
  • Write safety properties and create traces that violate the property.
  • Write liveness properties and create traces that violate the property.
  • Convert a state transition system into a Buchi Automaton
  • Given a Buchi Automaton, write a regular expression that includes the $\omega$-operator that is the language detected by the Automaton.
  • Compute the intersection of two Buchi automaton.
  • Perform double-depth-first search to detect cycles in a given Buchi automaton. Indicate pre-order traversal numbers on both searches and show the evolution of the runtime stack.
  • Given a correctness property, write a never claim to detect when the property is violated.

I expect the test to take at least 1.5 hour of student time. The total time limit on the test is 2 hours.

cs-486/exams.1488328767.txt.gz · Last modified: 2017/02/28 17:39 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0