meta data for this page
  •  

Proposal from Prof. Damani - 16th Nov 2010.

Preface: Last year when I proposed 'Program Derivation' course, Ajit commented to me, 'forget deriving algorithms, can you teach students how to translate pseudo-code into correct programs'. This course is partly in response to that. Turns out that there are many companies in Europe that have been selling Certified Software for well over a decade - Escher technologies, Esterel Technologies, and Praxis Incorporation. Do you remember being amazed at Knuth's “I believe that last bug in Tex was found and removed on November 27 , 1985.” Well then look at software for Paris Metro, Line 14: 110,000 lines of B models, generating 86,000 lines of Ada. No bugs have been detected in it since its release in October 1998. No unit tests were performed for the Line 14 project; they were replaced by some global tests that were all successful. Other stories can be found in “Formal Methods: Practice and Experience”, ACM Computing Surveys, Volume 41 Issue 4, October 2009 ( http://portal.acm.org/citation.cfm?id=1592434.1592436 ).

Course Name: [Topics in] System Specification and Implementation
Credit Structure: 3 0 0 6
Prerequisite: Some course in logic or formal methods.

Course Content: The emphasis of the course will be on understanding System Specification Methods and Program Correctness Concepts and exploring the same using various tools. Many examples of non-trivial algorithms, large software systems, network protocols, and distributed systems will be discussed. The course will involve large case studies and the students will be required to do numerous proofs, either manually or using some tools. Depending on the chosen methodology, different subsets of the following topics will be covered in different offerings:

High Level Concepts:
Modeling: Abstract models of physical reality
Specification: What is it that we want
Validation: Are we building/wanting the right thing
Verification: Are we implementing what has been specified

Technical Details:
Specification Languages: Formally specifying what we want our system to do. One of the specification languages from ASM (Abstract State Machine), VDM (Vienna Development Model), B and Event-B, Alloy, Spec# etc. will be covered.
Mathematical Objects: Sets, Finite Sequences, Finite Trees, Well founded Relations.
State Machines: Specifying the State, specifying the Operations, Termination.
Proof Obligations: Weakest Precondition Calculus, Invariants, Variants. Refinement: Starting with an abstract system and converting it into an implementation through a series of refinements. Proof obligations during refinements.

Tools:
Static Analyzers, Proof Obligation Generators, Proving tools (automatic and interactive), Animators, Model Checkers. The course will focus on using these tools and will not discuss how to build such tools.

Texts/References:
1. Modeling in Event-B: System and Software Engineering, J. R. Abrial, Cambridge, 2010.
2. Abstract State Machines: A Method for High Level System Design and Analysis, Borger and Stark, Springer, 2003.
3. Modeling Systems: Practical Tools and Techniques in Software Development, Second edition, Fitzgerald and Larsen, Cambridge, 2009.
4. The B-book: Assigning Programs to Meanings, J. R. Abrial, Cambridge, 1996.
5. Software Abstractions: Logic, Language, and Analysis, Daniel Jackson, MIT Press, 2006.