PSF - A Retrospective

Veltin, G.J.

Artykuł - szczegóły

Tytuł artykułu

PSF - A Retrospective

Autorzy

Veltin G.J.

Wybrane pełne teksty z tego czasopisma

https://fi.episciences.org/

Identyfikatory

Warianty tytułu

Języki publikacji

Abstrakty

Modern day computer architectures offer ever-increasing support for parallel processing, still it turns out to be quite difficult for programmers and therefore programs to tap into these parallel resources. To benefit from real general-purpose parallel computing we claim that it is likely that a paradigm shift is needed in the way we think about programming. This change of thought in turn will need to be reflected in future programming languages as well. We think that the field of process algebra provides thorough insight in how to reason about the construction of software for concurrent systems and will be one of the enabling technologies supporting this transition. The wish to connect process algebra, a mathematical theory, to the world of computer-readable and executable specifications led to the development of PSF (Process Specification Formalism). PSF is an implementation of the process algebra ACP (Algebra of Communicating Processes) integrating ASF (Algebraic Specification Formalism) to specify algebraic data types. One of the first publications on PSF appeared in Fundamenta Informaticae in 1990. Here we stated as the first sentence of the abstract: "Traditional methods for programming sequential machines are inadequate for specifying parallel systems". Unfortunately, though some advancements have been made since 1990, we can still uphold this statement 20 years later. This current report documents the developments that lead to the construction of PSF and the 1990 publication and moreover it also documents how PSF and its tools have evolved since 1990 taking the conclusion and the outlook for future work from the original article as a reference point. Using the knowledge gained both in constructing tools for PSF and in using PSF to specify concurrent systems, we will judge, discuss and criticise the design decisions taken and show paths for future developments.

Słowa kluczowe

process algebras algebraic data types concurrency parallel systems formal specifications ACP ASF PSF Algebra of Communicating Processes Process Specification Formalism Algebraic Specification Formalism

Wydawca

IOS Press

Czasopismo

Fundamenta Informaticae

Rocznik

2010

Tom

Vol. 100, nr 1/4

Strony

181--227

Opis fizyczny

Bibliogr. 93 poz.

Twórcy

autor

Veltin G.J.

University of Applied Sciences Emden/Leer, Constantiaplatz 4, 26723 Emden, Germany, gjv@imut.de

Bibliografia

