Write a Blog >>
FormaliSE 2021
Tue 18 - Fri 21 May 2021
co-located with ICSE 2021
Thu 20 May 2021 10:00 - 10:30 at FormaliSE Room - Monitoring & Biological systems

This paper considers the problem of decentralized monitoring of a class of non-functional properties (NFPs) with quantitative operators, namely cumulative cost properties. The decentralized monitoring of NFPs can be a non-trivial task for several reasons: (i) they are typically expressed at a high abstraction level where inter-event dependencies are hidden, (ii) NFPs are difficult to be monitored in a decentralized way, and (iii) lack of effective decomposition techniques. We address these issues by providing a formal framework for decentralized monitoring of LTL formulas with quantitative operators. The presented framework employs the tableau construction and a formula unwinding technique (i.e., a transformation technique that preserves the semantics of the original formula) to split and distribute the input LTL formula and the corresponding quantitative constraint in a way such that monitoring can be performed in a decentralized manner. The employment of these techniques allows processes to detect early violations of monitored properties and perform some corrective or recovery actions. We demonstrate the effectiveness of the presented framework using a case study based on a Fischertechnik training model, a sorting line which sorts tokens based on their color into storage bins. The analysis of the case study shows the effectiveness of the presented framework not only in early detection of violations, but also in developing failure recovery plans that can help to avoid serious impact of failures on the performance of the system.

Thu 20 May

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:00 - 11:30
Monitoring & Biological systemsFormaliSE 2021 at FormaliSE Room
10:00
30m
Talk
Monitoring Cumulative Non-functional Properties
FormaliSE 2021
Omar Al Bataineh National University of Singapore, Singapore, Arvind Easwaran Nanyang Technological University, Daniel Jun Xian Ng Nanyang Technological University, Singapore
Pre-print Media Attached
10:30
30m
Talk
Feasibility of Spatial Model Checking for Nevus Segmentation
FormaliSE 2021
Gina Belmonte Azienda Toscana Nord Ovest S. C. Fisica Sanitaria Nord, Lucca, Italy, Giovanna Broccia ISTI-CNR, FMT Lab, Vincenzo Ciancia Istituto di Scienza e Tecnologie dell'Informazione "A. Faedo", Consiglio Nazionale delle Ricerche, Pisa, ITALY, Diego Latella ISTI-CNR, Pisa, Italy, Mieke Massink CNR-ISTI Pisa, Italy
Pre-print Media Attached
11:00
30m
Talk
Formal characterization and efficient verification of a biological robustness property
FormaliSE 2021
Lucia Nasti Università di Pisa - Dipartimento di Informatica, Roberta Gori University of Pisa, Paolo Milazzo University of Pisa - Department of Computer Science
Pre-print Media Attached

Information for Participants
Thu 20 May 2021 10:00 - 11:30 at FormaliSE Room - Monitoring & Biological systems
Info for room FormaliSE Room:

Go directly to this room on Clowdr