Go to:
Esta página em português Ajuda Autenticar-se
Clube de Leitura FEUP :: Vamos a Livros
You are here: Start > EIC0039

Site map
Edifício A (Administração) Edifício B (Aulas) - Bloco I Edifício B (Aulas) - Bloco II Edifício B (Aulas) - Bloco III Edifício B (Aulas) - Bloco IV Edifício C (Biblioteca) Edifício D (CICA) Edifício E (Química) Edifício F (Minas e Metalurgia) Edifício F (Minas e Metalurgia) Edifício G (Civil) Edifício H (Civil) Edifício I (Electrotecnia) Edifício J (Electrotecnia) Edifício K (Pavilhão FCNAUP) Edifício L (Mecânica) Edifício M (Mecânica) Edifício N (Garagem) Edifício O (Cafetaria) Edifício P (Cantina) Edifício Q (Central de Gases) Edifício R (Laboratório de Engenharia do Ambiente) Edifício S (INESC) Edifício T (Torre do INEGI) Edifício U (Nave do INEGI) Edifício X (Associação de Estudantes)

Formal Methods in Software Engineering

Code: EIC0039     Acronym: MFES

Classification Keyword
OFICIAL Software Engineering

Instance: 2018/2019 - 1S Ícone do Moodle

Active? Yes
Web Page: http://moodle.up.pt/
Responsible unit: Department of Informatics Engineering
Course/CS Responsible: Master in Informatics and Computing Engineering

Cycles of Study/Courses

Acronym No. of Students Study Plan Curricular Years Credits UCN Credits ECTS Contact hours Total Time
MIEIC 158 Syllabus since 2009/2010 4 - 6 56 162

Teaching Staff - Responsibilities

Teacher Responsibility
Ana Cristina Ramada Paiva

Teaching - Hours

Lectures: 2,00
Recitations: 2,00
Type Teacher Classes Hour
Lectures Totals 1 2,00
Ana Cristina Ramada Paiva 2,00
Recitations Totals 6 12,00
João Carlos Pascoal Faria 4,00
Flávio Henrique Ferreira Couto 4,00
Ana Cristina Ramada Paiva 4,00
Mais informaçõesLast updated on 2018-09-17.

Fields changed: Components of Evaluation and Contact Hours

Teaching language



1- BACKGROUND Students should have knowledge about software processes and software modelling.

2- SPECIFIC AIMS To develop abstraction capabilities in order to describe what the system should do and not the way to do it. Be familiar with formal methods and the way they can contribute to increase the quality of software systems.

3- PREVIOUS KNOWLEDGE Software engineering; Computing Theory; Algorithm design and analysis.

4- PERCENT DISTRIBUTION Scientific component:75% Technological component:25%

5- LEARNING OUTCOMES At the end of the course students should be able to: - Apply formal methods of specification (based on models, based on properties, based on behavior) and verification ("Model-checking, formal proofs and test) in the development of software systems. - Identify existing formal methods and know when they should be applied and which are most suitable in each case.

Learning outcomes and competences

At the end of the course, students should be able to specify a software system in a declarative way, to distinguish the various existing formal methods and when to apply them and realize the usefulness of these techniques for improving the quality of software systems.

Working method



1. Introduction
1.1 What are formal methods?
1.2 Importance and applicability of formal methods in the development of software
1.3 Life cycle models and software development processes by incorporating formal methods.
1.4 Specification, refinement, implementation, verification and validation
1.5 Classification of formal methods
1.6 Explicit vs. implicit models, executable vs. non-executable
1.7 Formal verification techniques

2. Formal Events
2.1 Proof of program correction. Application of Hoare logic to proof of algorithm correction.
2.2 A correct programming approach by construction. Program refinement techniques.
2.3 The Dafny tool.

3. Alloy Constraint Analyser for modelling and semantic analysis
3.1 Declarative modelling
3.2 Difference related to model checking
3.3 Alloy commands
3.4 Functions; predicates; facts; assertions and verifications (checks)
3.5 Static vs. dynamic modelling
3.6 Simulation of an operation
3.7 Check safety properties
3.8 Alloy analyser tool

4. Model Based Specification
4.1 VDM-SL and VDM++ languages
4.2 Data representation based on mathematical structures (sets, sequences, finite functions)
4.3 State and non-state specification
4.4 Definition of types, values and functions
4.5 Definition of classes, instance variables and operations
4.6 Expressions and instructions
4.7 Design-by-contact: definition of invariables, preconditions and postconditions
4.8 Description of algorithms, executable specifications
4.9 Analysis of specification consistency
4.10 Connection of VDM++ to UML
4.11 Code generation from a formal specification
4.12 VDMTools

Mandatory literature

Daniel Jackson; Software Abstractions, MIT Press, 2006. ISBN: 0-262-10114-9
Fitzgerald, John; Validated designs for object-oriented systems. ISBN: 1-85233-881-4
Derrick G. Kourie, Bruce W. Watson; The correctness-by-construction approach to programming. ISBN: 978-3-642-27918-8

Complementary Bibliography

Alagar, V. S.; Specification of software systems. ISBN: 0-387-98430-5
Richard Bornat; Proof and Disproof in Formal Logic, Oxford University Press, 2005. ISBN: 0-19-8530269

Teaching methods and learning activities

Theoretical classes will be based on the presentation of the themes of the course. Practical classes will be based on exercises, so that students can contact with the various tools available and to do their assignments.


Alloy Analyzer


Technological sciences > Technology > Computer technology > Software technology
Technological sciences > Engineering > Computer engineering

Evaluation Type

Distributed evaluation without final exam

Assessment Components

Designation Weight (%)
Teste 60,00
Trabalho laboratorial 40,00
Total: 100,00

Amount of time allocated to each course unit

Designation Time (hours)
Estudo autónomo 60,00
Frequência das aulas 52,00
Trabalho laboratorial 50,00
Total: 162,00

Eligibility for exams

Students have to reach a minimum mark of 40% in the continuous assessment component. The presence in the practical classes is recorded and mandatory according to existing legislation.
Minimum of 40% in every interim exam.

Calculation formula of final grade

Distributed evaluation without final exam, with the following components:
(A) Practical work - (40% of the final mark), minimum grade of 40%.
(B) Mini exam1 - 1h30m (30% of the final mark), minimum grade of 40%.
(C) Mini exam2 - 1h30m (30% of the final mark), minimum grade of 40%.

Final grade = (A) * 40% + (B) * 30% + (C) * 30%

Examinations or Special Assignments

Practical work of VDM++: delivery on the 3rd January; defense of practical work between 4 and 10 January.

The defense of practical work is mandatory for ALL students.

Special assessment (TE, DA, ...)

Students excused from attendance at practical classes should contact the teacher for special sessions of follow up. The defense of practical work is mandatory for ALL students.

Classification improvement

- The marks obtained in practical work can be improved in the next edition of the discipline
- The classification of the interim tests can be improved by in the appeal exame.


Students with class attendance in the previous year will have to take both interim exams. The marks obtained in the previous year in the work of VDM++ will be used as a mark for the work in VDM++ of this edition.

Recommend this page Top
Copyright 1996-2019 © Faculdade de Engenharia da Universidade do Porto  I Terms and Conditions  I Accessibility  I Index A-Z  I Guest Book
Page generated on: 2019-03-19 at 18:01:49