TY - GEN
T1 - Runtime Verification with Imperfect Information Through Indistinguishability Relations
AU - Ferrando, Angelo
AU - Malvone, Vadim
N1 - Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.
PY - 2022/1/1
Y1 - 2022/1/1
N2 - Software systems are hard to trust, especially when autonomous. To overcome this, formal verification techniques can be deployed to verify such systems behave as expected. Runtime Verification is one of the most prominent and lightweight approaches to verify the system behaviour at execution time. However, standard Runtime Verification is built on the assumption of perfect information over the system, that is, the monitor checking the system can perceive everything. Unfortunately, this is not always the case, especially when the system under analysis contains rational/autonomous components and is deployed in real-world environments with possibly faulty sensors. In this work, we present an extension of the standard Runtime Verification of Linear Temporal Logic properties to consider scenarios with imperfect information. We present the engineering steps necessary to update the verification pipeline, and we report the corresponding implementation when applied to a case study involving robotic systems.
AB - Software systems are hard to trust, especially when autonomous. To overcome this, formal verification techniques can be deployed to verify such systems behave as expected. Runtime Verification is one of the most prominent and lightweight approaches to verify the system behaviour at execution time. However, standard Runtime Verification is built on the assumption of perfect information over the system, that is, the monitor checking the system can perceive everything. Unfortunately, this is not always the case, especially when the system under analysis contains rational/autonomous components and is deployed in real-world environments with possibly faulty sensors. In this work, we present an extension of the standard Runtime Verification of Linear Temporal Logic properties to consider scenarios with imperfect information. We present the engineering steps necessary to update the verification pipeline, and we report the corresponding implementation when applied to a case study involving robotic systems.
KW - Autonomous Systems
KW - Imperfect Information
KW - Runtime Verification
UR - https://www.scopus.com/pages/publications/85140459127
U2 - 10.1007/978-3-031-17108-6_21
DO - 10.1007/978-3-031-17108-6_21
M3 - Conference contribution
AN - SCOPUS:85140459127
SN - 9783031171079
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 335
EP - 351
BT - Software Engineering and Formal Methods - 20th International Conference, SEFM 2022, Proceedings
A2 - Schlingloff, Bernd-Holger
A2 - Chai, Ming
PB - Springer Science and Business Media Deutschland GmbH
T2 - 20th International Conference on Software Engineering and Formal Methods, SEFM 2022
Y2 - 26 September 2022 through 30 September 2022
ER -