Software Architecture and Calculi 2019-20

Perfil de Métodos Formais em Engenharia de Software

Dep. Informática, Universidade do Minho

Funcionamento da UC a partir de 16 Março 2020

A UC seguirá o método de ensino flipped classroom, que se adapta especialmente bem a aulas não presenciais e irá envolver as seguintes acções, entre outras:

Objectives

The course provides a perspective on process algebra (architecture & calculi).

We start with well-established classical and probabilistic process algebras and illustrate their use in software engineering.

Given the rapid emergence of cyber-physical systems, we next give a special focus to timed and cyber-physical process algebras.

Finally, we lean on more uniform notions and techniques in process algebra, with the goal of giving theoretical foundations to the student and the tools necessary for (s)he to smoothly learn/adapt to modeling and reasoning about software composition in different computational paradigms.

This final part of the course will have a more theoretical, research-centred character, briefly presenting current research challenges.

Syllabus

Summaries (2019-20)

  • Feb 6: Introduction to the course dynamics.

    Labelled transition systems. Determinism, non determinism and probabilism. Corresponding notions of morphism. Bisimilarity. [slides]

  • Feb 13: Process algebra. Detailed study of CCS (Milner's Calculus of Communicating Systems): Operational semantics, expansion theorem; silent transitions and observational equivalences. [slides]

  • Feb 20: Process algebra: conclusion of the previous lecture. Exercises.

  • Feb 27: Modal logics for processes. The Hennessy-Milner theorem. [slides]

    Classification of transition systems. The probabilistic case. Variants. [slides]

  • Mar 5: Process modelling and verification in mCRL2 [slides 1] [slides 2].

    Discussion of examples [code].

  • Mar 12: CANCELLED: Covid-19 preventive determination

  • Mar 19: Timed Automata: syntax, semantics, and notions of equivalence. Examples and exercises [slides].

  • Mar 26: Hands-on UPPAAL [slides].

  • Apr 2: Hybrid Automata: syntax, semantics, and notions of equivalence. Examples and exercises [slides].

  • Apr 16: Revisions and exercises [exercises]. Presentation of the first project.

  • Apr 23: Simply-typed lambda-calculus and algebraic theories. Introduction to monads. [slides, auxiliar material].

  • Apr 30: Continuation of the previous class. Distinction between values and computations; tensorial strength. The computational meta-language [slides, the adventurers].

  • Mai 7: Revision of the previous classes. A tour around the Zoo of monads (cyber-physical, nondeterministic, internal state, and others). Monad combination. The Knight's quest. [slides, The Knight's quest].

    • Support

    Notes
    Links

    Bibliography

    Pragmatics

    Assessment

    A avaliação do aluno consistirá na realização de dois trabalhos práticos + apresentação (totalizando 90%) e TPCs que serão pedidos ao longo do ano lectivo (10%). Os trabalhos práticos serão realizados por grupos de dois alunos, enquanto que os TPCs serão realizados individualmente.
    1º Trabalho prático (45%)
    O primeiro trabalho prático vai incidir na modelação e análise de um sistema de tempo-real com base na ferramenta UPPAAL. Datas relevantes:
    2º Trabalho prático (45%)
    O segundo trabalho prático terá um caracter mais exploratório. Irá incidir não só incidir na modelação e análise de um sistema ciber-físico mas também num estudo comparativo de diferentes ferramentas para modelação/análise de sistemas ciber-físicos. Datas relevantes:
    Lecturers

    Contact