Cyber-Physical Computation 2021/2022


Introduction and objectives

Welcome to the webpage of the module "Cyber-Physical Computation", edition 2021/2022.

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. 2022 Introduction to the module and its dynamics (slides)
23 Feb. 2022 Labelled transition systems and their role as semantics objects. The Calculus of Communicating Systems (slides)
25 Feb. 2022 The semantics of CCS (slides). Exercises.
02 Mar. 2022 Observational Behaviour and Observational Equivalence (slides)
04 Mar. 2022 Continuation of the previous lecture. Exercises (slides)
09 Mar. 2022 Introduction to timed automata (slides).
11 Mar. 2022 Continuation of the previous lecture. Exercises (slides).
16 Mar. 2022 Observational equivalence for timed automata (slides).
18 Mar. 2022 Introduction to Uppaal.
23 Mar. 2022 Extra features of Uppaal. The logic CTL and its application to the verification of Timed Systems (slides).
25 Mar. 2022 Tackling the adventurers' problem with Uppaal (description of the problem).
30 Mar. 2022 Continuation of the previous lecture.
06 Apr. 2022 Recalling Haskell (file).
08 Apr. 2022 Continuation of the previous lecture (file). Presentation and discussion of the first practical assignment.
20 Apr. 2022 A simple While-language and its semantics (slides).
27 Apr. 2022 A hybrid While-language and its semantics (slides).
29 Apr. 2022 Continuation of the previous lecture (slides).
04 May 2022 A zoo of hybrid programs and common mistakes in hybrid programming (slides).
06 May 2022 Introduction to the simply-typed lambda-calculus(slides).
13 May 2022 Continuation of the previous lecture (slides).
17 May 2022 Integration of algebraic effects in lambda-calculus (slides).
20 May 2022 Contexts and tensorial strength. Exercises (slides).
25 May 2022 Several examples of monads at work (code).
27 May 2022 The Knight's quest and the Monty Hall problem (code).

Assessment

Assessment will consist of the following items:

  • Individual assynchronous test (20%); TPC-1, TPC-2.
  • Group assignment: modelling and analysis of a cyber-physical system via Uppaal (40%); TP-1.
  • Group assignment: modelling and analysis of a cyber-physical system via Haskell (40%);TP-2,Code.

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 ]


This file was generated by bibtex2html 1.99.

Contact

The day and time for appointments is Wednesday afternoon (but please send an email the day before if you wish to meet). If you prefer you can also just send an email with your questions to Renato Neves

Author: Renato Neves

Created: 2022-04-07 Thu 09:02

Validate