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
Alumni

PCF/2022-23

Cyber-Physical Programming

2022/23

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:

know the basic principles and representative models of cyber-physical computation;
have a broad knowledge of languages, tools, and techniques for engineering cyber-physical systems;
be proficient with the tools Uppaal and Lince, which cover model checking, testing, and simulation for cyber-physical systems;
be able to understand in which ways the state-of-the-art (of cyber-physical computation and engineering) is limited, and the potential outcomes of solving these limitations.

Syllabus

Labelled transition systems, their role as semantic objects, and corresponding notions of equivalence;
Timed labelled transition systems and corresponding notions of equivalence, composition, and synchronisation. Zeno behaviour;
From theory to practice: the tool Uppaal;
A while-language and its operational semantics;
A hybrid while-language and its operational semantics;
From theory to practice: the tool Lince;
Cyber-physical behaviour as yet another computational effect: the notion of a monad, the hybrid monad, and monad combination.

Summaries

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)
16 Mar. 2023	Semantics of Timed Automata. Introduction to UPPAAL (slides-3 slides-4)

Assessment

Assessment consist of the following items:

Two individual sets of exercises to do at home.
- TPC1 (15%)
- TPC2 (15% - not yet available)
Individual test (30% - after all the lectures);
Group assignment: modelling and analysis of a cyber-physical system via Uppaal and via Haskell (40% - not yet available);

Bibliography

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 ]