Loading...
Implementation relations and testing for cyclic systems with refusals and discrete time
Lefticaru, Raluca Hierons, R.M. Núñez, M.
Lefticaru, Raluca
Hierons, R.M.
Núñez, M.
Publication Date
2020-12
End of Embargo
Supervisor
Rights
© 2020 Elsevier. Reproduced in accordance with the publisher's self-archiving policy. This manuscript version is made available under the CC-BY-NC-ND 4.0 license (http://creativecommons.org/licenses/by-nc-nd/4.0/)
Peer-Reviewed
Yes
Open Access status
Accepted for publication
2020-07-10
Institution
Department
Awarded
Embargo end date
Additional title
Abstract
We present a formalism to represent cyclic models and study di erent semantic frameworks that support testing. These models
combine sequences of observable actions and the passing of (discrete) time and can be used to specify a number of classes of
reactive systems, an example being robotic systems. We use implementation relations in order to formally define a notion of
correctness of a system under test (SUT) with respect to a specification. As usual, the aim is to devise an extension of the classical
ioco implementation relation but available timed variants of ioco are not suitable for cyclic models. This paper thus defines new
implementation relations that encapsulate the discrete nature of time and take into account not only the actions that models can
perform but also the ones that they can refuse. In addition to defining these relations, we study a number of their properties
and provide alternative characterisations, showing that the relations are appropriate conservative extensions of trace containment.
Finally, we give test derivation algorithms and prove that they are sound and also are complete in the limit.
Version
Accepted manuscript
Citation
Lefticaru R, Hierons RM and Núñez M (2020) Implementation relations and testing for cyclic systems with refusals and discrete time. The Journal of Systems & Software. 170: 110738.
Link to publisher’s version
Link to published version
Link to Version of Record
Type
Article