Schedule: Lecture Slot 4 in SIC 301 Kresit
Instructor: Om Damani Office hours: TBD
TAs: Leela Surya Narayana TA office hours TBD
Moodle: Slides, Assignments, Solution, Newsgroup etc.
Pre-requisites Background in Structured Programming and Predicate Calculus: (CS 152 and CS 207) or CS 719 or Equivalent Courses. If you do not have the background then it is your responsibility to work extra hard and catch up.
Audit Requirements:
You have to do all the assignments. There will be at least one assignment per week. 80% attendance will also be required. You will not have to do project or write endsem. You will have to attempt midsem and quizzes.
1. Modeling in EventB: System and Software Engineering, J. R. Abrial, Cambridge, 2010.
| Sr. No: Date | Topic | Resource |
|---|---|---|
| 1/2: 03,04/01 | Introduction: Specification, Formal Methods, 'Correct by Construction' approach | slides |
| 3: 06/01 | Ch2, Bridge Traffic Controller: Problem description, the simplest abstraction - no bridge/sensor/traffic-light; Introduction to Sequent Calculus | Ch2, slides |
| 4: 10/01 | First refinement: Introducing the one-way bridge | slides |
| 5: 11/01 | Second refinement: Introducing the traffic lights | slides |
| 6-8: 13,17/01 | Bridge Traffic Controller: remaining refinements | slides |
| 9-13: 18-31/01 | Ch 3, Mechanical Press Controller | slides |
| 14-16: 1-7/02 | A Simple Location Access Control | slides |
| 17-21: 8-17/02 | Ch16, Location Access Control | slides |
| 22-23: 28/02,01/03 | Ch15, Sequential Program Development | slides |
| 24-28: 03-14/03 | Schorr Waite Algorithm | Paper, slides |
| 29-32: 15-22/03 | Ch4, Ch6, File Transfer Protocol | slides |
| 33-38: 24/03-07/04 | Ch7, Concurrent Reader Writer | slides |
| 39-41: 11-14/04 | Ch12, Routing Algorithm for a Mobile Agent | slides |