Formal Methods in Software Engineering

E0 272 Formal Methods in Software Engineering

January-May 2012, 5:00pm-6:30pm Tue Thu, Room 252 CSA
Credits 3:1

Instructors: K. V. Raghavan, Deepak D'Souza, Prahlad Sampath. Guest lectures by Nigamanth Sridhar.

TAs: Anirudh Kushwah (anirudhkushwah@csa), Arjun Suresh (arjunsuresh@csa)

Lecture slides

Jan. 5: Introduction
Jan. 10, 12, 17, 19: Alloy
Jan. 25, Feb. 1, 2, 9: Rodin
Feb. 14, 16: Resolve
Feb. 21, 23: Sal
Mar. 6, 8: Spin
Mar. 13, 15, 20: Refactoring
Mar. 22, 27: FindBugs
Mar. 29, Apr. 3: Pex
Apr. 5, 10: Hoare logic
Apr. 12, 13: Spec#

Assignments

Assignment 1, on Alloy. Posted Jan. 26. Due Feb. 2nd. Will not be accepted after Feb. 6th.
Assignment 2, on Rodin. Posted Feb. 8. Due Feb. 15. Will not be accepted after Feb. 18.
Assignment 3, on Resolve. Posted Feb. 23. Due on Mar. 1st. Will not be accepted after Mar. 6.
Assignment 4, on Sal. Posted Feb. 24th. Due Mar. 6th (no late days allowed). Skeleton Sal model for the assignment: trafficPedLight.sal.
Assignment 5, on Refactoring. Posted Mar. 20. Due Mar. 30. Will not be accepted after Apr. 1.
Assignment 6, on LTL model checking, and Spin. Posted Mar. 21. Due Apr. 2. Will not be accepted after Apr. 4.
Assignment 7, on FindBugs and Pex. Posted Apr. 5. Due Apr. 19. No late days permitted.

Motivation

Software is used for an increasing range of business and personal activities, and to control vital processes and tasks. This makes it important that software be developed efficiently, and the software be correct and reliable. However, software development and maintenance has largely remained mostly a human activity, with sub-optimal usage of tools and formal processes. This course will equip students with knowledge of the latest advances in the role of tools and formal methods in software engineering. The course will focus on all stages of software engineering, from requirements, design, coding, and verification. The methodology will be to study a series of advanced tools that address challenges faced in these steps. This will include both an introduction to the theoretical underpinnings of these tools, as well as hands-on exploration in class as well as well as in assignments.

Syllabus

Conceptual modeling of requirements using logic -- Alloy. Refinement of models -- Rodin and Resolve. Detailed design of state-based systems -- SAL, and Spin. Code development using refactoring -- Eclipse Refactorings. Identifying errors in code during development using dataflow analysis -- FindBugs. Proving properties of code using logical reasoning -- Spec#. White-box testing of applications -- Pex.

Prerequisites: Exposure to programming, and the basics of mathematical logic and discrete structures.

Tentative grading breakup

Assignments:	60%
Midsem exam:	15%
Final exam:	25%