News

• Project teams and assignments are being posted.
• Information on the proposed term project.
• Another video on using interactive theorem proving in Rodin plus a link to the documentation of the theorem provers in Atelier B (accesed by Rodin through plugins) [15/11/2011].
• Some videos on the use of Rodin posted [2/11/2011].
• Event-B material posted [22/09/2011].

Lecturers

Manuel Carro, Julio Mariño.

Overview

Software is getting more and more complex and is becoming responsible for critical tasks. Therefore, any technology aimed at ensuring the reliability and quality of software will be increasingly relevant.

There are many ways to approach these goals. The declarative approach relies on languages and logics with a solid mathematical foundation. This includes specificacion languages (VDM, Z, B, Event-B, OBJ, Alloy, ...), functional programming languages (Haskell, Erlang, λ-calculi…), logic programming languages (Prolog, CLP, ASP,…) among others.

Some basic knowledge of logic and functional and logic programming is assumed as a prerequisite.

Some goals of the course are:

• To motivate the use of declarative technologies in software development.
• To study the different families of declarative languages.
• To understand the differences between declarative and procedural languages and the impact of these aspects in software development.
• To identify the better niches for the industrial application of declarative technologies.

Material

General papers on formal methods

• Seven Myths of Formal Methods. Anthony Hall. IEEE Software, September 1990.
• Seven More Myths of Formal Methods. Jonathan P. Bowen, Michael G. Hinchey. IEEE Software, July 1995.
• Ten Commandments of Formal Methods. Jonathan P. Bowen, Michael G. Hinchey.
• Ten Commandments of Formal Methods... Ten Years Later. Jonathan P. Bowen, Michael G. Hinchey. IEEE Computer, January 2006.
• Verified Software: theories, tools, experiments. Vision of a Grand Challenge Project. Tony Hoare and Jay Misra, July 2005.
• Verified Software: A Grand Challenge. Cliff Jones, Peter O'Hearn, Jim Woodcock. IEEE Computer, April 2006.
• First Steps in the Verified Software Grand Challenge. Cliff Jones, Peter O'Hearn, Jim Woodcock. IEEE Computer, April 2006.
• A Specifier's Introduction to Formal Methods Jeanette M. Wing. IEEE Computer, 1990.
• Formal Specification: a Roadmap. Axel van Lamsweerde.

General references on logic

Any good book / class notes on first order logic will do. These are some reference we found useful in the past.

• Larry Paulson's Class notes and slides of the University of Cambridge. Recommended.
• Logic in Computer Science. Michael Huth, Mark Ryan. Cambridge University Press, 2001 (1st ed.), 2004 (2nd ed.). There should be copies in the School's library.
• Mathematical Logic for Computer Science. Mordechai Ben-Ari. Springer, 2001. There should be copies in the School's library.

References / material on Event-B

Note: these references can be updated as the course proceeds.

• The ultimate source of material for Event-B is the Event-B web portal.
• Faultless systems: yes we can!. A paper promoting the use of mathematical methods to ensure software integrity and dependability.
• A high-level view of the Event-B development and refinement model. This is a good, short introduction to the theory underlying the way EventB tackles the refinement of models. A must-read.
• The more complete reference for the Even-B method is the book Modeling in Event-B. Jean-Raymond Abrial. Cambridge University Press, 2010. We have copies in the library. Please get in touch with me if you need additional copies.
  • There is an errata sheet.
  • Chapters 1 (introduction) and 2 (controlling cars in a bridge) are freely available.
  • All the slides corresponding to the book chapters are available online! I recommend having a look at them in case of doubt as they are quite extensive. Rodin project files with the refinement are also available.
• Summary of mathematical notation plus notes on proofs, deduction, predicate and propositional calculus, set theory, arithmetic.
• Syntax reference card for Event-B.
• Summary of the mathematical toolkit of Event-B.

Classroom material (to be updated):

• Requirements, specifications, and building systems according to them.
• General introduction to Event-B.
• Development of a system to control cars in a bridge NOTE: updated by adding a couple of explanatory slides and merging some other slides. No real change on contents.
• Breaking news! Videos of the use of the Rodin platform to:
  • Write and validate the initial model.
  • Introduce the first refinement, correct, and verify it.
  • Introduce the variant for the new events (several attempts) and prove it correct.
  • Introduce and prove the deadlock-freedom property in the first model.
  • Prove deadlock freedom in second model without using deadlock freedom in first model using interactive theorem proving.
  Note: if the files do not play directly on your browser, please download them to your disk and play them from there. They use fairly standard codecs and containers. If still not working, consider using the VLC video player.
