nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

An Implementation Relation for Cyclic Systems with Refusals and Discrete Time

verfasst von : Raluca Lefticaru, Robert M. Hierons, Manuel Núñez

Erschienen in: Software Engineering and Formal Methods

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

This paper explores a particular type of model, a cyclic model, in which there are sequences of observable actions separated by discrete time intervals, introduces a novel implementation relation and studies some properties of this relation. Implementation relations formalise what it means for an unknown model of the system under test (SUT) to be a correct implementation of a specification. Many implementation relations are variants of the well known ioco implementation relation, and this includes several timed versions of ioco. It transpires that the timed variants of ioco are not suitable for cyclic models. Our implementation relation encapsulates the discrete nature of time in cyclic models and takes into account not only the actions that models can perform but also the ones that they can refuse at each point of time. We prove that our implementation relation is a conservative extension of trace containment and present two alternative characterisations.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Local Nontermination Detection for Parallel C++ Programs

Nächstes Kapitel Modular Indirect Push-Button Formal Verification of Multi-threaded Code Generators

https://tinyurl.com/nyf64av.

We will say that a state is stable if it is not possible to take a transition whose label is an output or an internal action.

Ammann, P., Offutt, J.: Introduction to Software Testing, 2nd edn. Cambridge University Press, Cambridge (2017)

Binder, R.V., Legeard, B., Kramer, A.: Model-based testing: where does it stand? Commun. ACM 58(2), 52–56 (2015)CrossRef

Briones, L.B., Brinksma, E.: A test generation framework for quiescent real-time systems. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol. 3395, pp. 64–78. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31848-4_5CrossRef

Cavalcanti, A., Ribeiro, P., Miyazawa, A., Sampaio, A., Conserva Filho, M., Didier, A.: RoboSim reference manual. Technical report, University of York (2019)

Cavalcanti, A., et al.: Verified simulation for robotics. Sci. Comput. Program. 174, 1–37 (2019)CrossRef

Cavalli, A.R., Higashino, T., Núñez, M.: A survey on formal active and passive testing with applications to the cloud. Ann. Telecommun. 70(3–4), 85–93 (2015)CrossRef

van Glabbeek, R.: The linear time-branching time spectrum I. The semantics of concrete, sequential processes. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, chapter 1, North Holland (2001)

Harel, D.: Statecharts: a visual formulation for complex systems. Sci. Comput. Program. 8(3), 231–274 (1987)CrossRef

Heerink, L., Tretmans, J.: Refusal testing for classes of transition systems with inputs and outputs. In: 19th Joint International Conference on Protocol Specification, Testing, and Verification and Formal Description Techniques, FORTE/PSTV 1999, pp. 23–38. Chapman & Hall (1997)

10.

Hierons, R.M., et al.: Using formal specifications to support testing. ACM Comput. Surv. 41(2), 9:1–9:76 (2009)CrossRef

11.

Hierons, R.M., Bowen, J.P., Harman, M. (eds.): Formal Methods and Testing. LNCS, vol. 4949. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78917-8CrossRef

12.

World Robotics 2018: International Federation of Robotics. Statistical Department (2018)

13.

ISO/IEC JTCI/SC21/WG7, ITU-T SG 10/Q.8: Information Retrieval, Transfer and Management for OSI; Framework: Formal Methods in Conformance Testing. Committee Draft CD 13245–1, ITU-T proposed recommendation Z.500. ISO - ITU-T (1996)

14.

Krichen, M., Tripakis, S.: Conformance testing for real-time systems. Form. Methods Syst. Des. 34(3), 238–304 (2009)CrossRef

15.

Marinescu, R., Seceleanu, C., Le Guen, H., Pettersson, P.: A research overview of tool-supported model-based testing of requirements-based designs. In: Advances in Computers, chapter 3, vol. 98, pp. 89–140. Elsevier (2015)

16.

Miyazawa, A., Ribeiro, P., Li, W., Cavalcanti, A., Timmis, J., Woodcock, J.: RoboChart: modelling and verification of the functional behaviour of robotic applications. Softw. Syst. Model. (2019, to appear)

17.

Myers, G.J., Sandler, C., Badgett, T.: The Art of Software Testing, 3rd edn. Wiley, Hoboken (2011)

18.

Phillips, I.: Refusal testing. Theor. Comput. Sci. 50(3), 241–284 (1987)MathSciNetCrossRef

19.

Rohmer, E., Singh, S.P., Freese, M.: V-REP: aversatile and scalable robot simulation framework. In: 26th IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2013, vol. 1, pp. 1321–1326. IEEE Computer Society (2013)

20.

Roscoe, A.W.: Understanding Concurrent Systems. Texts in Computer Science. Springer, London (2010). https://doi.org/10.1007/978-1-84882-258-0CrossRefMATH

21.

Schmaltz, J., Tretmans, J.: On conformance testing for timed systems. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 250–264. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-85778-5_18CrossRefMATH

22.

Shafique, M., Labiche, Y.: A systematic review of state-based test tools. Int. J. Softw. Tools Technol. Transf. 17(1), 59–76 (2015)CrossRef

23.

Tretmans, J.: Model based testing with labelled transition systems. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) Formal Methods and Testing. LNCS, vol. 4949, pp. 1–38. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78917-8_1CrossRef

Titel: An Implementation Relation for Cyclic Systems with Refusals and Discrete Time
verfasst von: Raluca Lefticaru
Robert M. Hierons
Manuel Núñez
Verlag: Springer International Publishing
Buch: Software Engineering and Formal Methods
Print ISBN: 978-3-030-30445-4

Electronic ISBN: 978-3-030-30446-1

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-30446-1_21

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner