Abstract
On one hand, eb 3 is a trace-based formal language created for the specification of information systems (IS). In particular, eb 3 points out the dynamic behaviour of the system. On the other hand, B is a state-based formal language well adapted for the specification of the IS static properties. We are defining a new approach called eb 4 that integrates both eb 3 and B to specify IS. eb 3 process expressions are used to represent and validate the behaviour of the system. Then, the specification is translated into B in order to specify and verify the main static properties of the IS. In this paper, we deal with the refinement of eb 3 process expressions into B specifications. Since this process cannot be automated, we define refinement patterns that can be reused to obtain B specifications that refine the event ordering properties specified in eb 3.
This is a preview of subscription content, log in via an institution to check access.
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., Mussat, L.: Introducing dynamic constraints in B. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 83–128. Springer, Heidelberg (1998)
Butler, M.: csp2B: A practical approach to combining CSP and B. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 490–508. Springer, Heidelberg (1999)
Evans, N., Treharne, H., Laleau, R., Frappier, M.: How to verify dynamic properties of information systems. In: SEFM 2004, Beijing, China, September 2004, pp. 416–425. IEEE Computer Society Press, Los Alamitos (2004)
Facon, P., Laleau, R., Nguyen, H.P.: Mapping object diagrams into B specifications. In: Methods Integration Workshop, eWiC, Leeds, UK, March 1996, Springer, Heidelberg (1996)
Fraikin, B., Frappier, M., Laleau, R.: State-based versus event-based specifications for information systems: a comparison of B and EB3. Software and Systems Modeling 4(3), 236–257 (2005)
Frappier, M., Laleau, R.: Proving event ordering properties for information systems. In: Bert, D., P. Bowen, J., 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 Systems Modeling 2(2), 134–149 (2003)
Gervais, F.: EB 4 : Vers une méthode combiné e de spécification formelle des systè mes d’information. In: Dissertation for the general examination, GRIL, Université de Sherbrooke, Québec (June 2004)
Gervais, F., Frappier, M., Laleau, R.: Synthesizing B substitutions for EB3 attribute definitions. Technical Report 683, CEDRIC, France (November 2004)
Gervais, F., Frappier, M., Laleau, R.: Synthesizing B specifications from EB3 attribute definitions. In: Romijn, J.M.T., Smith, G.P., van de Pol, J. (eds.) IFM 2005. LNCS, vol. 3771, pp. 207–226. Springer, Heidelberg (2005)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Mammar, A.: Un environnement formel pour le développement d’applications base de données. PhD thesis, CNAM, Paris, France (2002)
Mammar, A., Gervais, F., Laleau, R.: Systematic identification of preconditions from set-based integrity constraints. In: INFORSID 2006, Hammamet, Tunisia, June 2006, INFORSID, vol. 2, pp. 595–610 (2006)
Meyer, E., Souquières, J.: A systematic approach to transform OMT diagrams to a B specification. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 875–895. Springer, Heidelberg (1999)
Nguyen, H.P.: Dérivation de spécifications formelles B à partir de spécifications semi-formelles. PhD thesis, CNAM, Paris, France (1998)
Woodcock, J.C.P., Cavalcanti, A.L.C.: The Semantics of Circus. In: Bert, D., P. Bowen, J., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 184–203. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gervais, F., Frappier, M., Laleau, R. (2006). Refinement of eb 3 Process Patterns into B Specifications. In: Julliand, J., Kouchnarenko, O. (eds) B 2007: Formal Specification and Development in B. B 2007. Lecture Notes in Computer Science, vol 4355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11955757_17
Download citation
DOI: https://doi.org/10.1007/11955757_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68760-3
Online ISBN: 978-3-540-68761-0
eBook Packages: Computer ScienceComputer Science (R0)