Week 1: September 2, 2014.
Week 2: September 9, 2014
Week 3: September 16, 2014
Week 4: September 23, 2014
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 1. To keep things simple, assume that each sensor will either be "on" or "off" -- I would not include "polling" as part of the sensor behavior (as shown in one of the examples in the class notes).
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.
Hint 2. One unknown in this problem is the length of the train and, of course, your control strategy should work for all cases. An easy way to simulate the effect of a really short train is with the sequence:
sensor1.on --> sensor1.off --> sensor2.on --> sensor2.off --> sensor3.on --> sensor3.off.
Conversely, a long train will trigger the sensor sequence:
sensor1.on --> sensor2.on --> sensor3.on --> sensor1.off --> sensor2.off --> sensor3.off.
List all other assumptions that you make.
What to hand in
Hand in a 2-to-3 page report describing the processes and properties in your solution procedure and how they interact. Include screencaptures of the appropriate labeled transition systems.
Explain what worked well and in what ways you found LTSA to be limited.
Week 5: September 30, 2014
Week 6: October 7, 2014
Week 7: October 14, 2014
You can work in teams of two for this homework
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.
What to hand in
Hand in a 2-to-3 page report describing the processes and properties in your solution procedure and how they interact. Include screencaptures of the appropriate process models.
Explain what worked well and in what ways you found UPPAAL to be superior to LTSA.
Week 8: October 21, 2014
Week 9: October 28, 2014
Project 08: Verification and Validation of Automated Traffic Control System Project
Project 09: Verification and Validation in the Smart-Grid Environment
Project 10: Validation and Verification of Packaging Strategies for Humanitarian Aid/Disaster Relief (HA/DR) Response
Project 11: Water Distribution System Security
Project 12: Validation and Verification for Unmanned Underwater Autonomous Vehicles
Project 13: ....
Project 14: ....
Project 15: ....
Week 10: November 4, 2014
Project 1: Verification and Validation of the Pointing Control System for PIPER
Project 2: Markov Chains for Healthcare Process in Diabetic Management Health Complication
Project 3: Validation of Social Media Business Methodology
Project 4: Using JUnit tests to verify and validate a Course Management System
Project 5: Decision Support Model for Physical Protection System Validation and Verification
Project 6: Requirements Management and Verification for Manufacturing Processes
Project 7: Project Proposal: Hardware Design Verification using Verilog FPGA
Week 11: November 11, 2014
Week 12: November 18, 2014
Week 13: November 25, 2014
Week 14: December 2, 2014
Project 08: Verification and Validation of Automated Traffic Control System Project
Project 09: Verification and Validation in the Smart-Grid Environment
Project 10: Validation and Verification of Packaging Strategies for Humanitarian Aid/Disaster Relief (HA/DR) Response
Project 11: Water Distribution System Security
Project 12: Validation and Verification for Unmanned Underwater Autonomous Vehicles
Project 13: A Framework For Natural Language Processing in Requirements Engineering
Project 14: Verification and Validation of Parcel Router System
Project 15: JUnit Testing for a Predictive Analytics System
Week 15: December 9, 2014
Project 1: Verification and Validation of the Pointing Control System for PIPER
Project 2: Markov Chains for Healthcare Process in Diabetic Management Health Complication
Project 3: Validation of Social Media Business Methodology
Project 4: Using JUnit tests to verify and validate a Course Management System
Project 5: Decision Support Model for Physical Protection System Validation and Verification
Project 6: Requirements Management and Verification for Manufacturing Processes
Project 7: Project Proposal: Hardware Design Verification using Verilog FPGA
Last Modified: November 25, 2014,
Copyright © 2014, Institute for Systems Research, University of Maryland.