• Development of a program to search in a vector.
• Summary of proof obligations.
• Rodin can use a set of plugins with theorem provers from the Atelier B project. They are available as buttons in Rodin for simpler use. The reference manual for Atelier B gives some information on what these theorem provers do.
• We have posted information on the proposed term projects.
• Project / team assignment:
  • Team 1 (Project A): Reik Muller, Filip Wisniewski, Manuella Djambou.
  • Team 2 (Project B): Herbert Gómez, Maria Teresa Santillan, Darwin Vera.
  • Team 3 (Project A): Deepika Badampudi, Olena Kutsenko, Peerachai Kaowichakorn.
  • Team 4 (Project B): Detzabeth Pineda, Marco Molina, Fernando Fernandez.
  • Team 5 (Project B): Natalya Pasischnik, Diego Yucra, Ivan Brondino.

References on OBJ and algebraic specification

• Introducing OBJ. Joseph A. Goguen, Timothy Winkler, José Meseguer, Kokichi Futatsugi and Jean-Pierre Jouannaud.
• Algebraic Specification. Martin Wirsing. A chapter in the Handbook of Theoretical Computer Science, Vol. B: Formal Models and Semantics. Elsevier, 1990. ISBN 0 444 88074 7
• All About Maude -- A High Performance Logical Framework. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C. Lecture Notes in Computer Science, vol. 4350. [online version]

References on Z

• The Essence of Z Ed Currie. Pearson, 1999.
• The Z Notation. A Reference Manual. J.M. Spivey. Prentice Hall, 1989. ISBN 0-13-983768-X.
• Z: An Introduction to Formal Methods (2nd. ed.). Antoni Diller. John Wiley & Sons, 1994. ISBN 0-471-93973-0.
• Software Development with Z. J.B. Wordsworth. Addison-Wesley, 1992.

References on declarative programming

• Introduction to Functional Programming Using Haskell, 2nd. ed. Richard Bird. Prentice-Hall, 1998.
• Functional Programming A.J. Field, P.G. Harrison. Addison Wesley, 1988.
• The Art of Prolog: Advanced Programming Techniques Leon Sterling, Ehud Shapiro. The MIT Press, 1998 (2nd. ed.).
• Programming with Constraints: An Introduction Kim Marriott, Peter Stuckey. The MIT Press 1999 (2nd. ed.)

Office hours

Every lecturer has six hours for supervision, usually four fixed ones and two more on demand:

Julio Mariño: TBD

Manuel Carro: TBD

Homework

This is a list of the pending homework with links to the supplementary material (when appropriate) plus dates to hand it in.

Software

1. Event-B:
   • The Rodin platform.
2. Z
   • Style for typesetting Object Z specs in LateX.
   • The Community Z Tools at SourceForge.

Tentative schedule (can be updated as the course proceeds)

Sep. 14: Presentation lecture
Sep. 21: General introduction to formal methods
Sep. 28: Lecture cancelled
Oct. 5: Event-B: philosophy and hands-on introduction (cars in a bridge, with proof obligations)
Oct. 12: Holidays
Oct. 19: Event-B: cars in a bridge, with proof obligations (cont.)
Oct. 26: Event-B: cars in a bridge, with proof obligations (cont.)
Nov. 2: Event-B: cars in a bridge, with proof obligations (cont.)
Nov. 9: Holidays
Nov. 16: Event-B: search in a vector, with proof obligations and code generation
Nov. 23: Event-B: summary of proof obligations
Nov. 30: Alloy and lightweight formal methods
Dic. 7: Maude and algebraic specifications
Dic. 14: Maude and algebraic specifications (cont.)
Dic. 21: Program verification
Dic. 28: Christmas holidays
Jan. 4: Christmas holidays
Jan. 11: Term paper presentations
Jan. 18: Term paper presentations

Mailing lists

The mailing list of the course is at http://clip.dia.fi.upm.es/cgi-bin/mailman/listinfo/rsd. (Most of) You have already been subscribed. If you have not, please subscribe. Announcements, etc. will go through this mailing list. Please check also that the address in the mailing list is one that you usually consult.

Last modified: Thu Nov 24 17:00:04 CET 2011