Projects per year
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, so it 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 used 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 discusses this approach and demonstrates its
feasibility by presenting its implementation on top of a framework integrating the Agent Java PathFinder model checker. A high-level
Domain Specific Language is used to model the environment in a user-friendly way; the latter is then compiled to trace expressions
for both static formal verification and runtime verification. To evaluate our approach, we apply it to two different case studies, an
autonomous cruise control system, and a simulation of the Mars Curiosity rover
represents an abstraction of the actual environment, so it 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 used 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 discusses this approach and demonstrates its
feasibility by presenting its implementation on top of a framework integrating the Agent Java PathFinder model checker. A high-level
Domain Specific Language is used to model the environment in a user-friendly way; the latter is then compiled to trace expressions
for both static formal verification and runtime verification. To evaluate our approach, we apply it to two different case studies, an
autonomous cruise control system, and a simulation of the Mars Curiosity rover
Original language | English |
---|---|
Journal | ACM Transactions on Software Engineering and Methodology |
Volume | 30 |
Issue number | 4 |
DOIs | |
Publication status | Published - 10 May 2021 |
Fingerprint
Dive into the research topics of 'Towards a Holistic Approach to Verification and Validation of Autonomous Cognitive Systems'. Together they form a unique fingerprint.Projects
- 2 Finished
-
Novel Locomotion for Extreme Environments (Space)
Smith, K. (PI), Parslew, B. (CoI) & Weightman, A. (CoI)
16/03/20 → 31/03/21
Project: Research
-
Robotics and Artificial Intelligence for Nuclear (RAIN)
Lennox, B. (PI), Arvin, F. (CoI), Brown, G. (CoI), Carrasco Gomez, J. (CoI), Da Via, C. (CoI), Furber, S. (CoI), Luján, M. (CoI), Watson, S. (CoI), Watts, S. (CoI) & Weightman, A. (CoI)
2/10/17 → 31/03/22
Project: Research