CIS 720 – Fall 2012
Programming Assignment 1
Due Date: September 6, 2012
Build a model (in Promela) of a real-time preemptive scheduler. Your solution should prove that all deadlines are met. Illustrate this by verifying that the preemptive schedule in Lecture 1 is met, where A is the high priority and B is the low priority task.