##### Differences

This shows you the differences between two versions of the page.

 cs-486:exams [2014/09/02 10:44]egm created cs-486:exams [2018/12/13 10:50] (current)egm [Final Review] 2018/12/13 10:50 egm [Final Review] 2018/12/13 10:50 egm [Final Review] 2017/12/14 14:04 egm [Final Review] 2017/04/20 15:57 egm [Final Review] 2017/04/19 13:11 egm [Final Review] 2017/04/19 13:05 egm 2017/04/19 12:38 egm [Final Review] 2017/02/28 17:39 egm [Midterm Review] 2014/09/02 10:44 egm created Next revision Previous revision 2018/12/13 10:50 egm [Final Review] 2018/12/13 10:50 egm [Final Review] 2017/12/14 14:04 egm [Final Review] 2017/04/20 15:57 egm [Final Review] 2017/04/19 13:11 egm [Final Review] 2017/04/19 13:05 egm 2017/04/19 12:38 egm [Final Review] 2017/02/28 17:39 egm [Midterm Review] 2014/09/02 10:44 egm created Line 1: Line 1: == Final Review == == 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: + 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: - * Create ​minimum labeled traces such that they satisfy ​a given temporal logic formula + * Create ​Kripke structures ​that satisfy temporal logic formulas ([[Homework 7]]) - * Create ​BDDs from code showing ​the unique and compute tables as a final answer (IDs must follow ​the order of creation from ITE) + * Write temporal logic formulas for specification expressed in english--be sure you know both CTL and LTL sub-logics ([[Homework 7]]) - * Create a Boolean expression for a transition relation from a simple program ​like the dining philosophers in the homework + * Prove (or disprove) if two temporal logic formulas are equivalent ([[Homework 8]]). - * Write a Boolean function describing the initial state of a problem ​and perform ​reachability ​analysis using that function and a transition relation + * Given a Kripke structure and a set of CTL formulas, determine which states are labeled with which formulas ([[Homework 10]]). - * Perform CTL model checking using Boolean functions and fix-point computations + * Play computer and show how BDDs are created and managed with the '''​ITE'''​ method given a program using the Cudd interface. Be sure to show the unique ​table ''​and'' ​the recursive trees tracking the '''​ITE'''​ calls ([[Homework 11]] and [[Homework 12]]). + * Create a Boolean expression for a transition relation from a simple ​PROMELA ​program ​([[Homework 13]]) + * Write a Boolean function describing the initial state of a system ​and perform ​forward reachable ​analysis using that function and a given transition relation ​([[Homework 13]] but doing it abstractly similar to class rather than with BDDs).  ​ + * Perform CTL model checking using Boolean functions and fix-point computations ​on a given Kripke structure. Show each iteration of the fix-point calculations (abstractly similar to class rather than with BDDs). ​ I expect the test to take 2 hours of student time. I expect the test to take 2 hours of student time. - == Midterm Review == == 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. 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. - * Describe ​the LTL syntax, CTL syntax, and the different in semantics between LTL and CTL + * Translate if-statements and while-statements into PROMELA - * Write English descriptions as properties ​in CTL, LTL, or CTL*. Negate temporal logic formulas. + * Create a PROMELA verification model to solve a problem that uses shared memory for coordinating processes - * Create minimum labeled ​traces ​such that they satisfy a given temporal logic formula. + * 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. ​ - * Convert a Kripke structure to a Buechi automaton. + * Write safety ​properties ​and create traces that violate the property. - * Express the language accepted by a Buechi automaton as a regular expression ​augmented with the omega operator. + * Write liveness properties and create ​traces that violate the property. - * Compute the intersection of two Buechi ​automaton. + * Convert a state transition system into a Buchi Automaton - * Perform double-depth-first-search ​on a Buechi ​automaton. + * Given a Buchi Automaton, write a regular expression ​that includes ​the $\omega$-operator ​that is the language detected by the Automaton. - * Implement fairness in on-the-fly model checking. + * Compute the intersection of two Buchi automaton. - * Perform explicit state model checking given a Kripke and CTL property. + * 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 hour of student time. The total time limit on the test is 2 hours. + I expect the test to take at least 1.5 hour of student time. The total time limit on the test is 2 hours.