CSSE 373 Formal Methods in Specification and Design

HW11

Purpose: practice describing a reactive system using higher order statecharts

1. Keep track of how much time you spend on this assignment. You will submit your answers as a pdf file at the end of the homework.

2. Consider the following intersection (and the figure below):

   • First Avenue is an ordinary road running East-West. It has one lane for each direction.
   • One set of railroad tracks run parallel with First Avenue, about 50 feet North of First Avenue.
   • Main Street runs North-South, intersecting First Avenue and the railroad tracks. It also has one lane for each direction.
   • There are sensors that detect the presence of cars and trains at appropriate places.
   • There is a traffic light at the intersection of First Avenue and Main Street.
   • There are crossing gates on Main Street to prevent cars from crossing the railroad tracks when a train is near. Note that there is room for a few vehicles between the traffic light and the crossing gates.
   
3. Write a statechart specification of the traffic light and the crossing gates. Be sure to include those cases where the crossing gate may be moving. For full credit you must use the higher-order features of statecharts such as orthogonal substates and depth.
4. Give an argument that the traffic light signals will prevent collisions as long as they are obeyed. Be sure to include all cases of traffic. Describe each case in terms of states of the statechart.
5. Turn in your work by committing a single pdf file to the appropriate HW folder in your individual subversion repository for this course. Be sure your pdf file contains both your statechart and your answer to the question above.
6. Please complete the short, anonymous survey on ANGEL regarding this assignment. (I will study these surveys in detail after the conclusion of this offering of the course. If you have suggestions that you would like me to consider during this offering of the course, please tell me in person or use the separate Anonymous Suggestion Box on ANGEL.)