Abstract
A systematic refinement transformation of a program involving processes communicating through simple rendez-vous type connections is described. Both new connections and new processes are introduced in the refined program form. The refinement is based in the concept of Communications Extended Abstract Type (CAT), which is also covered, and it amounts to either selecting, or unhiding, a CAT implementation.
This refinement approach is made possible in the framework of a notation, PADD, which treats parallelism and parametric abstract types as two independent entities, combining them simply. Then, the operations of CAT implementations may involve parallel internal composition. As a consequence, a CAT may have both behavioral (unrefined) as well as structural (refined) implementations.
A framework for the organization and partition of correctness proofs, including timing aspects, is given. It is based on the refinement method and the CAT concept. The constructs and tools associated with the method are being incorporated into The Llull System (TLS), the current environment for the PADD notation, being used both at the university and industry.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
O. J. Dahl, B. Myhrhang, and K. Nygaard, Simula 67 Common Base Language, Norsk Regnesentral, Oslo, Norway, 1968.
O. J. Dahl, ‘Hierarchical program structures', In Structured Programming, Academic Press, New York, 1972.
B. Liskov, J. Guttag, Abstraction and Specification in Program Development, Mc-Graw Hill 1986.
R. W. Witty, Small scale software engineering, PhD Dissertation, Department of Computer Science, Brunel University, Uxbridge, UK, September 1981.
C.A.R. Hoare, Communicating Sequential Processes, Comm. ACM, Vol. 21, N. 8, August 1978.
C.A.R. Hoare, Communicating Sequential Processes, Prentice-Hall, Englewood Cliffs, N.J., 1985.
A.W. Roscoe, C.A.R. Hoare, The laws of OCCAM programming, Oxford University Computing Laboratory, Programming Research Group Report, Tech. Monograph PRG-53, February 1986.
R. Milner, A Calculus of Communicating Systems, Springer-Verlag, 1980.
R. Milner, Communication and Concurrency, Prentice-Hall 1989.
Michael Yoeli, Ed., Formal Verification of Hardware Design, IEEE Computer Society Press, Los Alamitos, California, 1990.
ISO DIS 8807: Information Processing Systems. Open System Interconnection. LOTOS A Formal Description Technique based on the Temporal Ordering of Observational Behavior, July 1988.
F. Alvarez-Cuevas, F. Oller, M. Bertran, J. Selga, ‘A Novel Algorithm for Voice Synchronization in Packet Switching Networks', IEEE Network Magazine, September 1993.
M. Bertran, F. Oller, F. Alvarez-Cuevas, A. Duran, M. Porta, ‘The Llull system (TLS). An integration of formalism and simulation for parallel-distributed and real-time software synthesis and development', Proc. Third AMAST Workshop on Real-Time Systems, Salt-Lake City, Utah, March 6–8, 1996.
M. Bertran, F. Alvarez-Cuevas, ... ‘A design environment with simulation and formal verification', Proc. 5th IEEE Communications. Soc. Computer Aided Modeling and Design of Communication Links and Networks, CAMAD'94, Princeton, New Jersey, USA, April 24–27, 1994.
M. Bertran, F. Oller, ... ‘An Environment for DSP System Development with Extended Abstract Types, and Dimensional Design (PADDE)', Proc. IEEE Intl. Conf. A.S.Signal Processing, ICASSP-93, Minneapolis, USA, April 1993, pp. I-449 to I-452.
M. Bertran, ‘PADD: A Schema Notation Integrating Parallelism and Abstraction', Report, E.T.S.E.Telecom. (UPC), Barcelona, Autumn 1989. Also in Proc. IEEE Com. soc. CAMAD'92, Montebello, Quebec, Canada, 29 sept.–2 oct., 1992.
M. Bertran, ‘On a Formal Definition and Application of Dimensional Design', Software — Practice and Experience, Vol. 18(11), pp 1029–1045 (November 1988).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bertran, M., Alvarez-Cuevas, F., Duran, A. (1997). Communication Extended Abstract Types in the refinement of parallel communicating processes. In: Bertran, M., Rus, T. (eds) Transformation-Based Reactive Systems Development. ARTS 1997. Lecture Notes in Computer Science, vol 1231. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63010-4_18
Download citation
DOI: https://doi.org/10.1007/3-540-63010-4_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63010-4
Online ISBN: 978-3-540-69058-0
eBook Packages: Springer Book Archive