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

Link to this comparison view

cs-486:homework-4-2016 [2017/01/11 18:47] (current)
egm created
Line 1: Line 1:
 +* Master Fairness in on-the-fly LTL model checking
 +== Reading ==
 +Chapter 9 of the course text.
 +== Paper Pencil Problems ==
 +# '''​(5 points)'''​ Create fairness constraints for the system in [[Homework 3]] that limits the verification to paths that release '''​fork1'''​ and '''​fork2'''​ in a finite amount of time.
 +# '''​(15 points)'''​ Perform on-the-fly model checking to see if our system satisfies the property on fair paths(i.e., check the intersection of the model '''​with fairness'''​ and the never claim). Please show the entire search graph as we did in class.
 +# '''​(5 points)'''​ Write the dining philosophers model in Promela and verify the same properties in SPIN. Submit the Promela for the model and the SPIN output. Some simple instructions for installing and using Spin are in the [[Tools]] page. Use the atomic keyword to make it so each location is a single atomic step so the state space is smaller than 15 states.
 +# '''​(5 points)'''​ Implement mutex 1 from [[Homework 1]] in PROMELA and verify mutual exclusion and deadlock freedom with SPIN. Attach the output from the verification to the homework. The PROMELA should have two processes both using Mutex 1 to arbitrate access to the critical section.
 +# '''​(5 points)'''​ Repeat the previous problem for mutex 2. 
cs-486/homework-4-2016.txt ยท Last modified: 2017/01/11 18:47 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