UP | HOME
a_software.gif
tercer_nivel_software.gif

Rigorous software development

Coordinator(s)/Instructor(s)

Length

4 Credits (ECTS)

Prerequisites

Knowledge of first order logic, basics of theorem proving, basics of set theory, and declarative (logic and / or functional) programming.

This course has specific requirements, and if your initial level is not adequate, you may not pass. Therefore, we ask you to please include it in the mail you ought to send to graduate.school (at) software.imdea.org with the list of courses you want to take from the IMDEA track. You will receive a mail stating the courses in which you are welcome to enroll. If you enroll in an IMDEA Track course for which you did not receive explicit approval, you may be asked to switch over to a different one.

Course web page (if any)

http://lml.ls.fi.upm.es/rsd/

Summary and objectives

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 specification languages (Event-B, Z, OBJ, …), functional programming languages (Haskell, Erlang, λ-calculi, …), and logic programming languages (Prolog, CLP, …) among others.

Some basic knowledge of 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 understand the differences between declarative and procedural languages and the impact of these aspects in software development.
  • To identify niches for the industrial application of declarative technologies.

Topics

  • Introduction to rigorous software development and level exam.
  • The Z specification language.
  • Event B.
  • Algebraic specifications: Maude
  • Alloy

Evaluation

Homework will be periodically proposed. In addition to that, depending on the number of students, either one or more presentations will be made by every student, or a final exam will have to be passed.

Recommended reading

  • 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.
  • Introducing OBJ. Joseph A. Goguen, Timothy Winkler, José Meseguer, Kokichi Futatsugi and Jean-Pierre Jouannaud.
  • 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]
  • The Essence of Z Ed Currie. Pearson, 1999.
  • Modeling in Event-B. Jean-Raymond Abrial. Cambridge University Press, 2010.
  • Refinement, Decomposition, and Instantiation of Discrete Models. Jean-Raymond Abrial, Stefan Hallerstede. Fundamente Informatica, 77 (2007) 1-28.
  • Faultless systems: yes we can! Jean-Raymond Abrial. IEEE Computer.



Back to the initial page
Go to the IMDEA Software Institute page

Fractals are used with permission from their author Cory Ench | © 2006-2007. IMDEA Software.
All rights reserved | Legal Notice | Privacy Policy