Document Actions

Formal Methods in Software Engineering

FORMAL METHODS IN SOFTWARE ENGINEERING

 

Course track

  • Current course tinynew.gif (2009/10) (classes started on the 1st of October) -- main text in Portuguese, notes in English
  • Previous course (2008/09)
  • Previous course (2007/08)

 

About the course

FMSE is a curricular unit offered by the FAST (Foundations and Applications of Software Technology) Group, according to the Bologna recommendations (2nd cycle).

It is an annual course (300 hours) wholly devoted to formal methods related topics and their application to industrial problems. It credits for 30 ECTS in the Bologna system.

 

Background

This unit stems from nearly 25 years of experience at Minho in teaching, researching and applying rigorous methods in the construction of software. Its main aim is to provide a consistent and solid answer to the requirements and challenges of the information age.

By resorting to the formal foundations of modelling, reasoning, programming and testing, this offer bears a special mark into the way future professionals are trained to meet high-quality standards in the design of software solutions to real-life problems. This aim is captured by the following «stamp», which software professionals should endeavour to be able to stick to IT products and services:

FMSE consists of four 5 ETCS modules on specialized topics which are linked together by a 10 ECTS lab module which acts as knowledge integration bus. This structure is intended to support the unit's overall aim of ensuring that solid theoretical knowledge finds its way to practice and real-life application.

 

Staff

 

ACM Classification

According to IEEE/ACM Curriculum Guidelines for Software Engineering:

  • Software/SOFTWARE ENGINEERING/Metrics --- 2
  • Software/SOFTWARE ENGINEERING/Requirements/Specifications --- 6
  • Software/SOFTWARE ENGINEERING/Software Architectures --- 6
  • Software/SOFTWARE ENGINEERING/Software/Program Verification --- 6
  • Software/SOFTWARE ENGINEERING/Testing and Debugging --- 4
  • Theory of Computation/LOGICS AND MEANINGS OF PROGRAMS/Specifying and Verifying and Reasoning about Programs --- 6

 

Required background

  • Experience in programming
  • Familiarity with declarative languages (logical, functional):
  • Predicate logic, lambda calculus and discrete mathematics at first cycle level.

 

Learning Outcomes

  • Create, analyse, refine, classify, animate, test, transform and calculate with abstract models of requirements in software engineering.
  • Transform specifications of complex information systems into efficient implementations on diverse technologies and platforms.
  • Model, analyse, classify and transform component interaction patterns, modular strategies (components, objects, services) and software architectural schemes.
  • Specify, express, and verify the validity of properties (correctness or other properties) of software systems, with the help of automatic and assisted proof tools.
  • Perform software quality control and plan / execute projects in software testing.
  • Document and justify software design decisions based on accurate software modelling and reasoning.
  • Manage software engineering projects in an integrated way from conception to implementation, testing and deployment.

     

    Contents

    FMSE consists of 4 thematic modules worth 5 ECTS each, linked together by a laboratorial ``bus'' of 10 ECTS (the so-called Cohesive Project) which ensures experimentation and practical application of the units main learning outcomes. Current thematic modules are as follows:

    ISC
    Information Systems by Calculation
    AMC
    Software Analysis, Modeling and Checking
    SFV
    Software Formal Verification
    PSA
    Processes and Software Architectures