Seminario di Informatica: “Temporal logic and formal verification for cyber-physical systems”

Giovedì 17 Novembre 2016, ore 11:30 - Aula 2AB40 - Davide Bresolin


Giovedì 17 Novembre 2016 alle ore 11:30 in Aula 2AB40, Davide Bresolin (Università di Padova) terrà un seminario dal titolo “Temporal logic and formal verification for cyber-physical systems”.

Cyber-Physical systems are characterized by the tight integration of cyber aspects (computing) with physical ones (e.g., mechanical, electrical, and chemical processes). Examples of such systems are autonomous robotic systems, multi-agent and embedded systems, automotive, aerospace and medical systems.
They need to operate under strong safety, performance, reliability and timing constraints. They are characterized by a mixed discrete and continuous behaviour that cannot be characterized faithfully using either discrete or continuous models only, and thus they need the development of new formalisms and new algorithmic techniques to be formally verified. This talks overviews my research activity in developing temporal logics and reachability analysis techniques for the verification of cyber-physical systems.

Download Seminari di Informatica