Recognising assumption violations in autonomous systems verification

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.