European Master in Software Engineering

Master
on Software and Systems

Jump directly to: Overview | Lecturers and office ours | Mailing lists | General papers | Logic and computer science | Event B | Floyd-Hoare / Dafny | Maude | Property-based testing

__13/09:__General introduction.

There are many ways to approach these
goals. The *rigorous* 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.

In this course we will give a hands-on overview of several rigorous software development methods, including both those which follow a "correctness by construction" approach and those which gear more towards verifying software written separately.

Therefore, some goals of the course are:

- To motivate the use of technologies in software development under the correctness-by-construction paradigm.
- To study different families of languages and technologies aimed at easing the process of building correct software.
- 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 / correctness by construction technologies.

Knowledge of formal (first-order) logic, proof techniques, functional and logic programming is assumed as a prerequisite.

- Manuel Carro office 036 at the IMDEA Software
Institute and D-3323 (under appointment) - mcarro |at| fi DOT upm
DOT es Office hours: send me a mail to get an
appointment.

- Julio Mariño D-2310 - jmarino |at| fi DOT upm DOT es Office hours: send me a mail to get an appointment.

- A collection of Software horror stories. The video of the Ariane 5 incident is a well known case.
- Some examples of the use of formal methods in industry.
- The challenge of producing verified software and some advances. The project goes on.
- A survey on the current applications of formal methods in industrial settings.
- A brief account of several formal specification methods and the road ahead.
- J. R. Abrial's Faultless Systems: Yes, we Can. A rationale for modern rigorous development methods by the creator of Event B.

- Lawrence Paulson's Logic and Proof notes and slides. Very good introduction to a series of topics related with logic. We advise reading at least the part related to propositional logic and first order logic, including proof systems.
- Michael Huth and Mark Dermot Ryan's Logic in Computer Science: Modelling and Reasoning about Systems, available in printed form at the Schools library. This is a truly delightful book that we personally recommend reading back to back. It relates logic with many areas of Computer Science with clear examples and is likely to open your perception of what logic and Computer Science have in common.
- Mathematical Logic for Computer Science. Mordechai Ben-Ari. Springer, 2001. There should be copies in the School's library.

- The most comprehensive reference about Event B is the book Modeling in Event-B: System and Software Engineering, published by Cambridge University Press. There is an errata sheet. The School has at least one copy. Parts of the book, as well as supporting material, are freely available at the Event B website. All the slides corresponding to the book chapters are available online. They are not a substitute for the book but they are almost self-explanatory. Rodin project files for the projects in every chapter are also available.
- A summary of the Event B language.
- A reference card with the deduction rules, the structure of Event B models and events, the formal definition of the proof obligations, and the ASCII syntax to write the symbols in Event B.
- Slides presenting the inference rules, overview of first-order predicate calculus, set theory, and relations.
- An introduction to the Event-B method with a description of its phases.
- A paper about refinement and decomposition in Event B. It is probably too abstract and advanced for the aims of this course, but the first five sections can probably be understood without too many problems.

- Homepage of the latest version of the Rodin Event B development method. Please ensure that this is actually the latest version by checking the Core Rodin homepage.
- Please find here installation instructions.
- Of all the plugins, the most interesting for us is the
*Atelier B Provers*. Install them by going to`Help`⇒`Install new software`⇒ select`Atelier B Provers`⇒ Select in box ⇒ Click`Next`⇒ Follow instructions. If you do not install these provers, most of the examples in the course will not work out of the box! - The handbook for Rodin is also online.
- All of the rewriting rules in the default Event B prover (this is extracted from the Event B website).

- Slides on Floyd-Hoare logic.
- Exercise sheet on program verification (Hoare logic and Dafny).

- Exercise sheet on algebraic specification using Maude.
- 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.
- An introduction to Maude.
- A manual for Maude.

- The source code used in my QuickCheck demo (Haskell).
- A short essay explaining how to use Erlang QuickCheck for testing Java programs.