CS 422: System Specification & Implementation (Spring 2011)

The course is about 'Correct by Construction' approach to System Development. It deals with formally specifying system properties and developing systems methodically to meet those specifications.

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.

Text Books

Unfortunately the text-book is not available in Indian edition. The instructor will make the required material available.

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