From CML to a Model-Based Concurrent Specification Language

Abstract

In this paper, we address the problem of specification and design of concurrent systems More accurately, we present the definition of a new specification language that is formal, wide-spectrum, model-based, concurrent, polymorphic, and strongly implicitly typed The lan guage is built upon a concurrent, functional, and imperative programming language Concurrent ML Specification aspects are supported thanks to the addition of some specification constructs and also by allowing axioms to appear in ML structures and signatures The resulting specification language is thus highly expressive though it embodies a restricted number of concepts We present here the motivations underlying the definition of such a language as well as the design choices Furthermore, we introduce the specification and development methodology and illustrate it on various examples We will see that many specification styles are allowed algebraic, applicative, state-based, concurrent applicative, and con current imperative

Keywords

formal methods concurrent and distributed systems specification design concurrent ML

Get full access to this article

View all access options for this article.

References

Battiston, E. , F. De Cindio , G. Mauri and L. Rapanotti. 1991. "Morphisms and minimal Models for OBJSA Net," in International Conference on Application and Theory of Petri Nets. Gjern.

Berghammer and Zierer. 1986. "Relational Algebraic Semantics of Deterministic and Nondeterministic Programs," Theoretical Computer Science, p. 43.

Bidoit, M. 1987. "The Stratified Loose Approach: A Generalization of Initial and Loose Semantics," in Proceedings of the 5th Workshop on Specification of Abstract Data Types. Springer Verlag.

Bidoit, M. 1989. "PLUSS, un Langage pour le Développement de Spécifications Algébriques Modulaires," Thèse de Doctorat d'Etat, Université Paris Sud, Orsay, July.

Bjorner, D. and C.B. Jones. 1982. Formal Specification and Software Development . Prentice-Hall.

Bolignano D. and M. Debbabi. 1993. "A Coherent Type Inference System for a Concurrent, Functional and Imperative Programming Language," in Proceedings of the AMAST'93 Conference. Springer Verlag, June.

Bolignano, D. and M. Debbabi. 1993. "A Semantic Theory for ML Higher Order Concurrency Primitives," in Proceedings of the NAPAW'93 Workshop, Cornell University, August.

Bolignano, D. and M. Debbabi. 1994. "A Semantic Theory for CML", in Proceedings of the TACS'94 Conference, Springer Verlay, April.

Bolignano, D. and M. Debbabi. 1992. "Higher Order Communicating Processes with Value-Passing, Assignment and Return of Results," in Proceedings of the ISAAC'92 Conference, Lecture Notes in Computer Science 650. Springer Verlag, December.

10.

Bolognesi, T. and E. Brinksma. 1989. The Formal Description Technique LOTOS , North Holland.

11.

Debbabi. M. 1994. "Intégration des Paradigmes de Programmation Parallèle, foonctionnelle et impérative: fondements sémantiques;" Thèse de Doctorat, Université Paris Sud, Centre d'Orsay, July.

12.

Ehrig, H. and B) Mahr. 1985. "Fundamentals of Algebraic Specification 1. Equations and Initial Semantics," EATCS Monographs on Theoretical Computer Science, Springer, Vol. 6.

13.

Futatsugi, K. , J.A. Goguen , J.- P. Jouannaud and J. Meseguer. 1985. "Principles of OBJ2 . in Proc. 12th ACM Symp. on Principles of Programming Languages, pp. 52-66.

14.

Gaudel, M.-C. 1983. Proposition pour un Langage d-Utilisation de Specifications Structurées: PLUSS. Technical Report, Laboratoire de la C.G. E.

15.

Goguen, J.A. 1978. "Some Design Principles and Theory for OBJ-0, A Language for Expressing and Executing Algebraic Specifications of Programs," in Proc. Intl. Conf. on Mathematical Studies of Information Processing, Springer LNCS , pp. 429-475.

16.

Hennessy, M. 1988. Algebraic Theory of Process . MIT Press .

17.

Hoare, C.A.R. 1978. "Communicating Sequential Processes," Communications of the ACM, 21(8):666-677.

18.

Hoare, C. A.R. Hoare. 1985. Communicating Sequential Processes. Prentice-Hall.

19.

Kahrs, S. , D.T. Sannella and A. Tarlecki. 1995. "The Definition of Extented ML," Technical Report LFCS Report Series ECS-LFCS-95-322, Laboratory for Foundations of Computer Science University of Edinburgh.

20.

Leveson, N.G. 1990. "Guest Editor's Introduction ," IEEE Transactions on Software Engineering, 16(9):929-931.

21.

Milner. A.J.R.G. 1989. Communication and Concurrency . Prentice-Hall.

22.

Milner, A.J.R.G. 1991. "A Calculus of Communicating Systems," in Lecture Notes in Computer Science 92. Springer-Verlag, pp. 281-305.

23.

Milner, A.J.R.G. and M. Tofte. 1991. Commentary on Standard ML. MIT Press.

24.

Milner, A.J.R.G. , M. Tofte and R. Harper. 1990. The Definition of Standard ML. MIT Press.

25.

Petri, C.A. 1962. Kommunikation mit Automaten. Ph.D. thesis, West Germany: Univ. Bonn.

26.

1992. RAISE Language Group. The RAISE Specification Language. Prentice-Hall .

27.

Reisig, W. 1985. "An Introduction," Monographs on Theoretical Computer Science. Volume 4, Springer-Verlag.

28.

Reppy, J.H. 1988. "Synchronous Operations as First-Class Values," SIG-PLAN Notices, 23(7):250-259, Proceedings of the ACM SIGPLAN '88 Conference on Programming Language Design and Implementation.

29.

Reppy. J. H. 1989. "First-Class Synchronous Operations in Standard ML," Technical Report TR89-1068, Dept. of Computer Science, Cornell University.

30.

Reppy, J.H. 1990. "Concurrent Programming with Events—the Concurrent ML Manual," Technical Report Department of Computer Science, Cornell University, November.

31.

Reppy, J.H. 1991. "CML: A Higher-Order Concurrent Language," in Proceedings of the ACM SIGPLAN '91 PLDI, SigPLAN Notices, 26(6).

32.

Reppy, J.H. 1991. "An Operational Semantics of First-Class Synchronous Operations ," Technical Report TR 91-1232, Department of Computer Science, Cornell University, August.

33.

Sannella, D. 1990. "Formal Program Development in Extended ML for the Working Programmer," in Proc. flrd BCS/FACS Refinement Workshop. Springer Verlag .

34.

Sannella, D. and A. Tarlecki. 1985. "Program Specification and Development in Standard ML," in Proc. 12th ACM Symposium on Principles of Programming Languages.

35.

Sannella, D.T. and A. Tarlecki. 1990. "Extended ML: Past, Present and Future," in roc. 7th Workshop on Specification of Abstract Data Types, Wusterhausen, pp. 297-322, Springer LNCS, p. 534.

36.

Spivey. J.M. 1988. Understanding Z: A Specification Language and Its Formal Semantics. Cambridge University Press.

37.

Wing, J.M. 1990. 'A Specifier's Introduction to Formal Methods," IEEE Computer, pp. 8-24, September.