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

Next revision | Previous revision | ||

cs-486:exams [2014/09/02 10:44] egm created |
cs-486:exams [2018/12/13 10:50] (current) egm [Final Review] |
||
---|---|---|---|

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. |