Abstract
In B, the expression of dynamic constraints is notoriously missing. In this paper, we make various proposals for introducing them. They all express, in different complementary ways, how a system is allowed to evolve. Such descriptions are independent of the proposed evolutions of the system, which are defined, as usual, by means of a number of operations. Some proof obligations are thus proposed in order to reconcile the two points of view. We have been very careful to ensure that these proposals are compatible with refinement. They are illustrated by several little examples, and a larger one. In a series of small appendices, we also give some theoretical foundations to our approach. In writing this paper, we have been heavily influenced by the pioneering works of Z. Manna and A. Pnueli [11], L. Lamport [10], R. Back [5] and M. Butler [6].
Supported by STERIA, SNCF, RATP and INRETS
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
J.-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press (1996)
J.-R. Abrial. Extending B Without Changing it (for Developing Distributed Systems). First B Conference (H. Habrias editor). Nantes (1996)
J.-R. Abrial and L. Mussat. Specification and Design of a Transmission Protocol by Successive Refinements Using B. in Mathematical Methods in Program Development Edited by M.Broy and B. Schieder. Springer-Verlag (1997)
K.R. Apt and E.-R. Olderog. Proof Rules and Transformations Dealing with Fairness. Science of Computer Programming (1983)
R.J.R. Back and R. Kurki-Suonio. Decentralization of Process Nets with Centralized Control. 2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing (1983)
M. J. Butler. Stepwise Refinement of Communicating Systems. Science of Computer Programming (1996)
K.M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley (1988)
I.J. Hayes (editor). Specification Case Study. Prentice-Hall (1987)
C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall (1985)
L. Lamport. The Temporal Logic of Actions. SRC Report 57 (1991)
Z. Manna and A. Pnueli. Adequate Proof Principles for Invariance and Liveness Properties of Concurrent Systems. Science of Computer Programming (1984)
A. Udaya Shankar An Introduction to Assertional Reasoning for Concurrent Systems. ACM Computing Survey (1993)
Steria. Atelier B Version 3.3. (1997)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abrial, J.R., Mussat, L. (1998). Introducing dynamic constraints in B. In: Bert, D. (eds) B’98: Recent Advances in the Development and Use of the B Method. B 1998. Lecture Notes in Computer Science, vol 1393. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0053357
Download citation
DOI: https://doi.org/10.1007/BFb0053357
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64405-7
Online ISBN: 978-3-540-69769-5
eBook Packages: Springer Book Archive