Requirements Verification in CPSs

Speakers: Prof. Luca Pulina, Prof. Armando Tacchella, Dr. Simone Vuotto

When considering functional and non-functional requirements analysis in adaptive and/or reconfigurable CPSs, we face the problem of guaranteeing desired properties in implements capable of modifying their internal parameters to achieve and maintain a prescribed quality of service even in the face of a partially unknown and mutating environment. While adaptation is a desirable (non-functional) requirement for CPSs in many circumstances, most CPSs are deployed in applications where misbehaviour can cause serious damage to the surrounding environment, which makes requirement analysis mandatory. Unfortunately, adaptivity is conflicting with other requirements, e.g., safety: safety can be easily increased by reducing the amount of automatic reconfiguration, while changing internal parameters during operation may yield unsafe control policies. Goal of this tutorial is to explore techniques and tools that can support requirement analysis in the context of adaptive cyber-physical systems. The proposed tools and techniques are currently researched and developed in EU Horizon 2020 project CERBERO ( and in the RAS project PROSSIMO (