Notes From Class

Week 1: September 3, 2013.

Lecture slides: Quick Review of ENSE 621 and ENSE 622 .
The lecture notes can be purchased from Steve Sutton at ISR for $50.

Week 2: September 10, 2012

Lecture slides: System Process and Workflow Modeling .

Week 3: September 17, 2012

Note: I will try to get a zip file of the support material to students at the remote sites via Dropbox ... today.
Lecture slides: Established Approaches to Validation and Verification

Week 4: September 24, 2013

Lecture slides: Emerging Approaches to Validation and Verification

Week 5: October 1, 2013

Lecture slides: Model-Based Design with LTSA
Homework 1 : Now due October 16.
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 6: October 8, 2013

Lecture slides: Formal Approaches to Validation with Logic

Week 7: October 15, 2013

Lecture slides: System Behavior Modeling and Validation with UPPAAL

Week 8: October 22, 2013

Lecture slides: Formal Validation with Spatial Logic and Spatio-Temporal Logic
Homework 2: Due November 5

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 9: October 29, 2013

Midterm Project Presentations
- Projects: 11 through 19.
Midterm Project Presentation Requirements
- Duration: Aim for 15 minutes; No more than 20 minutes.
- Slides: Only six slides.
- Content: Project Title and Who am I? What am I doing? Why is it important? How will the project relate to validation/verification? What's new?

Week 10: November 5, 2013

Midterm Project Presentations ...
- Projects: 1 through 10.

Week 11: November 12, 2013

Midterm Exam: ....

Week 12: November 19, 2013

Presentation by Dr. Huan Xu on her Ph.D. work at Caltech.
Design, Specification and Synthesis of Aircaft Electric Power Systems.

Week 13: November 26, 2013

Project work (I'll make a point of being in my office from about
mid-afternoon so stop by if you need to talk about your project.
Have a good Thanksgiving ....
Presentation Guidelines

Aim for 20 minutes and 20 slides, followed by a few minutes for questions.
All team members should participate in the presentation.
Everyone should come to class to hear the presentations.

Week 14: December 3, 2013

End-of-Semester Presentations: Projects 1 through 9.

Week 15: December 10 and 13, 2013

End-of-Semester Presentations: Projects 10 through 17.
Semester Projects Due on the last day of classes: December 13.
This is a hard deadline, so no extensions.