Repetitive Quiescence in Implementation and Testing (Extended Abstract)

G.J. Tretmans

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

5 Downloads (Pure)

Abstract

This paper studies implementation relations and testing based on labelled transition sys- tems, using the assumption that implementations communicate with their environment via inputs and outputs. Such implementations are formalized by restricting the class of transition systems to those systems that can always accept input actions. Implementation relations, which formalize the notion of correctness of these implementations with respect to labelled transition system specifications, are defined analogous to the theories of testing equivalence and preorder, and refusal testing. A test generation algorithm is given, which is proved to produce a sound and exhaustive test suite from a specification, i.e., a test suite that fully characterizes the set of correct implementations.
Original languageEnglish
Title of host publicationPartial-Order Reduzierung des Zustandsraumes bei der BDD-Modellprüfung
Subtitle of host publicationGI/ITG-Fachgespräch, 19. - 20. Juni 1997 in Berlin
EditorsA. Wolisz, I. Schieferdecker, A. Rennoch
Place of PublicationSankt Augustin
PublisherGMD-Forschungszentrum Informationstechnik GmbH
Pages23-37
Number of pages15
ISBN (Print)3-88457-315-2
Publication statusPublished - Jun 1997
EventFormale Beschreibungstechniken für verteilte Systeme 1997: GI/ITG-Fachgespräch - Berlin, Germany
Duration: 19 Jun 199720 Jun 1997

Publication series

NameGMD Studien
PublisherGMD-Forschungszentrum Informationstechnik GmbH
Volume315

Workshop

WorkshopFormale Beschreibungstechniken für verteilte Systeme 1997
CountryGermany
CityBerlin
Period19/06/9720/06/97

Fingerprint

Testing
Specifications
Acoustic waves

Keywords

  • FMT-TESTING

Cite this

Tretmans, G. J. (1997). Repetitive Quiescence in Implementation and Testing (Extended Abstract). In A. Wolisz, I. Schieferdecker, & A. Rennoch (Eds.), Partial-Order Reduzierung des Zustandsraumes bei der BDD-Modellprüfung: GI/ITG-Fachgespräch, 19. - 20. Juni 1997 in Berlin (pp. 23-37). (GMD Studien; Vol. 315). Sankt Augustin: GMD-Forschungszentrum Informationstechnik GmbH.
Tretmans, G.J. / Repetitive Quiescence in Implementation and Testing (Extended Abstract). Partial-Order Reduzierung des Zustandsraumes bei der BDD-Modellprüfung: GI/ITG-Fachgespräch, 19. - 20. Juni 1997 in Berlin. editor / A. Wolisz ; I. Schieferdecker ; A. Rennoch. Sankt Augustin : GMD-Forschungszentrum Informationstechnik GmbH, 1997. pp. 23-37 (GMD Studien).
@inproceedings{e3ce101191af4e48b060b9f49d9756bf,
title = "Repetitive Quiescence in Implementation and Testing (Extended Abstract)",
abstract = "This paper studies implementation relations and testing based on labelled transition sys- tems, using the assumption that implementations communicate with their environment via inputs and outputs. Such implementations are formalized by restricting the class of transition systems to those systems that can always accept input actions. Implementation relations, which formalize the notion of correctness of these implementations with respect to labelled transition system specifications, are defined analogous to the theories of testing equivalence and preorder, and refusal testing. A test generation algorithm is given, which is proved to produce a sound and exhaustive test suite from a specification, i.e., a test suite that fully characterizes the set of correct implementations.",
keywords = "FMT-TESTING",
author = "G.J. Tretmans",
year = "1997",
month = "6",
language = "English",
isbn = "3-88457-315-2",
series = "GMD Studien",
publisher = "GMD-Forschungszentrum Informationstechnik GmbH",
pages = "23--37",
editor = "A. Wolisz and I. Schieferdecker and A. Rennoch",
booktitle = "Partial-Order Reduzierung des Zustandsraumes bei der BDD-Modellpr{\"u}fung",

}

Tretmans, GJ 1997, Repetitive Quiescence in Implementation and Testing (Extended Abstract). in A Wolisz, I Schieferdecker & A Rennoch (eds), Partial-Order Reduzierung des Zustandsraumes bei der BDD-Modellprüfung: GI/ITG-Fachgespräch, 19. - 20. Juni 1997 in Berlin. GMD Studien, vol. 315, GMD-Forschungszentrum Informationstechnik GmbH, Sankt Augustin, pp. 23-37, Formale Beschreibungstechniken für verteilte Systeme 1997, Berlin, Germany, 19/06/97.

Repetitive Quiescence in Implementation and Testing (Extended Abstract). / Tretmans, G.J.

Partial-Order Reduzierung des Zustandsraumes bei der BDD-Modellprüfung: GI/ITG-Fachgespräch, 19. - 20. Juni 1997 in Berlin. ed. / A. Wolisz; I. Schieferdecker; A. Rennoch. Sankt Augustin : GMD-Forschungszentrum Informationstechnik GmbH, 1997. p. 23-37 (GMD Studien; Vol. 315).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Repetitive Quiescence in Implementation and Testing (Extended Abstract)

AU - Tretmans, G.J.

PY - 1997/6

Y1 - 1997/6

N2 - This paper studies implementation relations and testing based on labelled transition sys- tems, using the assumption that implementations communicate with their environment via inputs and outputs. Such implementations are formalized by restricting the class of transition systems to those systems that can always accept input actions. Implementation relations, which formalize the notion of correctness of these implementations with respect to labelled transition system specifications, are defined analogous to the theories of testing equivalence and preorder, and refusal testing. A test generation algorithm is given, which is proved to produce a sound and exhaustive test suite from a specification, i.e., a test suite that fully characterizes the set of correct implementations.

AB - This paper studies implementation relations and testing based on labelled transition sys- tems, using the assumption that implementations communicate with their environment via inputs and outputs. Such implementations are formalized by restricting the class of transition systems to those systems that can always accept input actions. Implementation relations, which formalize the notion of correctness of these implementations with respect to labelled transition system specifications, are defined analogous to the theories of testing equivalence and preorder, and refusal testing. A test generation algorithm is given, which is proved to produce a sound and exhaustive test suite from a specification, i.e., a test suite that fully characterizes the set of correct implementations.

KW - FMT-TESTING

M3 - Conference contribution

SN - 3-88457-315-2

T3 - GMD Studien

SP - 23

EP - 37

BT - Partial-Order Reduzierung des Zustandsraumes bei der BDD-Modellprüfung

A2 - Wolisz, A.

A2 - Schieferdecker, I.

A2 - Rennoch, A.

PB - GMD-Forschungszentrum Informationstechnik GmbH

CY - Sankt Augustin

ER -

Tretmans GJ. Repetitive Quiescence in Implementation and Testing (Extended Abstract). In Wolisz A, Schieferdecker I, Rennoch A, editors, Partial-Order Reduzierung des Zustandsraumes bei der BDD-Modellprüfung: GI/ITG-Fachgespräch, 19. - 20. Juni 1997 in Berlin. Sankt Augustin: GMD-Forschungszentrum Informationstechnik GmbH. 1997. p. 23-37. (GMD Studien).