Abstract
A method is provided to reduce a labeled transition system while preserving testing equivalence. This method uses the refusal graph, an abstract structure for representing communicating systems, and two transformations for deriving a refusal graph from a labeled transition system and vice-versa. The reduced systems are in normal form for the testing equivalence and are minimal with respect to the bisimulation equivalence.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
E. Brinksma, G. Scollo, and C. Steenbergen. Lotos Specifications, their implementations and their tests. In B. Sarikaya and G.V. Bochmann, editors, Protocol Specification Testing and Verification, volume VI. Elsevier Science Publishers B.V., North-Holland, 1987.
R. Cleaveland and M. Hennessy. Testing Equivalence as Bisimulation Equivalence. In J. Sifaids, editor, Automatic Verification Methods for Finite State Systems, number 407 in Lecture Notes in Computer Science, pages 11–23, Grenoble-france, June 1989. Springer-Verlag.
K. Drira, P. Azéma, B. Soulas, and A.M. Chemali. Testability of a communicating system through an environment. In Proc. 4th International Join Conference on the Theroy and Practice of Software Development. TAPSOFT’93 (LNCS 668),ORSAY, FRANCE, April 1993.
Jean-Claude Fernandez, Hubert Garavel, Laurent Mounier, Anne Rasse, Carlos Rodriguez, and Joseph Sifakis. A toolbox for the verification of lotos programs. In Lori A. Clarke, editor, Proceedings of the 14th International Conference on Software Engineering ICSE’U (Melbourne, Australia),New-York, May 1992. ACM.
C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
R. Jacinto, G. Juanole, and K. Drira. On the application to OSI-TP of a Structured Analysis and Modelling Methodologie Based on Petri Nets Models. In Proceedings of the 4th IEEE Workshop on Future Trends in Distributed Computing Systems (FTDCS),Lisboa-Portugal, September 22–24 1993. To appear.
R. Milner. Communication and Concurrency.Prentice-Hall, 1989.
R. De Nicola and M.C.B. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83–133, 1984.
D. Park. Concurrency and automata on infinite sequences. In Lecture Notes in Computer Science, volume 104. Springer-Verlag, Berlin Heidelberg, 1981.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1994 British Computer Society
About this paper
Cite this paper
Drira, K., Azema, P. (1994). Verifying communication protocols via testing-projection. In: Nivat, M., Rattray, C., Rus, T., Scollo, G. (eds) Algebraic Methodology and Software Technology (AMAST’93). Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3227-1_26
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3227-1_26
Publisher Name: Springer, London
Print ISBN: 978-3-540-19852-9
Online ISBN: 978-1-4471-3227-1
eBook Packages: Springer Book Archive