Métodos Formais em Engenharia de Software
Cálculo de Sistemas de Informação
Programação Ciber-física
Verificação Formal
Calendário | Sumários
Anos anteriores


Cyber-Physical Programming


Introduction and objectives

Welcome to the webpage of the module “Cyber-Physical Programming”, edition 2022/2023.

Cyber-physical systems are networks of computational devices that closely interact with physical processes in order to reach a prescribed goal; for example a desired velocity, a desired temperature or, more generally, a desired energy level. They range from small medical devices, such as pacemakers and insulin pumps, to networks of autonomous vehicles and district-wide smart grids. This module is devoted to such systems.

The main learning goal is two-fold: 1) to prepare the student to a disciplined way of developing and analysing cyber-physical systems, by presenting their basic principles, adequate models of computation, and respective tools; 2) and to introduce the student to the main limitations of the area’s state-of-the-art – via pedagogical illustrations extracted from real world-scenarios involving e.g. cruise controllers, sampling algorithms, and timed variants of concurrent algorithms.

At the end of the module, the student will:



16 Feb. 2023 Introduction to the module and its dynamics (slides-1)
23 Feb. 2023 Labelled transition systems and their role as semantics objects. The Calculus of Communicating Systems (slides-2)
2 Mar. 2023 Equivalence of Labelled Transition Systems. (slides-2)
16 Mar. 2023 Formalisation of Timed Automata and its composition (slides-3)
22 Mar. 2023 Compensation lecture: Semantics and equivalence of Timed Automata (slides-3)
23 Mar. 2023 Introduction to the UPPAAL model checker (slides-4)
30 Mar. 2023 Verification using CTL in UPPAAL (slides-4)
13 Apr. 2023 Operational semantics of simple languages. Recalling Haskell (slides) (code)
20 Apr. 2023 Implementations of different semantics in Haskell. Introduction to hybrid semantics (slides) (code)
27 Apr. 2023 A zoo of hybrid programs. Exercises. (slides)
04 May 2023 Continuation of the previous lecture. A brief overview of simply-typed lambda calculus. (slides) (slides)
18 May 2023 Continuation of the previous lecture. lambda-calculus with algebraic operations. (slides) (slides)
25 May 2023 Working with monads (code).


Assessment consist of the following items:


Rajeev Alur and David L Dill. A theory of timed automata. Theoretical computer science, 126(2):183--235, 1994. [ bib ]

Thomas A Henzinger. The theory of hybrid automata. In Verification of digital and hybrid systems, pages 265--292. Springer, 2000. [ bib ]

Glynn Winskel. The formal semantics of programming languages: an introduction. MIT press, 1993. [ bib ]

Sergey Goncharov, Renato Neves, and José Proença. Implementing hybrid semantics: From functional to imperative. In International Colloquium on Theoretical Aspects of Computing, pages 262--282. Springer, 2020. [ bib ]

Miran Lipovaca. Learn you a haskell for great good!: a beginner's guide. no starch press, 2011. [ bib ]

Philip Wadler. Monads for functional programming. In International School on Advanced Functional Programming, pages 24--52. Springer, 1995. [ bib ]

This file was generated by bibtex2html 1.99.

Supplementary bibliography

Bart Jacobs. Introduction to coalgebra, volume 59. Cambridge University Press, 2017. [ bib ]

Chucky Ellison and Grigore Rosu. An executable formal semantics of c with applications. ACM SIGPLAN Notices, 47(1):533--544, 2012. [ bib ]

This file was generated by bibtex2html 1.99.


The day and time for appointments is Wednesday afternoon (Renato Neves) or Thursday morning (José Proença). Please email us the day before if you wish to meet. If you prefer you can also just send an email with your questions to Renato Neves or to José Proença, or we can try to book an online meeting.