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 |

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 course is devoted to such systems.

Our main goal is to make the student an adept of the engineering discipline of cyber-physical systems – by presenting the respective basic principles, computational models, tools, and current limitations. The course involves several pedagogical illustrations extracted from real world-scenarios involving e.g. cruise controllers, sampling algorithms, and timed variants of concurrent algorithms.

Date | Description |
---|---|

08 feb. 2024 | Introduction to the module and its logistics (slides) |

14 feb. 2024 | Introduction to CCS. Exercises (slides) |

22 feb. 2024 | Introduction to the theory of timed automata. Exercises (slides) |

28 feb. 2024 | Continuation of the previous lecture. UPPAAL, the philosophers, and the adventurers (slides and video) |

07 mar. 2024 | Continuation of the previous lecture. Verification of timed systems with UPPAAL (slides and adventurers) |

14 mar. 2024 | Operational semantics of simple languages. Recalling Haskell (slides and code) |

21 mar. 2024 | Continuation of the previous lecture. Operational semantics of a hybrid while-language (slides and code) |

04 apr. 2024 | A Zoo of hybrid programs and design patterns (slides and code) |

11 apr. 2024 | Continuation of the previous lecture. Brief introduction to lambda-calculus (slides and code) |

18 apr. 2024 | Continuation of the previous lecture. Lambda-calculus with algebraic operations (slides) |

02 may 2024 | Semantics of Lambda-calculus with algebraic operations. Exercises (slides) (code) |

The assessment is comprised of the following items:

- Two individual sets of exercises to do at home (30%). (TPC-1) (TPC-2)
- Two group assignments (70%). (TP1) (TP2 and Code)

The day and time for appointments is Wednesday afternoon. Please email me the day before if you wish to meet. If you prefer you can also send an email with your questions, or we can have an online meeting.

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.*

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.*