An approach to testing specifications (Preliminary Draft)

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

An approach to testing specifications (Preliminary Draft)

Source

Proceedings of the ACM SIGSOFT/SIGPLAN software engineering symposium on High-level debugging table of contents

Pages: 53 - 59

Year of Publication: 1983

ISBN:0-89791-111-3

Authors

C. Jard
G. V. Bochmann

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): n/a, Downloads (12 Months): n/a, Citation Count: 1

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/800007.808008 What is a DOI?

ABSTRACT

An approach to testing the consistency of specifications is explored, which is applicable to the design validation of communication protocols and other cases of step-wise refinement. In this approach, a testing module compares a trace of interactions obtained from an execution of the refined specification (e. g. the protocol specification) with the reference specification (e. g. the communication service specification). Non-determinism in reference specifications presents certain problems. Using an extended finite state transition model for the specifications, a strategy for limiting the amount of non-determinacy is presented. An automated method for constructing a testing module for a given reference specification is discussed. Experience with the application of this testing approach to the design of a Transport protocol and a distributed mutual exclusion algorithm is described.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	K. A. Bartlett and D. Rayner, "The certification of data communication protocols", Proc. IEEE Symp. on Comp. Network Protocols, Washington DC, May 1980, pp. 12-17.
	2	G. V. Bochmann and C. A. Sunshine, "Formal methods in communication protocol design", IEEE Trans. COM-28, 4 (April 1980), pp. 624-631.
	3	G. V. Bochmann, "A General Transition Model for Protocols and Communication Services", IEEE Trans. on Communications, Vol. COM 28, 4 (April 1980), pp. 643-650.
	4	G. V. Bochmann, E. Cerny and C. Lacaille, "Formal specification of a Transport service", Département d'IRO, Université de Montréal, also WASH-9 of ISO TC97/SC16/WGI ad hoc group on FDT.
	5	G. V. Bochmann and A. Léveillé, "Formal specification of a Transport protocol", Département d'IRO, Université de Montréal.
	6	G. V. Bochmann and M. Raynal, "Structured specification of communicating systems", Publ. 428, Département d'IRO, Université de Montréal, 1982.
	7	J. M. Ayache, P. Azéma and M. Diaz, "Observer: a concept for detecting at run time control errors in concurrent systems", LAAS, presented at the IEEE Fault Tolerant Computing Symposium, Madison, June 1979.
	8	M. Cagné, "Un compilateur pour un langage de spécification", Document de travail 120, Dec. 1981.
	9	J. Goguen, "Thoughts on specification, design and verification", ACM Software Eng. Notes 5, 3 (July 1980), pp. 29-33.
	10	"Tutorial on formal description techniques (FDT)", ISO TC97/SC 16 N, (Canada)
	11	C. Jard, "Définition d'un modèle de simulation pour la validation de protocoles", Note technique CNET Lannion, - Département EVP - NT/LAA/SLC/49 (June 1981).
	12	C. Jard, "Spécification et validation d'un algorithme distribué d'exclusion mutuelle. Mise en oeuvre de la simulation: méthode et résultants", Note technique CNET Lannion, Département EVP, NT/LAA/SLC/93 (July 1982).
	13	Leslie Lamport, Time, clocks, and the ordering of events in a distributed system, Communications of the ACM, v.21 n.7, p.558-565, July 1978 [doi>10.1145/359545.359563]