Developing parallel object-oriented programs in the framework of VDM
Tóm tắt
After surveying the rely-guarantee and some related approaches to extending VDM to develop parallel programs, two main problems are found. One problem is that all explorations of parallelism are done in the stage of operation decomposition or afterwards so that the degree of parallelism is restricted. Another problem is that the atomicity is fixed at one level and the development complexity can not be controlled effectively because there is no natural means to let the level of granularity be under flexible control of the designer. In order to solve these two problems, we introduce a new concept — data decomposition which is based on the ideas of model split, modularisation and operation decomposition, and combine it with VDM to form a more general formal development method DD-VDM, in which some kind of operation decompositions, i.e., operation split can be done before some data reifications. Then a nested parallel object-oriented structure is proposed. Combining these ideas into the unified framework, this paper presents a hierarchical object-oriented design methodology in which two kinds of parallelism, that is, internal parallelism and service parallelism, can be exploited gradually and a kind of virtual atomicity is provided.
Tài liệu tham khảo
Jones, C.B. (1981), “Development Methods for Computer Programs Including a Notion of Interference,” PhD Thesis, Oxford University.
Jones, C.B. (1983), “Specification and Design of (Parallel) Programs,” InProceedings of IFIP '83, North-Holland, pp. 321–332.
Jones, C.B. (1990),Systematic Software Development Using VDM, Second Edition, Prentice-Hall.
Jones, C.B. and R.C.F. Shaw, Eds. (1990),Case Studies in Systematic Software Development, Prentice-Hall.
Jones, C.B. (1991), “Interference Resumed,” Technical Report UMCS-91-5-1, Department of Computer Science, University of Manchester.
Jones, C.B. (1993a), “Constraining Interference in an Object-Oriented Design Method,” InTAPSOFT '93: Theory and Practice of Software Development, Lecture Notes in Computer Science, Vol. 668, M.-C. Gaudel and J.-P. Jouannaud, Eds., Springer-Verlag, pp. 136–150.
Jones, C.B. (1993b), “A Pi-Calculus Semantics for an Object-Based Design Notation,” InCONCUR'93: 4th International Conference on Concurrency Theory, Lecture Notes in Computer Science, Vol. 715, E. Best, Ed., Springer-Verlag, pp. 158–172.
Jones, C.B. (1993c), “Reasoning About Interference in an Object-Based Design Method,” InFME'93: Industrial-Strength Formal Methods, Lecture Notes in Computer Science, Vol. 670, Springer-Verlag. pp. 1–18.
Jones, C.B. (1993d), “Process-Algebraic Foundations for an Object-Based Design Notation,” Technical Report, UMCS-93-10-1, Department of Computer Science, University of Manchester.
Milner, R. (1989),Communication and Concurrency, Prentice Hall.
Milner, R. (1991), “The Polyadic π-Calculus: A Tutorial,” Research Report LFCS-91-180, Laboratory for Foundations of Computer Science, Computer Science Department, Edinburgh University.
Milner, R., J. Parrow and D. Walker (1992), “A Calculus of Mobile Processes,”Information and Computation 100, 41–77.
Stolen, K. (1990), “Development of Parallel Programs on Shared Data-Structures,” PhD Thesis, Manchester University.
Zwiers, J. (1988),Compositionality, Concurrency and Partial Correctness: Proof Theories for Networks of Processes, and Their Connections, Lecture Notes in Computer Science, Vol. 321, Springer-Verlag.