Por Carlos Mão de Ferro.

A central problem of designing Cyber-Physical Systems (CPS) is to verify that the assembled subsystems behave as expected. The smallest mistake can render the whole system stuck or undergo unpredictable behaviors. Given that the number of systems being integrated can be extremely large (e.g. integrating thousands of sensors in a autonomous car), it is of utterly importance that the verification process is modular, automatic and ideally provide a visual feedback that is comprehensible for humans.

In this third and final seminar I will present the complete toolchain for programming CPS as proposed in my PhD. In particular, I will discuss how a domain-specific programming language can be analysed against a specification by using a verification algorithm that checks the integration of stateful systems and other safety properties (e.g., absence of deadlocks). This tool is able to verify systems with billions of systems in a few seconds on a personal computer. In an alternative scenario, I will also hint on how it might be possible to adapt an existing programming language (e.g., Python) to verify the same set of properties. As a final step in the toolchain, I will address the execution environment by showing examples of CPS programs that have been verified and can be deployed on an embedded device.

More information: https://moodle.ciencias.ulisboa.pt/course/view.php?id=2964#section-4

Transmissão em direto via Zoom.