Differences

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

Link to this comparison view

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 syntaxCTL syntaxand 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 pollinsert sortedpattern match (including ​the ''​eval()''​ function), ​and copy values from the channel. ​ 
-* Convert a Kripke structure to Buechi automaton. +* Write safety ​properties ​and create traces that violate the property.  
-Express the language accepted by 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 Buchi Automaton 
-* Perform double-depth-first-search ​on Buechi ​automaton. +Given 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 Kripke and CTL property. +* Perform double-depth-first search ​to detect cycles in given Buchi automaton. ​Indicate pre-order traversal numbers ​on both searches and show the evolution of the runtime stack.  
- +Given 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.
cs-486/exams.1409676243.txt.gz · Last modified: 2014/09/02 10:44 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