Abstract
eb 3 is a trace-based formal language created for the specification of information systems (IS). Attributes, linked to entities and associations of an IS, are computed in eb 3 by recursive functions on the valid traces of the system. On the other hand, B is a state-based formal language also well adapted for the specification of IS. In this paper, we deal with the synthesis of B specifications that correspond to eb 3 attribute definitions, in order to specify and verify safety properties like data integrity constraints. Each action in the eb 3 specification is translated into a B operation. The substitutions are obtained by an analysis of the CAML-like patterns used in the recursive functions that define the attributes in eb 3. Our technique is illustrated by an example of a simple library management system.
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.
Similar content being viewed by others
References
Abrial, J.R.: The B-Book: Assigning programs to meanings. Cambridge University Press, Cambridge (1996)
Abrial, J.R., Cansell, D.: Click’n Prove: Interactive proofs within set theory. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 1–24. Springer, Heidelberg (2003)
Abrial, J.R., Mussat, L.: Introducing dynamic constraints in B. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, p. 83. Springer, Heidelberg (1998)
B-Core (UK) Ltd.: B-Toolkit, http://www.b-core.com/btoolkit.html
Butler, M.: csp2B: a practical approach to combining CSP and B. Formal Aspects of Computing 12(4), 182–198 (2000)
Clearsy: Atelier B, http://www.atelierb-societe.com
Cousineau, G., Mauny, M.: The functional approach to programming. Cambridge University Press, Cambridge (1998)
Elmasri, R., Navathe, S.B.: Fundamentals of Database Systems, 4th edn. Addison-Wesley, Reading (2004)
Evans, N., Treharne, H., Laleau, R., Frappier, M.: How to verify dynamic properties of information systems. In: 2nd IEEE Intern. Conf. SEFM, Beijing, China, September 2004. IEEE Computer Society Press, Los Alamitos (2004)
Facon, P., Laleau, R., Nguyen, H.P.: Mapping object diagrams into B specifications. In: Method Integration Workshop, Leeds, UK. Series EWICS. Springer, Heidelberg (1996)
Fischer, C.: Combination and implementation of processes and data: from CSP-OZ to Java. Ph.D. Thesis, University of Oldenburg (2000)
Fraikin, B., Frappier, M., Laleau, R.: State-Based versus Event-Based Specifications for Information Systems: a Comparison of B and EB3. Software and System Modeling 4(3), 236–257 (2005)
Frappier, M., Laleau, R.: Proving event ordering properties for information systems. In: Bert, D., Bowen, J.P., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 421–436. Springer, Heidelberg (2003)
Frappier, M., St-Denis, R.: EB3: an Entity-Based Black-Box Specification Method for Information Systems. Software and System Modeling 2(2), 134–149 (2003)
Gervais, F.: EB4: Vers une méthode combinée de spécification formelle des systèmes d’information. Dissertation for the general examination, GRIL, Université de Sherbrooke, Québec (June 2004)
Gervais, F., Frappier, M., Laleau, R.: Generating relational database transactions from recursive functions defined on EB3 traces. In: Proc. SEFM 2005, Koblenz, Germany, September 2005. IEEE Computer Society Press, Los Alamitos (2005)
Gervais, F., Frappier, M., Laleau, R.: How to synthesize relational database transactions from EB3 attribute definitions? In: Proc. MSVVEIS 2005, Miami, USA, May 2005. INSTICC Press (2005)
Gervais, F., Frappier, M., Laleau, R.: Synthesizing B substitutions for EB3 attribute definitions. Technical Report 683, CEDRIC, Paris, France (November 2004)
Gervais, F., Frappier, M., Laleau, R., Batanado, P.: EB3 attribute definitions: Formal language and application. Technical Report 700, CEDRIC, Paris, France (February 2005)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)
Ledru, Y.: Identifying pre-conditions with the Z/EVES theorem prover. In: Proc. 13th International Conf. on Automated Software Engineering. IEEE Computer Society Press, Los Alamitos (1998)
Mammar, A., Laleau, R.: Design of an automatic prover dedicated to the refinement of database applications. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 834–854. Springer, Heidelberg (2003)
Nguyen, H.P.: Dérivation de spécifications formelles B à partir de spécifications semi-formelles. Ph.D. Thesis, CEDRIC, CNAM, Évry (December 1998)
Woodcock, J.C.P., Cavalcanti, A.L.C.: The semantics of Circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, p. 184. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gervais, F., Frappier, M., Laleau, R. (2005). Synthesizing B Specifications from eb 3 Attribute Definitions. In: Romijn, J., Smith, G., van de Pol, J. (eds) Integrated Formal Methods. IFM 2005. Lecture Notes in Computer Science, vol 3771. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11589976_13
Download citation
DOI: https://doi.org/10.1007/11589976_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30492-0
Online ISBN: 978-3-540-32240-5
eBook Packages: Computer ScienceComputer Science (R0)