An Operational Guide to Monitorability  

Luca Aceto

Reykjavik University and Gran Sasso Science Institute, L'Aquila

Abstract

Monitorability underpins the technique of Runtime Verification because it delineates what properties can be verified at runtime. Although many definitions of monitorability exist, few are defined explicitly in terms of the operational guarantees provided by monitors, which are the computational entities carrying out the verification. We view monitorability as a spectrum, where the fewer guarantees that are required of monitors, the more properties become monitorable. Accordingly, we present a monitorability hierarchy based on this trade-off. For regular specifications, we give syntactic characterisations in Hennessy–Milner logic with recursion for its levels. Finally, we map existing monitorability definitions into our hierarchy. Our work gives a unified framework that makes the operational asumtions and guarantees of each definition explicit. This provides a rigorous foundation that can inform design choices and correctness claims for runtime verification tools.

This presentation is based on joint work with Antonis Achilles (Reykjavik University), Adrian Francalanza (University of Malta), Anna Ingólfsdótt (Reykjavik University) and Karoliina Lehtinen (University of Liverpool).

Biography

Luca Aceto is a professor of Computer Science at Reykjavik University, Iceland, and at the Gran Sasso Science Institute, L'Aquila, Italy. Previously, he held permanent academic positions at the University of Sussex, UK, and at Aalborg University, Denmark. He is an elected member of Academia European, the Academy of Europe. He was the President of the European Association for Theoretical Computer Science from July 2012 till July 2016, and a
co-founder and first chair of the IFIP WG 1.8 on Concurrency Theory. He currently serves as the chair of the editorial board of LIPIcs. Luca Aceto's research has mostly focused on concurrency theory (with emphasis on process calculi), structural operational semantics, logic in computer science and runtime monitoring. He received a Distinguished Dissertation Award of the British Computer Society in 1991 and the Reykjavik University Research Award in 2012.

 برگزار کننده: دانشگاه خاتم              زمان: چهارشنبه 24 دیماه 1399 ساعت: 15:30          مهلت ثبت‌نام: ۲۳ دی‌ماه ۱۳۹۹

از کلیه دانشجویان و علاقه‌مندان گرامی دعوت می‌شود در زمان مقرر در این سخنرانی شرکت نمایند. (سخنرانی به زبان انگلیسی می‌باشد.)

لطفا جهت شرکت در سخنرانی (رایگان)، فرم ثبت‌نام (الزامی) را از طریق آدرس و یا QR Code درج شده در زیر تکمیل فرمایید.

سخنرانی به صورت آنلاین می‌باشد. پس از ثبت‌نام، اطلاعات و نحوه شرکت در رویداد از طریق ایمیل اطلاع‌رسانی می‌گردد.