Recognising Assumption Violations in Autonomous Systems Verification



Ferrando, Angelo ORCID: 0000-0002-8711-4670, Dennis, LA ORCID: 0000-0003-1426-1896, Ancona, Davide, Fisher, Michael and Mascardi, Viviana
(2018) Recognising Assumption Violations in Autonomous Systems Verification. In: Autonomous Agents and Multi-agent Systems, Stockholm, Sweden.

Access the full-text of this item by clicking on the Open Access link.
[img] Text
aamas18.pdf - Author Accepted Manuscript

Download (419kB)

Abstract

When applying formal verification to a system that interacts with the real world we must use a model of the environment. This model represents an abstraction of the actual environment, but is necessarily incomplete and hence presents an issue for system verification. If the actual environment matches the model, then the verification is correct; however, if the environment falls outside the abstraction captured by the model, then we cannot guarantee that the system is well-behaved. A solution to this problem consists in exploiting the model of the environment for statically verifying the system's behaviour and, if the verification succeeds, using it also for validating the model against the real environment via runtime verification. The paper reports on a demonstration of the feasibility of this approach using the Agent Java Pathfinder model checker. Trace expressions are used to model the environment for both static formal verification and runtime verification.

Item Type: Conference or Workshop Item (Unspecified)
Uncontrolled Keywords: Runtime Verification, Model Checking, Autonomous Systems, Trace expressions
Depositing User: Symplectic Admin
Date Deposited: 12 Jun 2018 09:06
Last Modified: 19 Jan 2023 01:32
Open Access URL: http://ifaamas.org/Proceedings/aamas2018/pdfs/p193...
Related URLs:
URI: https://livrepository.liverpool.ac.uk/id/eprint/3022440