COSC 6384: Real-Time Systems Homework 3, Part 2, Spring 2007 (1) Specify the following protocol as a finite-state graph. There is one sender process and one receiver process. The sender repeats the following infinitely often: generate message, send message, wait for acknowledgement. The receiver repeats the following infinitely often: wait for message, send acknowledgement, print message. Then specify in CTL: sender waits for an acknowledgement for a sent message before generating a new message. Define labels as needed. (10 points) (2) Consider a smart airbag deployment system in an automobile. A sensor is attached to the driver's seat that detects the distance between the driver and the steering wheel. This distance depends on the shape and size of the driver, and the position of the steering wheel. Based on this distance, the airbag computer determines how fast the airbag should be fully inflated. The airbay will deploy when a collision impact with a speed exceeding 30mph occurs; otherwise, it will not deploy. If the distance is far (> 1.5 ft), the airbag will be fully deployed within 50ms. If the distance is average (between 1.0 ft and 1.5 ft), the airbag will be fully deployed within 40ms. If the distance is near (< 1.0 ft), the airbag will be fully deployed within 30ms. Specify this system as a finite state graph or Statechart. (10 points). (2) Consider the following set of inequalities. 1. t_1: B + 10 <= C 2. t_2: A - 10 <= B 3. t_3: C <= A 4. t_4 or t_7: C - 10 <= D or B + 10 <= D 5. t_6 or t_7: D + 10 <= B + 10 <= D 6. t_5 or t_6: D + 10 <= C or D + 10 <= B Construct the constraint graph for these inequalities. List the positive cycles. Using these positive cycles, construct a tree to find out if this set of inequalities is unsatisfiable. (10 points)