Abstract
We are interested in verifying dynamic properties of reactive systems. The reactive systems are specified by B event systems in a refinement development. The refinement allows us to combine proof and model-checking verification techniques in a novel way. Most of the PLTL dynamic properties are preserved by refinement, but in our approach, the user can also express how a property evolves during the refinement. The preservation of the abstract property, expressed by a PLTL formula F 1, is used as an assumption for proving a PLTL formula F 2 which expresses an enriched property in the refined system. Formula F 1 is verified by model-checking on the abstract system. So, to verify the enriched formula F 2, it is enough to prove some propositions depending on the respective patterns followed by F 1 and F 2. In this paper, we show how to obtain these sufficient propositions from the refinement relation and the semantics of the PLTL formulae. The main advantage is that the user does not need to express a variant or a loop invariant to obtain automatic proofs of dynamic properties, at least for finite state event systems. Another advantage is that the model-checking is done on an abstraction with few states.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J.-R. Abrial. The B Book. Cambridge University Press-ISBN 0521-496195, 1996.
J.-R. Abrial and L. Mussat. Introducing dynamic constraints in B. In Second Conference on the B method, France, volume 1393 of Lecture Notes in Computer Science, pages 83–128. Springer Verlag, April 1998.
F. Bellegarde, C. Darlot, J. Julliand, and O. Kouchnarenko. Reformulate dynamic properties during B refinement and forget variants and loop invariants. In Proc. Int. Conf. ZB’2000, York, Angleterre. Springer-Verlag, August 2000. LNCS to appear.
F. Bellegarde, J. Julliand, and O. Kouchnarenko. Ready-simulation is not ready to express a modular refinement relation. In Proc. Int. Conf. on Fundamental Aspects of Software Engineering, FASE’2000, volume 1783 of Lecture Notes in Computer Science, pages 266–283. Springer-Verlag, April 2000.
G. Holzmann. Design and validation of protocols. Prentice Hall software series, 1991.
J. Julliand, F. Bellegarde, and B. Parreaux. De l’expression des besoins à l’expression formelle des propriétés dynamiques. Technique et Science Informatiques, 18(7), 1999.
L. Lamport. A temporal logic of actions. ACM Transactions On Programming Languages And Systems, TOPLAS, 16(3):872–923, May 1994.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag-ISBN 0-387-97664-7, 1992.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bellegarde, F., Darlot, C., Julliand, J., Kouchnarenko, O. (2001). Reformulation: a Way to Combine Dynamic Properties and B Refinement. In: Oliveira, J.N., Zave, P. (eds) FME 2001: Formal Methods for Increasing Software Productivity. FME 2001. Lecture Notes in Computer Science, vol 2021. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45251-6_2
Download citation
DOI: https://doi.org/10.1007/3-540-45251-6_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41791-0
Online ISBN: 978-3-540-45251-5
eBook Packages: Springer Book Archive