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/2017:__General introduction.-
__18/10/2017:__Introduction to Event-B witht the slides up-to-date -
__25/10/2017:__No lecture (attending conference) -
__31/10/2017:__Lecture corresponding to Thursday 1/11/2017 (holidays) and up-to-date slides covering: event example, simple invariants, invariant establisment -
__2/11/2017:__Sequent calculus, deduction rules, invariant proofs, (non-)inductive invariant, termination, postconditions. Up-to-date Slides. Very recommended reading: sections 3.3, 6.4, and 6.5 of Logic and Proof (Lawrence Paulson's course notes). A very good book to read: Logic in Computer Science: Modelling and Reasoning about Systems. __8/11/2017__Slides on Refinement (first part). Searching in a sorted array. Constants, invariants. Proofs for refinement. A Model which performs a random search and refinement which performs a random search in a narrowing window. This model contains only the proofs that RODIN performs automatically.

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.
- A survey on loop
invariants. Section 3.2 has tips on how to find out invariants
and Section 4 includes examples of invariants for many common
algorithms.
**Note:**it only deals with sequential systems.

- 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.
- > 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 at SourceForge.
- The handbook for Rodin is also online. It does not correspond the latest tool version: some details differ, but the basic ideas remain.
- Installation instructions for RODIN.
- The
*Atelier B Provers*plugin is necessary for any non-trivial development. Install it 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 course examples will not work. - Interesting sections of the manual
**(Read them and have them in you bookmarks)**: - How to set up a Rodin project (but we will see it in the lectures).
- Hints on discharging proofs using RODIN. Do read it. It has many hints and information on how to use the built-in and external theorem provers.
- An explanation of the proving perspective from the user interface point of view.
- A catalog of the proof obligations generated by RODIN and their meaning.
- A list of the rewriting rules in the default Event B prover (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.