Syllabus

Module aims to cover:

• • Theoretical and practical aspects associated with the formal development of software systems.

  • Theoretical and practical aspects associated with simulation, verification, and visualisation of software systems.

General Objective: Use of a high-level notation to formally develop critical systems, as well as study theoretical and practical aspects associated with the simulation, verification, and visualisation of models.

Course Content:

• • Introduction to the development of critical systems

    • • Software engineering challenges

      • Software reliability and dependability

  • Overview of formal methods

    • • When to use formal methods

      • Formal methods approaches

      • Applications and tools

  • Review of Formal Logic

    • • Propositional logic

      • Predicate logic

  • Review of Discrete Mathematics

    • • Sets, relations, and functions

      • Sequences

  • B method

    • • Abstract machines

      • Sets, relations, functions, and sequences in B

      • Modelling non-determinism

      • Data refinement

      • Refinement of non-determinism

      • Implementations

      • Model simulation and verification

      • Introduction to proofs in B

      • Model visualisation in B

      • Code generation

Basic Bibliography:

• • SCHNEIDER, Steve. The B-Method. Palgrave, 2001.

  • ClearSy. B language – reference manual. Version 1.8.6.

  • MOOC by IMD (UFRN): The B-Method (https://mooc.imd.ufrn.br/).

  • O’REGAN, Gerard. Concise Guide to Formal Methods: Theory, Fundamentals and Industry Applications. Springer, 2017.

Additional Bibliography:

• • ALAGAR, Vangalur; PERIYASAMY, Kasilingam. Specification of Software Systems. Springer, 2nd edition, 2011.

  • ABRIAL, Jean-Raymond. The B-book: Assigning Programs to Meanings. Cambridge University Press, 1996.