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.

   NO LATE DAYS ALLOWED ON THIS ASSIGNMENT.

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.

   You may draw your statechart neatly by hand and scan it, or use a drawing programming such as Visio or OmniGraffle to create the diagram.

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. Record the amount of time you spent on this assignment in your answers file.
6. 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 questions above.