{"id":265,"date":"2021-06-21T12:27:05","date_gmt":"2021-06-21T12:27:05","guid":{"rendered":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/?page_id=265"},"modified":"2022-11-25T19:02:51","modified_gmt":"2022-11-25T19:02:51","slug":"a-gentle-introduction-to-runtime-verification-of-autonomous-systems","status":"publish","type":"page","link":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/?page_id=265","title":{"rendered":"A Gentle Introduction to Runtime Verification of Autonomous Systems"},"content":{"rendered":"<p><img loading=\"lazy\" decoding=\"async\" class=\" alignright\" src=\"https:\/\/www.cse.chalmers.se\/~gersch\/foto.jpg\" width=\"225\" height=\"404\" \/><\/p>\n<h2><a href=\"https:\/\/www.cse.chalmers.se\/~gersch\/\">Gerardo Schneider<\/a>, <a href=\"https:\/\/www.chalmers.se\/en\/departments\/cse\/organisation\/fm\/Pages\/default.aspx\">Formal Methods Division<\/a>, <a href=\"https:\/\/www.chalmers.se\/cse\/EN\/\">Department of Computer Science and Engineering<\/a>, a shared department between <a href=\"https:\/\/www.chalmers.se\/en\/\">Chalmers<\/a> and the <a href=\"https:\/\/www.gu.se\/english\">University of Gothenburg<\/a>, Gothenburg, Sweden<\/h2>\n<div>The slides and the videos are available on <a href=\"https:\/\/ecampus.paris-saclay.fr\/course\/view.php?id=63482#section-3\">eCampus<\/a>.<\/div>\n<div><\/div>\n<div class=\"\">Autonomous cars and unmanned aerial vehicles (UAV) are examples of autonomous systems, which can operate autonomously and interact with each\u00a0other and with people in different (more or less) intelligent ways. They are\u00a0characterised by the kind of interaction between the system\u00a0and its environment and how they respond to changes in the environment. The design and deployment of autonomous systems, as for any other software system, must be done having in mind that the system satisfies certain functional and non-functional properties. One way to verify (and eventually guarantee) that the system is correct is by using formal methods.<\/div>\n<div class=\"\"><\/div>\n<div class=\"\">Runtime Verification (RV) \u00a0is a formal methods technique\u00a0that studies how to synthesise monitors from high-level formal specifications languages. RV focuses\u00a0on the problem of observing a single execution trace, providing a\u00a0formal framework for testing, debugging and monitoring, complementing other (static) verification techniques like model checking.<\/div>\n<div class=\"\"><\/div>\n<div class=\"\">The objective of this seminar is to introduce RV in general and provide some examples of its use in the context of autonomous systems. For that, I will first give an overview of RV, and then show different scenarios where such technique can be used in the context of autonomous systems. At the end I will present challenges and interesting research directions in the domain.<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Gerardo Schneider, Formal Methods Division, Department of Computer Science and Engineering, a shared department between Chalmers and the University of Gothenburg, Gothenburg, Sweden The slides and the videos are available on eCampus. Autonomous cars and unmanned aerial vehicles (UAV) are examples of autonomous systems, which can operate autonomously and interact with each\u00a0other and with people [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-265","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=\/wp\/v2\/pages\/265","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=265"}],"version-history":[{"count":10,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=\/wp\/v2\/pages\/265\/revisions"}],"predecessor-version":[{"id":440,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=\/wp\/v2\/pages\/265\/revisions\/440"}],"wp:attachment":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=265"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}