Introduction and objectives
Welcome to the webpage of the module “Cyber-Physical Computation”,
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
- 14 feb. 2023 – Introduction to the module and its dynamics (slides-1)
- 21 feb. 2023 - Formalising and reasoning over labelled transition systems (slides-2)
- 28 feb. 2023 - Equivalence of labelled transition systems (slides-2)
- 3 mar. 2023 - Exercises on equivalences; Introduction to Timed automata (slides-3)
- 14 mar. 2023 - Formalisation of Timed Automata (TA) and its composition (slides-3)
- 17 mar. 2023 - Exercises on the composition of TA; Semantics TA (slides-3)
- 21 mar. 2023 - Semantics and equivalence of Timed automata (slides-3)
- 24 mar. 2023 - Introduction to UPPAAL model checker (slides-4)
- 28 mar. 2023 - Modelling in Uppaal and introduction to CTL (slides-4)
- 31 mar. 2023 - Verification using CTL in UPPAAL (slides-4)
- 31 mar. 2023 - Compensation lecture: modelling adventurers on a bridge (Instructions) (My solution)
- 11 apr. 2023 - Operational semantics of simple languages. Recalling Haskell (Slides) (Code)
- 14 apr. 2023 - Implementations of different semantics in
Haskell (Code)
- 18 apr. 2023 - Introduction to hybrid semantics (Slides)
- 28 apr. 2023 - A zoo of hybrid programs (Slides)
- 02 may 2023 - A brief overview of simply-typed lambda-calculus (Slides)
- 05 may 2023 - Continuation of the previous lecture (Slides)
- 16 may 2023 - lambda-calculus and algebraic operations (Slides)
- 19 may 2023 - Written assessment.
- 23 may 2023 - Working with monads (Code)
Assessment
Assessment consist of the following items:
- Two individual sets of exercises to do at home.
- Individual test (30% - 19th May);
- Group assignment (40% - 26th June);
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 ]
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 ]
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.