{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T20:06:16Z","timestamp":1773086776820,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540304920","type":"print"},{"value":"9783540322405","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11589976_13","type":"book-chapter","created":{"date-parts":[[2005,10,26]],"date-time":"2005-10-26T13:38:16Z","timestamp":1130333896000},"page":"207-226","source":"Crossref","is-referenced-by-count":11,"title":["Synthesizing B Specifications from eb 3 Attribute Definitions"],"prefix":"10.1007","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Gervais","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marc","family":"Frappier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R\u00e9gine","family":"Laleau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning programs to meanings","author":"J.R. Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-Book: Assigning programs to meanings. Cambridge University Press, Cambridge (1996)"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/10930755_1","volume-title":"Theorem Proving in Higher Order Logics","author":"J.R. Abrial","year":"2003","unstructured":"Abrial, J.R., Cansell, D.: Click\u2019n Prove: Interactive proofs within set theory. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 1\u201324. Springer, Heidelberg (2003)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/BFb0053357","volume-title":"B\u201998: Recent Advances in the Development and Use of the B Method","author":"J.R. Abrial","year":"1998","unstructured":"Abrial, J.R., Mussat, L.: Introducing dynamic constraints in B. In: Bert, D. (ed.) B 1998. LNCS, vol.\u00a01393, p. 83. Springer, Heidelberg (1998)"},{"key":"13_CR4","unstructured":"B-Core (UK) Ltd.: B-Toolkit, http:\/\/www.b-core.com\/btoolkit.html"},{"issue":"4","key":"13_CR5","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/PL00003930","volume":"12","author":"M. Butler","year":"2000","unstructured":"Butler, M.: csp2B: a practical approach to combining CSP and B. Formal Aspects of Computing\u00a012(4), 182\u2013198 (2000)","journal-title":"Formal Aspects of Computing"},{"key":"13_CR6","unstructured":"Clearsy: Atelier B, http:\/\/www.atelierb-societe.com"},{"key":"13_CR7","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139173018","volume-title":"The functional approach to programming","author":"G. Cousineau","year":"1998","unstructured":"Cousineau, G., Mauny, M.: The functional approach to programming. Cambridge University Press, Cambridge (1998)"},{"key":"13_CR8","volume-title":"Fundamentals of Database Systems","author":"R. Elmasri","year":"2004","unstructured":"Elmasri, R., Navathe, S.B.: Fundamentals of Database Systems, 4th edn. Addison-Wesley, Reading (2004)","edition":"4"},{"key":"13_CR9","volume-title":"2nd IEEE Intern. Conf. SEFM","author":"N. Evans","year":"2004","unstructured":"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)"},{"key":"13_CR10","series-title":"Series EWICS","volume-title":"Method Integration Workshop","author":"P. Facon","year":"1996","unstructured":"Facon, P., Laleau, R., Nguyen, H.P.: Mapping object diagrams into B specifications. In: Method Integration Workshop, Leeds, UK. Series EWICS. Springer, Heidelberg (1996)"},{"key":"13_CR11","unstructured":"Fischer, C.: Combination and implementation of processes and data: from CSP-OZ to Java. Ph.D. Thesis, University of Oldenburg (2000)"},{"issue":"3","key":"13_CR12","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/s10270-005-0083-4","volume":"4","author":"B. Fraikin","year":"2005","unstructured":"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\u00a04(3), 236\u2013257 (2005)","journal-title":"Software and System Modeling"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/3-540-44880-2_25","volume-title":"ZB 2003: Formal Specification and Development in Z and B","author":"M. Frappier","year":"2003","unstructured":"Frappier, M., Laleau, R.: Proving event ordering properties for information systems. In: Bert, D., Bowen, J.P., King, S. (eds.) ZB 2003. LNCS, vol.\u00a02651, pp. 421\u2013436. Springer, Heidelberg (2003)"},{"issue":"2","key":"13_CR14","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s10270-003-0024-z","volume":"2","author":"M. Frappier","year":"2003","unstructured":"Frappier, M., St-Denis, R.: EB3: an Entity-Based Black-Box Specification Method for Information Systems. Software and System Modeling\u00a02(2), 134\u2013149 (2003)","journal-title":"Software and System Modeling"},{"key":"13_CR15","unstructured":"Gervais, F.: EB4: Vers une m\u00e9thode combin\u00e9e de sp\u00e9cification formelle des syst\u00e8mes d\u2019information. Dissertation for the general examination, GRIL, Universit\u00e9 de Sherbrooke, Qu\u00e9bec (June 2004)"},{"key":"13_CR16","volume-title":"Proc. SEFM 2005","author":"F. Gervais","year":"2005","unstructured":"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)"},{"key":"13_CR17","unstructured":"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)"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Gervais, F., Frappier, M., Laleau, R.: Synthesizing B substitutions for EB3 attribute definitions. Technical Report 683, CEDRIC, Paris, France (November 2004)","DOI":"10.1007\/11589976_13"},{"key":"13_CR19","unstructured":"Gervais, F., Frappier, M., Laleau, R., Batanado, P.: EB3 attribute definitions: Formal language and application. Technical Report 700, CEDRIC, Paris, France (February 2005)"},{"key":"13_CR20","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)"},{"key":"13_CR21","volume-title":"Proc. 13th International Conf. on Automated Software Engineering","author":"Y. Ledru","year":"1998","unstructured":"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)"},{"key":"13_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"834","DOI":"10.1007\/978-3-540-45236-2_45","volume-title":"FME 2003: Formal Methods","author":"A. Mammar","year":"2003","unstructured":"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.\u00a02805, pp. 834\u2013854. Springer, Heidelberg (2003)"},{"key":"13_CR23","unstructured":"Nguyen, H.P.: D\u00e9rivation de sp\u00e9cifications formelles B \u00e0 partir de sp\u00e9cifications semi-formelles. Ph.D. Thesis, CEDRIC, CNAM, \u00c9vry (December 1998)"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/3-540-45648-1_10","volume-title":"ZB 2002: Formal Specification and Development in Z and B","author":"J.C.P. Woodcock","year":"2002","unstructured":"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.\u00a02272, p. 184. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11589976_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,10]],"date-time":"2020-04-10T14:05:47Z","timestamp":1586527547000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11589976_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540304920","9783540322405"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/11589976_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}