Notes From Class
Notes From Class
Week 1: September 4, 2012.
Click here for step-by-step instructions on downloading and installing the software on a Mac.
For plugin installation and unlock instructions refer to:
http://www.nomagic.com/support/installation-and-use.html
For plugin and product compatibility please refer to:
http://www.nomagic.com/support/compatibility.html
Week 2: September 11, 2012
Week 3: September 18, 2012
Week 4: September 25, 2012
Week 5: October 2, 2012
You can work in teams of two for this homework
The railroad crossing problem shown in Figure 1 is a benchmark problem for the validation of safety-critical applications.
Figure 1. Simplified model for the railroad crossing problem.
For the system to operate safely, things need to happen in the correct order, and they need to be timely. In this homework we will abstract away the details of time and space, and just look at the interactions among the various subsystems with LTSA.
Develop a detailed model of the railroad crossing problem in LTSA.
Your model should include processes for the sensors (e.g., a:sensor, b:sensor, c:sensor), the gate, the gate controller, and the train. Also indicate the property automata that you would use for safety and progress checks.
My suggestion is to keep the functionality of the sensors as simple as possible (i.e., simply measure whether or not the track is occupied by a train at a particular point) and then put all of the system smarts in the gate controller.
The first and third sensors should detect the arrival and departure of a train. A safety violation will occur if the second sensor is activated before the gate has been completely lowered.
You should aim for a modeling formulation where behavior is a composition of lower level behavior, e.g., something like:
||RailwayCrossing = ( Train || Gate || Controller || Sensor1 || Sensor2 || Sensor3 )
Hint. To keep things simple, assume that each sensor will either be "on" or "off" -- I would not include "poling" as part of the sensor behavior.
The purpose of the Train process is to define valid sequences of sensor switching. For example, the front of the train will trigger the sequence of actions:
sensor1.on --> sensor2.on --> sensor3.on,
And the back of the train will trigger the sequence,
sensor1.off --> sensor2.off --> sensor3.off.
For some ideas on how to implement the gate controller, see the oneway bridge example in the LTSA distribution. The process is called BRIDGE, but it's really a traffic controller.
List all other assumptions that you make.
Week 6: October 9, 2012
Week 7: October 16, 2012
Develop a detailed model of the railroad crossing problem in UPPAAL.
My suggestion is that you study and adapt the train-gate example discussed in class. Assign reasonable times for each activity and periods that a train will spend in each zone. Then try to identify boundaries that separate safe behavior from unsafe behavior.
List all other assumptions that you make.
Week 8: October 23, 2012
Week 9: October 30, 2012
Week 10: November 6, 2012
Midterm Project Presentations ...
Projects 1 through 7.
Week 11: November 13, 2012
Midterm Project Presentations
Projects 8 through 12.
Week 12: November 20, 2012
Week 13: November 27, 2012
Week 14: December 4, 2012
Week 15: December 11, 2012
Last Modified: November 13, 2012,
Copyright © 2012, Institute for Systems Research, University of Maryland.