Implementation relations and testing for cyclic systems: adding probabilities

This paper concerns the systematic testing of robotic control software based on state-based models. We focus on cyclic systems that typically receive inputs (values from sensors), perform computations, produce outputs (sent to actuators) and possibly change state. We provide a testing theory for such cyclic systems where time can be represented and probabilities are used to quantify non-deterministic choices, making it possible to model probabilistic algorithms. In addition, refusals, the inability of a system to perform a set of actions, are taken into account. We consider several possible testing scenarios. For example, a tester might only be able to passively observe a sequence of events and so cannot check probabilities, while in another scenario a tester might be able to repeatedly apply a test case and so estimate the probabilities of sequences of events. These different testing scenarios lead to a range of implementation relations (notions of correctness). As a consequence, this paper provides formal definitions of implementation relations that can form the basis of sound automated testing in a range of testing scenarios. We also validate the implementation relations by showing how observers can be used to provide an alternative but equivalent characterisation.

URI

http://hdl.handle.net/10454/19414

Version

Published version

Citation

Nunez M, Hierons RM and Lefticaru R (2023) Implementation relations and testing for cyclic systems: adding probabilities. Robotics and Autonomous Systems. 165: 104426.

Link to Version of Record

https://doi.org/10.1016/j.robot.2023.104426

Type

Article