Formal Methods in Software Engineering

Code:

EIC0039

Acronym:

MFES

Keywords
Classification	Keyword
OFICIAL	Software Engineering

Instance: 2019/2020 - 1S

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	144	Syllabus since 2009/2010	4	-	6	56	162

Teaching language

English

Objectives

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

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 Discrete Mathematics; Algorithms and Data Structures; Algorithm Design and Analysis; Theory of Computation; Software Engineering.

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, properties, and behavior) and verification (formal proofs and model-checking) 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 unit, students should be able to formally specify and verify a software system, to distinguish between the various formal methods that exist and when to apply them and to understand the usefulness of these techniques for improving the quality of software systems.

Working method

Presencial

Pre-requirements (prior knowledge) and co-requirements (common knowledge)

Desirable pre-requisites: Discrete Mathematics; Algorithms and Data Structures; Algorithm Design and Analysis; Theory of Computation; Software Engineering.

Program

1. Introduction
1.1 What are formal methods.
1.2 Importance and applicability of formal methods in software development.
1.3 Formal methods in the software life cycle: specification, refinement, implementation, verification, and validation.
1.4 Classification of formal methods.
1.5 Formal verification techniques.

2. Formal program verification
2.1 Program verification with Hoare logic.
2.2 Program verification by weakest precondition calculus.
2.3 Introduction to the Dafny language (type system, program organization, specification and verification mechanisms, tools).
2.4 Specification and verification of imperative programs and algorithms in Dafny.
2.5 Design by contract and verification of data structures and object-oriented programs in Dafny.
2.6 Advanced specification and verification techniques in Dafny (data abstraction, refinement, lemmas, etc.).

3. Model checking of reactive systems
3.1 Modeling of reactive systems: transition and concurrency systems.
3.2 Linear temporal properties.
3.3 Temporal logic: linear (LTL) and branched (CTL and CTL *).
3.4 Model checkers.
3.5 Symbolic model checking: BDDs and OBDDs.
3.6 Decision algorithms based on finite automata.

Mandatory literature

Huth, M., & Ryan, M. ; Logic in Computer Science, Cambridge University Press, 2004. ISBN: 978-0-511-26401-6
Baier Christel; Principles of model checking, MIT Press, 2008. ISBN: 978-0-262-02649-9

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
Daniel Jackson; Software Abstractions, MIT Press, 2006. ISBN: 0-262-10114-9
Derrick G. Kourie, Bruce W. Watson; The correctness-by-construction approach to programming. ISBN: 978-3-642-27918-8

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.

Software

Spin
Dafny extension for Visual Studio Code
iSpin
Dafny
jSpin

keywords

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

Evaluation Type

Distributed evaluation without final exam

Assessment Components

Designation	Weight (%)
Teste	100,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

The presence in the practical classes, as well as theoretical classes with invited speakers, 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:
(MT1) Mini exam1 - up to 2h (50% of the final mark), minimum grade of 40%.
(MT2) Mini exam2 - up to 2h (50% of the final mark), minimum grade of 40%.

Examinations or Special Assignments

Students with a grade higher than 75% in the 1st mini-exam can develop an individual project (P) in Dafny for specifying, implementing and verifying a medium complexity algorithm or data structure not previously verified in Dafny. The final grade is calculated as 50% * max(P, MT1) + 50% * MT2.

There will be an appeal exam with two parts (corresponding to MT1 and MT2) that all students can access (provided they have met the attendance rules and have taken both mini-tests), to obtain approval or to improve their classification to one or both parties.

Classification improvement

The classification of the interim tests can be improved by in the appeal exam.

Observations

Invited talk on october, 10 (participation mandatory):  "Formal Method, Software Development and Safety Critical Systems" by Thierry Lecomte, ClearSy.