Specification, Verification and Synthesis in Cyberphysical Systems

          @misc{ scivideos_16952,
            doi = {},
            url = {https://simons.berkeley.edu/talks/cyber-physical-systems},
            author = {},
            keywords = {},
            language = {en},
            title = {Specification, Verification and Synthesis in Cyberphysical Systems},
            publisher = {The Simons Institute for the Theory of Computing},
            year = {2021},
            month = {jan},
            note = {16952 see, \url{https://scivideos.org/index.php/Simons-Institute/16952}}
          }
          

Abstract

Cyberphysical systems are roughly characterized as systems enabled by coordination between computational and physical components and resources. They appear in a vast range of applications. Most applications of cyberphysical systems are subject to strict requirements for---to name a few---safety, security, and privacy. Formal methods for specification, verification, and synthesis have the potential to provide the languages, tools, and discipline necessary to meet these strict requirements. On the other hand, this potential can be realized only through proper connections between formal methods and several other fields. This tutorial will provide an overview of the complications in the context of cyberphysical systems that may benefit---and have benefited---from formal methods. It will provide examples of problems whose solution heavily relies on formal methods: correct-by-construction synthesis of hierarchical control protocols; synthesis of strategies under limitations on information availability; and verifiability of learning-enabled components.