Final Review
The final is on Monday, December 17th, from 11:00 – 14:00 in TMCB 134. One page of notes allowed (any size and any font). It consists short answer problems. Here is a comprehensive list of topics:
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.
Back to top