Abstract
This paper presents a tool for verifying dynamic properties using the B formal method. For example, in a library system, typical dynamic properties would be that a member has a possibility to borrow a book or make a reservation if it is already reserved by another member. Starting from a B specification and a dynamic property, this tool generates the proof obligations that permit the user to check whether the property is verified on the B specification. The goal of such a tool is to discharge the users from tedious and error-prone activities.
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
Abrial, J.R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)
Mammar, A., Frappier, M., Diagne, F.: A Proof-Based Approach to Verifying Reachability Properties. In: Chu, W.C., Wong, W.E., Palakal, M.J., Hung, C.C. (eds.) SAC, pp. 1651–1657. ACM (2011)
Frappier, M., Diagne, F., Mammar, A.: Proving Reachability in B using Substitution Refinement. Electron. Notes Theor. Comput. Sci. 280, 47–56 (2011)
Mammar, A., Frappier, M., Chane-Yack-Fa, R.: Proving the Absence Property Pattern Using the B Method. In: HASE, pp. 167–170 (2012)
Diagne, F.: Preuve de Propriétés Dynamiques en B. PhD thesis, Télécom SudParis/Université de Sherbrooke (2013), http://www-public.it-sudparis.eu/~mammar_a/theseFamaDiagne.pdf
Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice Hall International series in computer science. Prentice Hall (1994)
Pnueli, A.: The Temporal Logic of Programs. In: FOCS, pp. 46–57 (1977)
ClearSy: Manuel de Référence du Langage B. ClearSy, France (2007)
Frappier, M., Fraikin, B., Chossart, R., Chane-Yack-Fa, R., Ouenzar, M.: Comparison of Model Checking Tools for Information Systems. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 581–596. Springer, Heidelberg (2010)
Abrial, J.R., Mussat, L.: Introducing dynamic constraints in b. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 83–128. Springer, Heidelberg (1998)
Barradas, H.R., Bert, D.: Specification and Proof of Liveness Properties under Fairness Assumptions in B Event Systems. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 360–379. Springer, Heidelberg (2002)
Hoang, T.S., Abrial, J.R.: Reasoning about Liveness Properties in Event-B. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 456–471. Springer, Heidelberg (2011)
Leuschel, M., Butler, M.: ProB: An Automated Analysis Toolset for the B Method. STTT 10(2), 185–203 (2008)
Frappier, M., Fraikin, B., Chossart, R., Chane-Yack-Fa, R., Ouenzar, M.: Comparison of Model Checking Tools for Information Systems. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 581–596. Springer, Heidelberg (2010)
Abrial, J.R.: Modeling in Event-B - System and Software Engineering. Cambridge University Press (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Diagne, F., Mammar, A., Frappier, M. (2014). A Tool for Verifying Dynamic Properties in B. In: Giannakopoulou, D., Salaün, G. (eds) Software Engineering and Formal Methods. SEFM 2014. Lecture Notes in Computer Science, vol 8702. Springer, Cham. https://doi.org/10.1007/978-3-319-10431-7_23
Download citation
DOI: https://doi.org/10.1007/978-3-319-10431-7_23
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10430-0
Online ISBN: 978-3-319-10431-7
eBook Packages: Computer ScienceComputer Science (R0)