Monitoring Cumulative Non-functional Properties
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 MayDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:00 - 11:30 | |||
10:00 30mTalk | 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 30mTalk | 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 30mTalk | 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 |
Go directly to this room on Clowdr