[1] Anderson, E., Bai, Z., Dongarra, J., Greenbaum, A., McKenney, A., Du Croz, J., Hammerling, S., Demmel, J., Bischof, C., Sorensen, D.: LAPACK: A portable linear algebra library for high-performance computers, Proceedings of the 1990 conference on Supercomputing, IEEE Computer Society Press, 1990.
[2] ANSI/IEEE: Carrier Sense Multiple Access with Collision Detection, standard 802.3, 1985.
[3] ANSI/IEEE: Logical Link Control, standard 802.2, 1985.
[4] ANSI/IEEE: Token Ring Access Method, standard 802.5, 1985.
[5] Apple Inc.: Technology Brief, Grand Central Dispatch, 2009.
[6] Baeten, J., Bergstra, J. A., Mauw, S., Veltink, G. J.: A Process Specification Formalism Based on Static COLD, in: Algebraic Methods II: Theory, Tools and Applications [papers from a workshop in Mierlo, The Netherlands, September 1989] (J. A. Bergstra, L. M. G. Feijs, Eds.), vol. 490 of Lecture Notes in Computer Science, Springer, 1991, 303-335.
[7] Baeten, J. C.M.: Procesalgebra, Programmatuurkunde,Kluwer, Deventer, The Netherlands, 1986, In Dutch.
[8] Baeten, J. C.M.: A brief history of process algebra, Theoretical Computer Science, 335(2-3), 2005, 131-146.
[9] Baeten, J. C. M., Basten, T., Reniers, M. A.: Process algebra (equational theories of communicating processes), vol. 50 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge, 2010.
[10] Baeten, J. C. M., Bergstra, J. A.: Global renaming operators in concrete process algebra, Information and Computation, 78(3), 1988, 205-245.
[11] Baeten, J. C. M., Bergstra, J. A., Klop, J. W.: Conditional axioms and L/B calculus in process algebra, Proceedings, IFIP C"onf. on Formal Description of Programming Concepts-Ill Ebberup, 1986, 53-75.
[12] Baeten, J. C. M., Bergstra, J. A., Klop, J. W.: Syntax and defining equations for an interrupt mechanism in process algebra, Fundamenta Informaticae, IX, 1986, 127-168.
[13] Baeten, J. C. M., Bos, V.: Formalizing Programming Variables in Process Algebra, Technical Report 493, TUCS Software Construction Laboratory, Turku, Finland, 2002.
[14] Baeten, J. C. M., Weijland, W. P.: Process Algebra, vol. 18 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge, 1990.
[15] Bell, D., LaPadula, L.: Secure computer systems: Mathematical foundations, Technical report, Technical Report MTR-2547, 1973.
[16] Bergstra, J. A.: A mode transfer operator in process algebra, Technical Report P8808, Programming Research Group, University of Amsterdam, Amsterdam, 1988.
[17] Bergstra, J. A., Bethke, I., Ponse, A.: Process algebra with iteration and nesting, The Computer Journal, 37(4), 1994, 243.
[18] Bergstra, J. A., Heering, J., Klint, P., Eds.: Algebraic specification, ACM, New York, NY, USA, 1989, ISBN 0-201-41635-2.
[19] Bergstra, J. A., Heering, J., Klint, P.: The algebraic specification formalism ASF, in: Algebraic specification (J. A. Bergstra, J. Heering, P. Klint, Eds.), ACM, New York, NY, USA, 1989, ISBN 0-201-41635-2, 1-66.
[20] Bergstra, J. A., Klint, P.: The discrete time TOOLBUS a software coordination architecture, Science of Computer Programming, 31(2-3), 1998, 205-229.
[21] Bergstra, J. A., Klop, J. W.: Fixed point semantics in process algebras, Technical Report IW 206, Mathematical Centre, Amsterdam, 1982.
[22] Bergstra, J. A., Klop, J. W.: Process algebra for synchronous communication, Information and control, 60(1-3), 1984, 109-137.
[23] Bergstra, J. A., Klop, J. W.: Algebra of communicating processes with abstraction, Theoretical Computer Science, 37(1), 1985, 77-121.
[24] Bergstra, J. A., van der Weide, T. P.: Process Semantics of Algebraic Datatypes, Colloquia Mathematica Societatis János Bolyai 26, Mathematical Logic in Computer Science, Salgótarján, Hungary, 1978.
[25] Blackford, L. S., Petitet, A., Pozo, R., Remington, K., Whaley, R. C., Demmel, J., Dongarra, J., Duff, I., Hammarling, S., Henry, G.: An updated set of basic linear algebra subprograms (BLAS), ACM Transactions on Mathematical Software, 28(2), 2002, 135-151.
[26] Blom, S., Fokkink, W., Groote, J., Van Langevelde, I., Lisser, B., van de Pol, J.: μCRL: A toolset for analysing algebraic specifications, Proceedings of the 13th International Conference on Computer Aided Verification, number 2102 in LNCS, Springer Verlag, 2001.
[27] van den Brand, M. G. J., van Deursen, A., Dinesh, T. B., Kamperman, J. F. T., E., V., Eds.: ASF+SDF'95, number P9504 in Technical Reports of the Programming Research Group, University of Amsterdam, 1995.
[28] Bray, T., Paoli, J., Sperberg-McQueen, C., Maler, E., Yergeau, F., Cowan, J.: Extensible markup language (XML) 1.1, W3C Recommendation,W3C, 2006.
[29] Brinch Hansen, P.: Distributed processes: a concurrent programming concept, Commun. ACM, 21(11), 1978, 934-941.
[30] Brunekreef, J. J.: A Formal Specification of the Amoeba Transaction Protocol, Technical Report P9108, Programming Research Group, University of Amsterdam, Amsterdam, 1991.
[31] Brunekreef, J. J.: A Formal Specification of three Sliding Window Protocols (revised version), Technical Report P9102b, Programming Research Group, University of Amsterdam, Amsterdam, 1991.
[32] Brunekreef, J. J.: A Formal Specification of Two Simple Protocols for Local Area Networks, Technical Report P9109, Programming Research Group, University of Amsterdam, Amsterdam, 1991.
[33] Brunekreef, J. J., Ponse, A.: An algebraic specification of a model factory, Part IV, Technical Report P9316, Programming Research Group, University of Amsterdam, Amsterdam, 1993.
[34] Diertens, B.: New Features in PSF I - Interrupts, Disrupts and Priorities, Technical Report P9417, Programming Research Group, University of Amsterdam, Amsterdam, 1994.
[35] Diertens, B.: Simulation and Animation of Process Algebra Specifications, Technical Report P9713, Programming Research Group, University of Amsterdam, Amsterdam, 1997.
[36] Diertens, B.: Generation of Animations for Simulation of Process Algebra Specifications, Technical Report P2003, Programming Research Group, University of Amsterdam, Amsterdam, 2000.
[37] Diertens, B.: Software (Re-)Engineering with PSF, Technical Report P0505, Programming Research Group, University of Amsterdam, Amsterdam, 2005.
[38] Diertens, B.: Software (Re-)Engineering with PSF II: from architecture to implementation, Technical Report PRG0609, Programming Research Group, University of Amsterdam, Amsterdam, 2006.
[39] Diertens, B.: Software (Re-)Engineering with PSF III: an IDE for PSF, Technical Report PRG0708, Programming Research Group, University of Amsterdam, Amsterdam, 2007.
[40] Diertens, B.: A Process Algebra Software Engineering Environment, Technical Report PRG0808, Programming Research Group, University of Amsterdam, Amsterdam, 2008.
[41] Diertens, B.: Software Engineering with Process Algebra, PhD dissertation, University of Amsterdam, Programming Research Group, October 2009.
[42] Diertens, B.: Software Engineering with Process Algebra: Modelling Client / Server Architectures, Technical Report PRG0908, Programming Research Group, University of Amsterdam, Amsterdam, 2009.
[43] Diertens, B., Ponse, A.: New Features in PSF II - Iteration and Nesting, Technical Report P9425, Programming Research Group, University of Amsterdam, Amsterdam, 1994.
[44] DIS, ISO: 8824: Specification of Abstract Syntax Notation One (ASN. I), Basic Encoding Rules, 1987.
[45] van der Duyn Schouten, F. A., Klusener, A. S., van Vlijmen S F M, Vos de Wael, S. L. E.: A decision support system for the maintenance of lights of traffic regulation systems, Technical report, Utrecht University, Utrecht, the Netherlands, 1996, In Dutch.
[46] Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specifications ETACS Monographs on Theoretical Computer Science, Vol 6, 1985.
[47] Feijs, L. M. G., Jonkers, H. B. M.: Formal specification and design, vol. 35 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge, 1992.
[48] Fuggetta, A.: A classification of case technology, Computer, 26(12), 1993, 25-38.
[49] van Glabbeek, R. J., Vaandrager, F. W.: Modular specifications in process algebra, Theoretical Computer Science, 113(2), 1993, 293-348.
[50] van Glabbeek, R. J., Weijland, W. P.: Branching time and abstraction in bisimulation semantics (extended abstract), in: Information Processing 'Eighty-Nine: Proceedings of the IFIP 11th World Computer Congress, San Francisco, CA, 28 Aug. to 1 Sept., 1989 (G. X. Ritter, Ed.), Elsevier Science Inc., New York, NY, USA, 1989, 613-618.
[51] van Glabbeek, R. J., Weijland, W. P.: Branching time and abstraction in bisimulation semantics, Journal of the ACM (JACM), 43(3), 1996, 555-600.
[52] Groote, J., Mathijssen, A., van Weerdenburg, M., Usenko, Y.: From [mu] CRL to mCRL2:: Motivation and Outline, Electronic Notes in Theoretical Computer Science, 162, 2006, 191-196.
[53] Groote, J., Ponse, A.: The syntax and semantics of μCRL, Algebra of Communicating Processes '94 (A. Ponse, C. Verhoef, S. v. Vlijmen, Eds.), Workshops in Computing Series, Springer-Verlag, 1995.
[54] Groote, J. F., Mathijssen, A., Reniers, M., Usenko, Y., van Weerdenburg, M.: The Formal Specification Language mCRL2, Methods for Modelling Software Systems (MMOSS) (E. Brinksma, D. Harel, A. Mader, P. Stevens, R.Wieringa, Eds.), number 06351 in Dagstuhl Seminar Proceedings, Internationales Begegnungsund Forschungszentrumfür Informatik (IBFI), Schloss Dagstuhl, Germany, Dagstuhl, Germany, 2007, ISSN 1862-4405.
[55] Heering, J., Klint, P.: Prehistory of the ASF+SDF system (1980 - 1984), in: van den Brand et al. [27].
[56] Hennessy,M.,Milner, R.: Algebraic laws for nondeterminismand concurrency, Journal of the ACM(JACM), 32(1), 1985, 137-161.
[57] Hillebrand, J. A., Ponse, A.: An algebraic specification of a model factory, Part II, Technical Report P9214, Programming Research Group, University of Amsterdam, Amsterdam, 1992.
[58] Hoare, C. A. R.: Communicating sequential processes, Communications of the ACM, 21(8), 1978, 666-677.
[59] ISO: 8807: Information processing systems-open systems interconnection-LOTOS-a formal description technique based on the temporal ordering of observational behaviour, Standard, International Standards Organization, Geneva, Switzerland, 15, 1987.
[60] ITU, X.: 680-X. 693, Information Technology-Abstract Syntax Notation One (ASN. 1) & ASN, 1, 2002.
[61] Jacobsson, H., Mauw, S.: A token ring network in PSFd, Technical Report P8914, Programming Research Group, University of Amsterdam, Amsterdam, 1989.
[62] Jensen, K.: Coloured Petri nets, Petri nets: central models and their properties, 1992, 248-299.
[63] Kleene, S.: Representation of Events by Nerve Nets In CE Shannon and J. McCarthy, editors, Automata Studies, 1956.
[64] Klint, P.: The evolution of implementation techniques in the ASF+SDF Meta-Environment, in: van den Brand et al. [27].
[65] Mauw, S.: An algebraic specification of process algebra, including two examples, Technical Report FV 87-06, Computer Science Department, University of Amsterdam, Amsterdam, 1987.
[66] Mauw, S.: PSF - A Process Specification Formalism, PhD dissertation, University of Amsterdam, Programming Research Group, December 1991.
[67] Mauw, S., Mulder, J. C.: A PSF Library of Data Types, in: van den Brand et al. [27], 53-64.
[68] Mauw, S., Veltink, G. J.: A process specification formalism, Technical Report P8814, Programming Research Group, University of Amsterdam, Amsterdam, 1988.
[69] Mauw, S., Veltink, G. J.: An Introduction to PSFd, TAPSOFT'89: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Current Issues in Programming Languages (CCIPL) (J. D´ıaz, F. Orejas, Eds.), number 352 in LNCS, Springer Verlag, 1989.
[70] Mauw, S., Veltink, G. J.: A Tool Interface Language for PSF, Technical Report P8912, Programming Research Group, University of Amsterdam, Amsterdam, 1989.
[71] Mauw, S., Veltink, G. J.: A process specification formalism, Fundam. Inf., 13(2), 1990, 85-139, ISSN 0169-2968.
[72] Mauw, S., Veltink, G. J.: A Proof Assistant for PSF, Computer Aided Verification, Proceedings of the 3rd International Workshop, CAV '91 (K. G. Larsen, A. Skou, Eds.), number 575 in LNCS, Springer Verlag, 1991.
[73] Mauw, S., Veltink, G. J., Eds.: Algebraic specification of communication protocols, vol. 36 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge, 1993.
[74] Milner, R.: A Calculus of Communicating Systems, vol. 92 of LNCS, 1980.
[75] Mulder, J. C.: The inevitable coffee machine, Technical Report P8915, Programming Research Group, University of Amsterdam, Amsterdam, 1989.
[76] Mulder, J. C.: Case Studies in Process Specification and Verification, PhD dissertation, University of Amsterdam, Programming Research Group, December 1990.
[77] Mullender, S. J.: Principles of Distributed Operating System Design, PhD dissertation, Universiteit Twente, Enschede, The Netherlands, October 1985.
[78] Munshi, A.: The OpenCL specification version 1.0, Khronos OpenCL Working Group, 2009.
[79] Plotkin, G. D.: A Structural Approach to Operational Semantics, Technical Report DAIMI FN-19, Aarhus University, Aarhus, Denmark, 1981.
[80] Polak, E. E.: An efficient implementation of branching bisimulation and distinguishing formulae, Technical Report P9216, Programming Research Group, University of Amsterdam, Amsterdam, 1992.
[81] Ponse, A., Verschuren, J. A.: An algebraic specification of a model factory, Part III, Technical Report P9303, Programming Research Group, University of Amsterdam, Amsterdam, 1993.
[82] Srinivasan, S.,Mycroft, A.: Kilim: Isolation-typed actors for Java, European Conference on Object Oriented Programming ECOOP 2008, Springer, 2008.
[83] Tanenbaum, A. S.: Computer Networks, Prentice-Hall, 1989.
[84] Veltink, G. J.: A Process Specification Formalism, Master's thesis, Programming Research Group, University of Amsterdam, Amsterdam, May 1988.
[85] Veltink, G. J.: From PSF to TIL, Technical Report P9009, Programming Research Group, University of Amsterdam, Amsterdam, 1990.
[86] Veltink, G. J.: XP, an Experiment in Modular Specification, Proceedings of the IFIP TC6/WG6. 1 Fourth International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols: Formal Description Techniques, IV, North-Holland Publishing Co., 1991.
[87] Veltink, G. J.: The PSF toolkit, Computer Networks and ISDN Systems, 25(7), 1993, 875-898.
[88] Veltink, G. J.: Tools for PSF, PhD dissertation, University of Amsterdam, Programming Research Group, June 1995.
[89] Veltink, G. J.: PSF & The PSF Toolkit, STAK '96, Softwaretechnik in Automation und Kommunikation - Rechnergestützte Teamarbeit (J. Swoboda, Ed.), number 137 in ITG Fachbericht, VDE Verlag, Berlin, Offenbach, Germany, 1996.
[90] Veltink, G. J., Walters, H. R.: Case Study I: Teaching Algebraic Specifications, in: Tools for PSF, University of Amsterdam, Programming Research Group, June 1995, 139-163.
[91] Verhoef, C.: On the Register Operator, Technical Report P9003, Programming Research Group, University of Amsterdam, Amsterdam, 1990.
[92] van Vlijmen, S. F. M., van Waveren, A.: An algebraic specification of a model factory, Technical Report P9209, Programming Research Group, University of Amsterdam, Amsterdam, 1992.
[93] van Wamel, J. J.: A Library for PSF, Technical Report P9301, Programming Research Group, University of Amsterdam, Amsterdam, 1993.

Typ dokumentu

Bibliografia

Identyfikator YADDA

bwmeta1.element.baztech-article-BUS8-0010-0054