{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T17:10:02Z","timestamp":1748797802029,"version":"3.41.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2016,3,1]],"date-time":"2016-03-01T00:00:00Z","timestamp":1456790400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2016,3]]},"abstract":"Abstract<\/jats:title>E<\/mml:mi>B<\/mml:mi><\/mml:mstyle><\/mml:mstyle><\/mml:mrow>3<\/mml:mn><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>is a specification language for information systems. The core of theE<\/mml:mi>B<\/mml:mi><\/mml:mstyle><\/mml:mstyle><\/mml:mrow>3<\/mml:mn><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>language consists of process algebraic specifications describing the behaviour of the entities in a system, and attribute function definitions describing the entity attributes. The verification ofE<\/mml:mi>B<\/mml:mi><\/mml:mstyle><\/mml:mstyle><\/mml:mrow>3<\/mml:mn><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>specifications against temporal properties is of great interest to users ofE<\/mml:mi>B<\/mml:mi><\/mml:mstyle><\/mml:mstyle><\/mml:mrow>3<\/mml:mn><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>. In this paper, we propose a translation fromE<\/mml:mi>B<\/mml:mi><\/mml:mstyle><\/mml:mstyle><\/mml:mrow>3<\/mml:mn><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>to LOTOS NT (LNT for short), a value-passing concurrent language with classical process algebra features. Our translation ensures the one-to-one correspondence between states and transitions of the labelled transition systems corresponding to theE<\/mml:mi>B<\/mml:mi><\/mml:mstyle><\/mml:mstyle><\/mml:mrow>3<\/mml:mn><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>and LNT specifications. We automated this translation with theE<\/mml:mi>B<\/mml:mi><\/mml:mstyle><\/mml:mstyle><\/mml:mrow>3<\/mml:mn><\/mml:msup>2<\/mml:mn>L<\/mml:mi>N<\/mml:mi>T<\/mml:mi><\/mml:mstyle><\/mml:mstyle><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>tool, thus equipping theE<\/mml:mi>B<\/mml:mi><\/mml:mstyle><\/mml:mstyle><\/mml:mrow>3<\/mml:mn><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>method with the functional verification features available in the CADP toolbox.<\/jats:p>","DOI":"10.1007\/s00165-016-0362-6","type":"journal-article","created":{"date-parts":[[2016,3,4]],"date-time":"2016-03-04T13:37:53Z","timestamp":1457098673000},"page":"145-178","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Verification of EB3 specifications using CADP"],"prefix":"10.1145","volume":"28","author":[{"given":"Dimitris","family":"Vekris","sequence":"first","affiliation":[{"name":"LACL, Universit\u00e9 Paris-Est, 61, avenue du G\u00e9n\u00e9ral de Gaulle, 94010, Cr\u00e9teil, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fr\u00e9d\u00e9ric","family":"Lang","sequence":"additional","affiliation":[{"name":"Inria Grenoble Rh\u00f4ne-Alpes and LIG-CONVECS Team, 655, avenue de l\u2019Europe, Montbonnot, 38334, Saint Ismier, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Catalin","family":"Dima","sequence":"additional","affiliation":[{"name":"LACL, Universit\u00e9 Paris-Est, 61, avenue du G\u00e9n\u00e9ral de Gaulle, 94010, Cr\u00e9teil, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Radu","family":"Mateescu","sequence":"additional","affiliation":[{"name":"Inria Grenoble Rh\u00f4ne-Alpes and LIG-CONVECS Team, 655, avenue de l\u2019Europe, Montbonnot, 38334, Saint Ismier, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Abdulla PA Bouajjani A Jonsson B Nilsson M (1999) Handling global conditions in parameterized system verification. In: Proceedings of CAV LNCS vol 1633. Springer Berlin pp 134\u2013145","DOI":"10.1007\/3-540-48683-6_14"},{"volume-title":"The B-book\u2014assigning programs to meanings","year":"2005","author":"Abrial JR","key":"e_1_2_1_2_2_2"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Barradas HR Bert D (2002) Specification and proof of liveness properties under fairness assumptions in B event systems. In: Proceedings of integrated formal methods LNCS vol 2335. Springer Berlin pp 360\u2013379","DOI":"10.1007\/3-540-47884-1_20"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Biere A Cimatti A Clarke E Zhu Y (1999) Symbolic model checking without BDDs. In: Workshop on Tools and Algorithms for the Construction and Analysis of Systems LNCS vol 1579. Springer Berlin pp 193\u2013207","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Bellegarde F Chouali S Julliand J (2002) Verification of dynamic constraints for B event systems under fairness assumptions. In: ZB 2002: formal specification and development in Z and B LNCS vol 2272. Springer Berlin pp 477\u2013496","DOI":"10.1007\/3-540-45648-1_25"},{"volume-title":"Handbook of process algebra","year":"2001","author":"Bergstra JA","key":"e_1_2_1_2_7_2"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90088-X"},{"key":"e_1_2_1_2_9_2","unstructured":"Chossart R (2010) \u00c9valuation d\u2019outils de v\u00e9rification pour les sp\u00e9cifications de syst\u00e8mes d\u2019information. Master\u2019s thesis Universit\u00e9 de Sherbrooke"},{"key":"e_1_2_1_2_10_2","unstructured":"ClearSy. Atelier B. http:\/\/www.atelierb.societe.com"},{"volume-title":"NuSMV 2: an opensource tool for symbolic model checking","year":"2002","author":"Cimatti A","key":"e_1_2_1_2_11_2"},{"volume-title":"Reference manual of the LOTOS NT to LOTOS translator\u2014version 5.4","year":"2011","author":"Champelovier D","key":"e_1_2_1_2_12_2"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Clarke EM Emerson EA Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications J ACM Trans Program Lang Syst vol 8. Springer Berlin pp 244\u2013263","DOI":"10.1145\/5397.5399"},{"key":"e_1_2_1_2_14_2","unstructured":"Emerson EA Lei CL (1986) Efficient model checking in fragments of the propositional Mu-calculus. In: Proceedings of logic in computer science pp 267\u2013278"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Evans N Treharne H Laleau R Frappier M (2004) How to verify dynamic properties of information systems. In: Workshop of software engineering and formal methods pp 416\u2013425","DOI":"10.1109\/SEFM.2004.1347547"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Frappier M Fraikin B Chossart R Chane-Yack-Fa R Ouenzar M (2010) Comparison of model checking tools for information systems. In: Proceedings of ICFEM LNCS vol 6447. Springer Berlin pp 581\u2013596","DOI":"10.1007\/978-3-642-16901-4_38"},{"key":"e_1_2_1_2_17_2","unstructured":"Formal Systems (Europe) Ltd. Failures-divergences refinement. FDR2 User Manual 1997"},{"key":"e_1_2_1_2_18_2","first-page":"134","volume-title":"J Softw Syst Model, vol 2","author":"Frappier M","year":"2003"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Garavel H Lang F Mateescu R Serwe W (2011) CADP 2010: a toolbox for the construction and analysis of distributed processes. In: Proceedings of tools and algorithms for the construction and analysis of systems LNCS vol 6605. Springer Berlin pp 372\u2013387","DOI":"10.1007\/978-3-642-19835-9_33"},{"key":"e_1_2_1_2_20_2","unstructured":"F. Gervais. Combinaison de sp\u00e9cifications formelles pour la mod\u00e9lisation des syst\u00e8mes d\u2019information . PhD thesis Universit\u00e9 de Sherbrooke 2006"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"J. Groslambert. Verification of LTL on B Event System. Technical report 2006","DOI":"10.1007\/11955757_11"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"F. Gervais M. Frappier R. Laleau. Synthesizing B Specifications from EB3 Attribute Definitions. In Proceedings of Integrated Formal Methods LNCS vol. 3771 pages 207\u2013226 Springer 2005","DOI":"10.1007\/11589976_13"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Gervais F Frappier M Laleau R (2006) Refinement of EB3 process patterns into B specifications. In: Proceedings of formal specification and development in B LNCS vol 4355. Springer Berlin pp 201\u2013215","DOI":"10.1007\/11955757_17"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Hoang T-S Abrial T-S (2011) Reasoning about liveness properties in Event-B. In: Proceedings of formal engineering methods LNCS vol 6991 pp 456\u2013471","DOI":"10.1007\/978-3-642-24559-6_31"},{"volume-title":"The spin model checker: primer and reference manual","year":"2004","author":"Holzmann GJ","key":"e_1_2_1_2_26_2"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.5555\/1146359"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Jiague ME Frappier M Gervais F Konopacki P Laleau R Milhau J St-Denis R (2010) Model-driven engineering of functional security policies. In: Proceedings of international conference on enterprise information pp 374\u2013379","DOI":"10.5220\/0003019403740379"},{"key":"e_1_2_1_2_29_2","unstructured":"ISO\/IEC (2001) Enhancements to LOTOS (E-LOTOS). International Standard number 15437:2001 International Organization for Standardization\u2014information technology Gen\u00e8ve"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Leuschel M Butler M (2003) ProB: a model checker for B. In: Proceedings of symposium on formal methods LNCS vol 2805. Springer Berlin pp 855\u2013874","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Leuschel M Massart M Currie A (2000) How to make FDR spin: LTL model checking of CSP by refinement. Technical report","DOI":"10.1007\/3-540-45251-6_6"},{"volume-title":"Programming from specifications","year":"1998","author":"Morgan CC","key":"e_1_2_1_2_33_2"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0323-x"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Milhau J Idani A Laleau R Labiadh MA Ledru Y Frappier M (2011) Combining UML ASTD and B for the formal specification of an access control filter. J Innov Syst Softw Eng 7:303\u2013313. Springer Berlin","DOI":"10.1007\/s11334-011-0166-z"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Mateescu R Thivolle D (2008) A model checking language for concurrent value-passing systems. In: Proceedings of formal methods LNCS vol 5014. Springer Berlin pp 148\u2013164","DOI":"10.1007\/978-3-540-68237-0_12"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. J. Found. Comput. Sci. vol 18. Springer Berlin pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00265555"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(82)91258-X"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Schneider S Treharne H (2005) CSP theorems for communicating B machines. J Formal Asp Comput vol 17. Springer Berlin pp 390\u2013422","DOI":"10.1007\/s00165-005-0076-7"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Schneider S Treharne H Wehrheim H Williams DM (2014) Managing LTL properties in event-B refinement. In: Proceedings of integrated formal methods. Springer Berlin pp 221\u2013237","DOI":"10.1007\/978-3-319-10181-1_14"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Treharne H Schneider S Bramble M (2003) Composing specifications using communication. In: Proceedings of ZB LNCS vol 2651. Springer Berlin pp 55\u201378","DOI":"10.1007\/3-540-44880-2_5"},{"key":"e_1_2_1_2_43_2","unstructured":"Vekris D (2014) Verification of EB3 specifications with the aid of model-checking techniques. https:\/\/tel.archives-ouvertes.fr\/tel-01140261\/document. PhD thesis Universit\u00e9 de Paris-Cr\u00e9teil"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Vekris D Dima C (2013) Efficient operational semantics for EB3 for verification of temporal properties. In: Proceedings of fundamentals of software engineering LNCS vol 8161 pp 133\u2013149. Springer Berlin","DOI":"10.1007\/978-3-642-40213-5_9"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Vekris D Lang F Dima C Mateescu R (2013) Verification of EB3 specifications using CADP. In: Proceedings of integrated formal methods LNCS vol 7940. Springer Berlin pp 61\u201376","DOI":"10.1007\/978-3-642-38613-8_5"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0362-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0362-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0362-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T16:43:38Z","timestamp":1748796218000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0362-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,3]]},"references-count":45,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2016,3]]}},"alternative-id":["10.1007\/s00165-016-0362-6"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0362-6","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2016,3]]}}}