Abstract
A new notion of refinement and several other new operators are proposed that allow for a compositional algebraic characterization of action systems and serializability in distributed database systems. A simple design language is introduced and is provided with a semantics essentially based on partial order models.
Various algebraic transformation rules are introduced. They are applied in the design process of a simple system, starting from a specification of functional behaviour via the intermediate step in the form of a “true concurrency” based initial design to an actual implementation on a two processor architecture.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R.J.R. Back, A calculus of refinements for program derivations, Acta Informatica 25, 1988.
H. Barringer, R. Kuiper and A. Pnueli, Now you may compose temporal logic specifications, Proc. of the 16th ACM Symposium on Theory of Computing, Washington, 1984, pp. 51–63.
P.A. Bernstein, V. Hadzilacos and N. Goodman, Concurrency Control and Recovery in Database Systems, Addison-Wesley, 1987.
K.M. Chandy and J. Misra, Parallel Program Design: A Foundation, Addison-Wesley, 1988.
P. Degano, R. De Nicola and U. Montanari, Partial orderings descriptions and observations of nondeterministic concurrent processes, Proc. of the REX workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, 1988, LNCS 354, pp. 438–466.
T. Elrad and N. Francez, Decomposition of distributed programs into communication closed layers, Science of Computer Programming 2, 1982.
H. Gaifman, Modeling Concurrency by Partial Orders and Nonlinear Transition Systems, Proc. of the REX workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, 1988, LNCS 354, pp. 467–488.
R.T. Gallager, P.A. Humblet and P.M. Spira, A distributed algorithm for minimum-weight spanning trees, ACM TOPLAS 5-1, 1983.
R. J. van Glabbeek and U. Goltz, Equivalence Notions for Concurrent Systems and Refinement of Actions, Arbeitspapiere der GMD, Number 366, GMD, 1989
C.A.R. Hoare and He Jifeng, The weakest prespecification, IPL, 1987.
J. Hooman, Specification and Compositional Verification of Real-Time Systems, Ph.D. Thesis, Eindhoven University of Technology, 1991.
C.B. Jones, Systematic software development using VDM, Prentice-Hall, 1986.
W. Janssen, M. Poel and J. Zwiers, Consistent alternatives of parallelism with conflicts, Memorandum INF-91-15, University of Twente.
S. Katz and D. Peled, Interleaving set temporal logic, Proc. of the 6th ACM Symposium on Principles of Distributed Computing, Vancouver, 1987, pp. 178–190.
L. Lamport, The Hoare Logic of concurrent programs, Acta Informatica 14, 1980.
Z. Manna and A. Pnueli, Verification of concurrent programs: the temporal framework, In R.S. Boyer and J.S. Moore (eds), The Correctness Problem in Computer Science, Academic Press, 1981.
M. Nielsen, U. Engberg and K.S. Larsen, Fully abstract models for a process language with refinement, Proc. of the REX workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, 1988, LNCS 354, pp. 523–548.
S. Owicki and D. Gries, An axiomatic proof technique for parallel programs, Acta Informatica 6, 1976.
L. Pomello, Refinement of Concurrent Systems Based on Local State Transformations, Proc. REX workshop on Stepwise Refinement of Distributed Systems, 1989 LNCS 430, pp. 641–668.
V. Pratt, Modelling Concurrency with Partial orders, International Journal of Parallel Programming 15, 1986, pp. 33–71.
F.A. Stomp and W.P. de Roever, Designing distributed algorithms by means of formal sequentially phased reasoning, Proc. of the 3rd International Workshop on Distributed Algorithms, Nice, LNCS 392, Eds. J.-C. Bermond and M. Raynal, 1989, pp. 242–253.
G. Winskel, An introduction to event structures, Proc. of the REX workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, 1988, LNCS 354, pp. 364–397.
J. Zwiers and W.P. de Roever, Predicates are Predicate Transformers: a unified theory for concurrency, Proc. of the conference on Principles of Distributed Computing, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Janssen, W., Poel, M., Zwiers, J. (1991). Action systems and action refinement in the development of parallel systems. In: Baeten, J.C.M., Groote, J.F. (eds) CONCUR '91. CONCUR 1991. Lecture Notes in Computer Science, vol 527. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54430-5_96
Download citation
DOI: https://doi.org/10.1007/3-540-54430-5_96
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54430-2
Online ISBN: 978-3-540-38357-4
eBook Packages: Springer Book Archive