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.
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., 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)