This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Integrated Environments for Formally Well-Founded Design and Simulation of Concurrent Systems
June 1988 (vol. 14 no. 6)
pp. 787-802

An ongoing project concerned with the development of environments that support the specification and design of concurrent systems is reported. The project has two key aspects: an existing and working system, Clara, that supports Milner's CCS as a specification and design language; and the development of general techniques for computer-aided generation of Clara-like environments for other concurrent languages. The Clara environment is emphasized. It has two main components: support for the usage of formal techniques in the design process, and a rich and highly interactive simulation facility. A further distinguishing feature is the environment's graphical user interface which is based on a pictorial version of CCS. The semantics of CCS is defined nonprocedurally in two phases: an operational semantics given as a set of inference rules, and an algebraic semantics represented by a set of equational rules.

[1] R. Bahkle and G. Snelting, "The PSG system: From formal language definitions to interactive programming environment,"ACM Trans. Program. Lang. Syst., vol. 8, pp. 547-576, Oct. 1986.
[2] J. Barnes and J. Fischer, Eds.,Proc. IEEE Int. Conf. Ada Applications and Environments, Paris, France, May 1985.
[3] D.R. Barstow, H.E. Shrobe, and E. Sandewall, Eds.,Interactive Programming EnvironmentsNew York: McGraw-Hill, 1984.
[4] P. M. Behr, W. K. Giloi, and H. Muhlenbein, "SUPRENUM: The German supercomputer architecture--Rationale and concepts," inProc. 1986 Int. Conf. Parallel Processing.
[5] S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe, "A theory of communicating sequential processes,"J. ACM, vol. 31, no. 3, pp. 560-599, July 1984.
[6] R. Buhr, "CAEDE: An iconic Prolog-based design environment approach for Ada," Carleton Univ., Ottawa, Ont., Canada, Jan. 1985.
[7] J. M. Butler and A. Y. Oruc, "Euclid: An architectural multiprocessor simulator," inProc. 6th Int. Conf. Distributed Computing Systems, Cambridge, MA, May 1986, pp. 280-287.
[8] CCITT, "Functional specification and description language (SDL)," Document AP VII, No. 20-E, Geneva, Switzerland, Document AP VII, No. 20-E, June 1980.
[9] L. Cardelli, "An algebraic approach to hardware description and verification," Ph.D. dissertation, Univ. Edinburgh, Dep. Comput. Sci., Rep. CST- 16-82, Apr. 1982.
[10] L. Cardelli and R. Pike, "Squeak: A language for communicating with mice,"Proc SIGGRAPH 85, ACM SIGGRAPH 19, pp. 199-204, July 1985.
[11] L. Clarke, J. C. Wileden, R. N. Taylor, M. Young, and L. J. Osterweil, "ARCADIA: A software development environment research project," inProc. IEEE Second Int. Conf. Ada Applications and Environments, Miami Beach, FL, Apr. 1986.
[12] P. Degano and E. Sandewall, Eds.,Integrated Interactive Computing Systems: Proc. European Conf. Integrated Interactive Computing Systems (ECICS 82). Amsterdam, The Netherlands: North-Holland, 1983.
[13] N. Delisle and M. Schwartz, "A programming environment for CSP," inProc. ACM SIGSOFT/SIGPLAN Symp. Practical Software Development Environments, Palo Alto, CA, Dec. 1986.
[14] T. W. Doeppner, Jr. and A. Giacalone, "A formal description of the UNIX operating system," inProc. 2nd ACM SIGACT/SIGOPS Symp. Principles of Distributed Computing, Montreal, P.Q., Canada, Aug. 1983.
[15] "Multimax technical summary," Encore Computer Corp., May 1985.
[16] G. Estrin, R. S. Fenchel, R. R. Razouk, and M. K. Vernon, "SARA (System ARchitects Apprentice): Modeling, analysis, and simulation support for design of concurrent systems,"IEEE Trans. Software Eng., vol. SE-12, no. 2, pp. 293-311, Feb. 1986.
[17] A. Giacalone and I. D. Kovacs, "IDCCS: An ideographic syntax for CS," Dep. Comput. Sci., Brown Univ., Tech. Rep. CS-83-05, Feb. 1983.
[18] A. Giacalone, M. C. Rinard, and T. W. Doeppner, Jr., "IDEOSY: An interactive and ideographic program description system," inProc. ACM SIGSOFT/SIGPLAN Symp. Practical Software Development Environments, Pittsburgh, PA, Apr. 1984, pp. 15-20.
[19] P. B. Henderson, Ed.,Proc. ACM SIGSOFT/SIGPLAN Symp. Practical Software Development Environments, Pittsburgh, PA, Apr. 1984.
[20] P. B. Henderson, Ed.,Proc. ACM SIGSOFT/SIGPLAN Symp. Practical Software Development Environments, Palo Alto, CA, Dec. 1986.
[21] M. C. B. Hennessy, W. Li, and G. Plotkin, "A first attempt at translating CSP into CCS," inProc. 2nd IEEE Int. Conf. Distributed Computing, 1981.
[22] M. C. B. Hennessy and W. Li, "Translating a subset of Ada into CS," inProc. IFIP Conf. Formal Description of Programming Concepts-II, 1983, pp. 227-247.
[23] M. C. B. Hennessy, "Acceptance trees,"J. ACM, vol. 34, no. 4, pp. 896-928, Oct. 1985.
[24] D. Hillis,The Connection Machine. Cambridge, MA: M.I.T. Press, 1985.
[25] C. A. R. Hoare, "A model for communicating sequential processes," Programming Research Group, Oxford Univ., Comput. Lab., Tech. Rep. PRG-22, 1981.
[26] C.A.R. Hoare,Communicating Sequential Processes, Prentice Hall, Englewood, N.J., 1985.
[27] C. A. R. Hoare, Ed.,Occam Programming Manual, INMOS Ltd. Englewood Cliffs, NJ: Prentice-Hall, 1984.
[28] P. C. Kanellakis and S. A. Smolka, "CCS expressions, finite state processes, and three problems of equivalences" inProc. 2nd ACM Symp. Principles of Distributed Computing, Montreal, P.Q., Canada, Aug. 1983, pp. 228-240.
[29] C. J. Koomen, "A structure theory for communication network control," Ph.D. dissertation, Delft Univ. Technology, 1982.
[30] O. Kramer and H. Muhlenbein, "Mapping strategies in message based multiprocessor systems," inProc. Conf. Parallel Architectures and Languages Europe (PARLE). Eindhoven, The Netherlands: Springer-Verlag, June 15-19, 1987.
[31] K. G. Larsen, "Context-dependent bisimulation between processes," Ph.D. dissertation, Dep. Comput. Sci., Univ. Edinburgh, Tech. Rep. CST-37-86, May 1986.
[32] R. Milner,A Calculus of Communicating Systems (Lecture Notes in Computer Science 92). New York: Springer-Verlag, 1980.
[33] R. Milner, "Calculi for Synchrony and Asynchrony," Theoret. Comput. Sci. 25, (1983), 267-310.
[34] R. Milner, "The standard ML core language," Dep. Comput. Sci., Univ. Edinburgh, Internal Rep. CSR-168-84, 1984.
[35] M. Moriconi and D. Hare, "The PegaSys system: Pictures as formal documentation of large programs,"ACM Trans. Prog. Lang. Syst., vol. 8, no. 4, pp. 524-546, Oct. 1986.
[36] H. Muhlenbein, O. Kramer, F. Limburger, M. Mevenkamp, and S. Streitz, "Design and rationale for MUPPET: A programming environment for message based multiprocessors," Gesellschaft fur Mathematik und Datenverarbeitung mbH, Sankt Augustin, West Germany, Tech. Rep., Feb. 1987.
[37] "NCUBE/ten: An overview," NCUBE Corp., 1986.
[38] R. D. Nicola and M. C. B. Hennessy, "Testing equivalences for processes,"Theoret. Comput. Sci., vol. 34, no. 1, pp. 83-133, 1984.
[39] J. Parrow, "Fairness properties in process algebra with applications in communication protocol verification," Ph.D. dissertation, Dep. Comput. Syst., Uppsala Univ., Sweden, 1985.
[40] C. A. Petri, "Kommunication mit automaten," Bonn Institut fur Instrumentelle Mathematik, Schriften des IIM No. 2, 1962.
[41] G. Plotkin, "A structural approach to operational semantics," Dep. Comput. Sci., Aarhus Univ., Internal Rep. DAIMI FN-19, Sept. 1981.
[42] G. Plotkin, "An operational semantics for CSP," Dep. Comput. Sci., Univ. Edinburgh, Internal Rep. CSR-114-82, May 1982.
[43] K. V. S. Prasad, "Specification and proof of a simple fault tolerant system in CCS," Dep. Comput. Sci., Univ. Edinburgh, Int. Rep. CSR-178-84, 1984.
[44] S.P. Reiss, "Pecan: Program Development Systems That Support Multiple Views,"Proc. Seventh Int'l Conf. Software Eng., CS Press, Los Alamitos, Calif., 1984, pp. 324-333.
[45] S. P. Reiss, "Visual languages and the garden system," Dep. Comput. Sci., Brown Univ., Providence, RI, Tech. Rep. CS-86-16, 1986.
[46] T. Reps and T. Teitelbaum, "The synthesizer generator reference manual," Dep. Comput. Sci., Cornell Univ., Aug. 1985.
[47] M. W. Sheilds and M. J. Wray, "A CCS specification of the OSI network service," Dep. Comput. Sci., Univ. Edinburgh, Tech. Rep. CSR-136-83, Aug. 1983.
[48] S. A. Smolka and R. E. Strom, "A CCS semantics for NIL," inFormal Description of Programming Concepts-III, M. Wirsing, Ed. Amsterdam, The Netherlands: North-Holland, 1987.
[49] R. E. Strom, S. Yemini, and P. Wegner, "Viewing Ada from a process model perspective," inProc. 1985 Ada Tec Conf., Paris, France, 1985.
[50] Reference Manual for the Ada Programming Language, U.S. Dep. Defense, Rep. MIL-STD 1815A, Feb. 1983.
[51] P. Wegner, "The Vienna definition language,"ACM Comput. Surveys, vol. 4, pp. 5-63, 1972.

Index Terms:
programming environments; parallel programming; specification language; concurrent systems; Clara; CCS; concurrent languages; formal techniques; interactive simulation; graphical user interface; operational semantics; inference rules; algebraic semantics; equational rules; computer graphics; parallel programming; programming environments; programming theory; simulation languages; specification languages; user interfaces
Citation:
A. Giacalone, S.A. Smolka, "Integrated Environments for Formally Well-Founded Design and Simulation of Concurrent Systems," IEEE Transactions on Software Engineering, vol. 14, no. 6, pp. 787-802, June 1988, doi:10.1109/32.6158
Usage of this product signifies your acceptance of the Terms of Use.