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.