{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T11:45:51Z","timestamp":1753875951259,"version":"3.41.2"},"reference-count":47,"publisher":"Oxford University Press (OUP)","license":[{"start":{"date-parts":[[2021,9,15]],"date-time":"2021-09-15T00:00:00Z","timestamp":1631664000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>Many disciplines have adopted component-based principles to avail themselves of the many advantages they bring, especially component reusability. In a short time, the component-based architecture became a renown branch in the IT world and the center of interest of many researchers. Much work has been conducted in this context for the verification of component-based applications (CBAs). However, the main focus has been on the structural aspect of such compositions, while the behavioral aspect has seldom been dealt with. In this paper, our goal is to close this gap and propose a formal approach to verify the behavioral correctness of CBAs. We first define a set of requirements to be satisfied by the structure and the behavior of a CBA, represented by a set of interactions that may occur between their components. Then, we build a formal Event-B model to represent these requirements in a rigorous and non-ambiguous way. The use of the Event-B refinement technique allows us to master the complexity of CBAs by introducing their elements in an incremental manner. The correctness of the development is ensured by establishing a set of proof obligations, under the Rodin platform, and also by animating it with the ProB animator\/model checker. The approach is illustrated by a running example.<\/jats:p>","DOI":"10.1093\/comjnl\/bxab115","type":"journal-article","created":{"date-parts":[[2021,9,14]],"date-time":"2021-09-14T11:10:52Z","timestamp":1631617852000},"source":"Crossref","is-referenced-by-count":1,"title":["An Event-B-Based Approach to Model and Verify Behaviors for Component-Based Applications"],"prefix":"10.1093","author":[{"given":"Amel","family":"Mammar","sequence":"first","affiliation":[{"name":"SAMOVAR, Telecom SudParis, Institut Polytechnique de Paris, Evry, 91025 France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lazhar","family":"Hamel","sequence":"additional","affiliation":[{"name":"University of Monastir, B.P 56 Avenue Taher Hadded, Monastir 5000, Tunisia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamed","family":"Graiet","sequence":"additional","affiliation":[{"name":"University of Monastir, B.P 56 Avenue Taher Hadded, Monastir 5000, Tunisia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2021,9,15]]},"reference":[{"volume-title":"SCA service component architecture\u2014Assembly model specification version 1.00","year":"2007","author":"Oasis","key":"2021091610212715800_ref1"},{"key":"2021091610212715800_ref2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"Abrial","year":"1996"},{"key":"2021091610212715800_ref3","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B\u2014System and Software Engineering","author":"Abrial","year":"2010"},{"key":"2021091610212715800_ref4","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur","year":"1994","journal-title":"Theoret. Comput. Sci."},{"key":"2021091610212715800_ref5","first-page":"161","article-title":"An Abstract Framework for Deadlock Prevention in BIP","volume-title":"Proc. FMOODS\/FORTE 13","author":"Attie","year":"2013"},{"key":"2021091610212715800_ref6","first-page":"98","article-title":"Formal Verification of Runtime Compensation of Web Service Compositions: A Refinement and Proof Based Proposal with Event-B","volume-title":"Proc. SCC 15","author":"Babin","year":"2015"},{"key":"2021091610212715800_ref7","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/TSC.2016.2594782","article-title":"Web service compensation at runtime: Formal modeling and verification using the event-B refinement and proof based formal method","volume":"10","author":"Babin","year":"2017","journal-title":"IEEE Trans. Services Comput."},{"key":"2021091610212715800_ref8","first-page":"5","article-title":"A Compositional Framework for Service Interaction Patterns and Interaction Flows","volume-title":"Proc. ICFEM 05","author":"Barros","year":"2005"},{"key":"2021091610212715800_ref9","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1109\/MS.2011.27","article-title":"Rigorous component-based system design using the BIP framework","volume":"28","author":"Basu","year":"2011","journal-title":"IEEE Softw."},{"key":"2021091610212715800_ref10","first-page":"743","article-title":"Automatic Verification of Interactions in Asynchronous Systems with Unbounded Buffers","volume-title":"Proc. ASE\u201914","author":"Basu","year":"2014"},{"volume-title":"Component Based Software Engineering A Complete Guide","year":"2020","author":"Blokdyk","key":"2021091610212715800_ref11"},{"key":"2021091610212715800_ref12","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/978-3-319-40648-0_13","article-title":"EventB2Java: A Code Generator for Event-B","volume-title":"Proc. NASA Formal Methods 16","author":"Cata\u00f1o","year":"2016"},{"key":"2021091610212715800_ref13","first-page":"228","article-title":"Automating the Building of Software Component Architectures","volume-title":"EWSA 2006: Software Architecture","author":"Desnos","year":"2006"},{"key":"2021091610212715800_ref14","first-page":"40","article-title":"Web service protocols: Compatibility and adaptation","volume":"31","author":"Dumas","year":"2008","journal-title":"IEEE Data Eng. Bull."},{"key":"2021091610212715800_ref15","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1504\/IJWGS.2005.007545","article-title":"A survey on web services composition","volume":"1","author":"Dustdar","year":"2005","journal-title":"Int. J. Web Grid Services"},{"volume-title":"Service-Oriented Architecture: Concepts, Technology, and Design","year":"2005","author":"Erl","key":"2021091610212715800_ref16"},{"key":"2021091610212715800_ref17","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1145\/1035167.1035202","article-title":"Web Services: A Process Algebra Approach","volume-title":"Proc. ICSOC 04","author":"Ferrara","year":"2004"},{"key":"2021091610212715800_ref18","doi-asserted-by":"crossref","first-page":"621","DOI":"10.1145\/988672.988756","article-title":"Analysis of Interacting BPEL Web Services","volume-title":"Proc. WWW 04","author":"Fu","year":"2004"},{"key":"2021091610212715800_ref19","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/j.tcs.2004.07.004","article-title":"Protocols: A formalism for specification and verification of reactive electronic services","volume":"328","author":"Fu","year":"2004","journal-title":"Theoret. Comput. Sci."},{"key":"2021091610212715800_ref20","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1109\/TSC.2010.1","article-title":"Event-based design and runtime verification of composite service transactional behavior","volume":"3","author":"Gaaloul","year":"2010","journal-title":"IEEE Trans. Services Comput."},{"key":"2021091610212715800_ref21","first-page":"251","article-title":"Event-B Based Approach for Verifying Dynamic Composite Service Transactional Behavior","volume-title":"Proc. ICWS 13","author":"Graiet","year":"2013"},{"key":"2021091610212715800_ref22","doi-asserted-by":"crossref","first-page":"987","DOI":"10.1007\/s00165-017-0425-3","article-title":"A verification and deployment approach for elastic component-based applications","volume":"29","author":"Graiet","year":"2017","journal-title":"Form. Asp. Comput."},{"year":"2008","author":"Kacem","article-title":"Mod\u00e9lisation des applications distribu\u00e9es \u00e0 architecture dynamique: Conception et validation","key":"2021091610212715800_ref23"},{"key":"2021091610212715800_ref24","first-page":"191","article-title":"A Petri Net-Based Model for Web Service Composition","volume-title":"Proc. ADC 03","author":"Hamadi","year":"2003"},{"key":"2021091610212715800_ref25","first-page":"220","article-title":"Transforming BPEL to Petri Nets","volume-title":"Proc. BPM 05","author":"Hinz","year":"2005"},{"key":"2021091610212715800_ref26","first-page":"174","article-title":"Supporting Reuse in Event-B Development: Modularisation Approach","volume-title":"Proc. ASM 10","author":"Iliasov","year":"2010"},{"volume-title":"The Theory of Timed I\/O Automata","year":"2010","author":"Kaynar","key":"2021091610212715800_ref27"},{"key":"2021091610212715800_ref28","first-page":"30:1","article-title":"Parameterized Systems in BIP: Design and Model Checking","volume-title":"Proc. CONCUR\u201916","author":"Konnov","year":"2016"},{"key":"2021091610212715800_ref29","first-page":"44","article-title":"Formal Verification of SCA Assembly Model with Event-B","volume-title":"Proc. SKG\u20192013","author":"Lahouij","year":"2013"},{"key":"2021091610212715800_ref30","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/j.entcs.2011.11.011","article-title":"Combining proof and model-checking to validate reconfigurable architectures","volume":"279","author":"Lanoix","year":"2011","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"2021091610212715800_ref31","first-page":"32","article-title":"Component Substitution through Dynamic Reconfigurations","volume-title":"Proc. FESCA 14","author":"Lanoix","year":"2014"},{"key":"2021091610212715800_ref32","first-page":"855","article-title":"ProB: A Model Checker for B","volume-title":"Proc. FM 03","author":"Leuschel","year":"2003"},{"key":"2021091610212715800_ref33","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/s10270-008-0098-8","article-title":"A systematic approach to generate B preconditions: Application to the database domain","volume":"8","author":"Mammar","year":"2009","journal-title":"Softw. Syst. Model."},{"year":"2020","author":"Mammar","article-title":"An Event-B-Based Approach to Model and Verify Behaviors for Component-Based Applications","key":"2021091610212715800_ref34"},{"key":"2021091610212715800_ref35","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1007\/s00165-014-0323-x","article-title":"Proof-based verification approaches for dynamic properties: Application to the information system domain","volume":"27","author":"Mammar","year":"2015","journal-title":"Form. Asp. Comput."},{"volume-title":"Understanding SCA (Service Component Architecture)","year":"2009","author":"Marino","key":"2021091610212715800_ref36"},{"key":"2021091610212715800_ref37","first-page":"19","article-title":"Analyzing Web Service Based Business Processes","volume-title":"Proc. ETAPS 05","author":"Martens","year":"2005"},{"volume-title":"Communication and Concurrency","year":"1989","author":"Milner","key":"2021091610212715800_ref38"},{"volume-title":"Service Component Architecture Assembly Model Specification Version 1.1","year":"2011","author":"OASIS","key":"2021091610212715800_ref39"},{"key":"2021091610212715800_ref40","first-page":"29","article-title":"Specifying Formal Executable Behavioral Models for Structural Models of Service-Oriented Components","volume-title":"Proc. ACT4SOC 10","author":"Riccobene","year":"2010"},{"key":"2021091610212715800_ref41","doi-asserted-by":"crossref","first-page":"1077","DOI":"10.1007\/s00165-013-0289-0","article-title":"A formal framework for service modeling and prototyping","volume":"26","author":"Riccobene","year":"2014","journal-title":"Form. Asp. Comput."},{"key":"2021091610212715800_ref42","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s10009-015-0381-2","article-title":"Code generation for event-B","volume":"19","author":"Rivera","year":"2017","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"2021091610212715800_ref43","first-page":"43","article-title":"Describing and Reasoning on Web Services Using Process Algebra","volume-title":"Proc. ICWS 04","author":"Sala\u00fcn","year":"2004"},{"key":"2021091610212715800_ref44","first-page":"199","article-title":"Decomposition tool for event-B","volume":"41","author":"Silva","year":"2011","journal-title":"Software"},{"key":"2021091610212715800_ref45","doi-asserted-by":"crossref","first-page":"687","DOI":"10.1145\/1135777.1135878","article-title":"ASDL: A Wide Spectrum Language for Designing Web Services","volume-title":"Proc. WWW 06","author":"Solanki","year":"2006"},{"key":"2021091610212715800_ref46","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1023\/A:1022407907596","article-title":"Synchronizations in team automata for groupware systems","volume":"12","author":"ter Beek","year":"2003","journal-title":"Comput. Supp. Coop. Work"},{"key":"2021091610212715800_ref47","first-page":"420","article-title":"WS-Net: A Petri-Net Based Specification Model for Web Services","volume-title":"Proc. ICWS 04","author":"Zhang","year":"2004"}],"container-title":["The Computer Journal"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/comjnl\/advance-article-pdf\/doi\/10.1093\/comjnl\/bxab115\/40392201\/bxab115.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/comjnl\/advance-article-pdf\/doi\/10.1093\/comjnl\/bxab115\/40392201\/bxab115.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,16]],"date-time":"2021-09-16T10:22:32Z","timestamp":1631787752000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/comjnl\/advance-article\/doi\/10.1093\/comjnl\/bxab115\/6367626"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,15]]},"references-count":47,"URL":"https:\/\/doi.org\/10.1093\/comjnl\/bxab115","relation":{},"ISSN":["0010-4620","1460-2067"],"issn-type":[{"type":"print","value":"0010-4620"},{"type":"electronic","value":"1460-2067"}],"subject":[],"published":{"date-parts":[[2021,9,15]]},"article-number":"bxab115"}}