Yes / 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. / Engineering and Physical Sciences Research Council Grant numbers: EP/R025134/2. Ministerio de Economía y Competitividad Grant numbers: RTI2018-093608-B-C31. Comunidad de Madrid Grant numbers: S2018/TCS-4314
| Identifer | oai:union.ndltd.org:BRADFORD/oai:bradscholars.brad.ac.uk:10454/17953 |
| Date | 14 July 2020 |
| Creators | Lefticaru, Raluca, Hierons, R.M., Núñez, M. |
| Publisher | Elsevier |
| Source Sets | Bradford Scholars |
| Language | English |
| Detected Language | English |
| Type | Article, Accepted manuscript |
| 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/) |
Page generated in 0.0017 seconds