{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T06:23:55Z","timestamp":1759991035965},"reference-count":23,"publisher":"Wiley","issue":"2","license":[{"start":{"date-parts":[[2011,1,23]],"date-time":"2011-01-23T00:00:00Z","timestamp":1295740800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Pract Exp"],"published-print":{"date-parts":[[2011,2]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Two methods have been identified for Event\u2010B model decomposition: shared variable and shared event. The purpose of this paper is to introduce the two approaches and the respective tool support in the Rodin platform. Besides alleviating the complexity for large systems and respective proofs, decomposition allows team development in parallel over the same Event\u2010B project which is very attractive in the industrial environment. Copyright \u00a9 2011 John Wiley &amp; Sons, Ltd.<\/jats:p>","DOI":"10.1002\/spe.1002","type":"journal-article","created":{"date-parts":[[2011,1,24]],"date-time":"2011-01-24T02:41:16Z","timestamp":1295836876000},"page":"199-208","source":"Crossref","is-referenced-by-count":35,"title":["Decomposition tool for event\u2010B"],"prefix":"10.1002","volume":"41","author":[{"given":"Renato","family":"Silva","sequence":"first","affiliation":[]},{"given":"Carine","family":"Pascal","sequence":"additional","affiliation":[]},{"given":"Thai Son","family":"Hoang","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Butler","sequence":"additional","affiliation":[]}],"member":"311","published-online":{"date-parts":[[2011,1,23]]},"reference":[{"key":"e_1_2_8_2_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"issue":"1","key":"e_1_2_8_3_2","first-page":"1","article-title":"Refinement, decomposition, and instantiation of discrete models: Application to event\u2010B","volume":"77","author":"Abrial JR","year":"2007","journal-title":"Fundamenta Informaticae"},{"key":"e_1_2_8_4_2","unstructured":"AbrialJR.Event model decomposition. Technical Report ETH Zurich 2009 (Unpublished)."},{"key":"e_1_2_8_5_2","unstructured":"ButlerM.Synchronisation\u2010based decomposition for event\u2010B. RODIN Deliverable D19 Intermediate Report on Methodology 2006;47\u201357."},{"key":"e_1_2_8_6_2","doi-asserted-by":"crossref","unstructured":"ButlerM.Decomposition structures for event\u2010B. Integrated Formal Methods iFM2009 February2009;20\u201338.","DOI":"10.1007\/978-3-642-00255-7_2"},{"key":"e_1_2_8_7_2","unstructured":"Rodin: RODIN project Homepage. Available at:http:\/\/rodin.cs.ncl.ac.uk[27 July2010]."},{"key":"e_1_2_8_8_2","unstructured":"ButlerMJ.A CSP approach to action systems. PhD Thesis Oxford University 1992;61\u201372."},{"key":"e_1_2_8_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/s002360050148"},{"key":"e_1_2_8_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0027291"},{"key":"e_1_2_8_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11811-1_24"},{"key":"e_1_2_8_12_2","unstructured":"Eclipse: Eclipse homepage. Available at:http:\/\/www.eclipse.org[27 July2010]."},{"key":"e_1_2_8_13_2","unstructured":"ButlerM HallerstedeS.The rodin formal modelling tool. BCS\u2010FACS Christmas 2007 Meeting\u2014Formal Methods In Industry London December2007;1\u20135."},{"key":"e_1_2_8_14_2","unstructured":"B4free. Available at:http:\/\/www.b4free.com[27 July2010]."},{"key":"e_1_2_8_15_2","unstructured":"ProB. Available at:http:\/\/www.stups.uni\u2010duesseldorf.de\/ProB\/overview.php[27 July2010]."},{"key":"e_1_2_8_16_2","unstructured":"SilvaR ButlerM. Parallel composition using event\u2010B. Available at:http:\/\/wiki.event\u2010b.org\/index.php\/Parallel_Composition_using_Event\u2010B[27 July2010]."},{"key":"e_1_2_8_17_2","volume-title":"FM'06 Doctoral Symposium","author":"Ball E","year":"2006"},{"key":"e_1_2_8_18_2","unstructured":"BallE.An incremental process for the development of multi\u2010agent systems in event\u2010B. PhD Thesis Southampton University 2008."},{"key":"e_1_2_8_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2008.39"},{"key":"e_1_2_8_20_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1016503426126"},{"key":"e_1_2_8_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.761449"},{"key":"e_1_2_8_22_2","unstructured":"ISO. LOTOS A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. Information Systems Processing\u2014Open Systems Interconnection 1987."},{"key":"e_1_2_8_23_2","doi-asserted-by":"crossref","unstructured":"ButlerM.Refinement and decomposition of value\u2010passing action systems. CONCUR '93: Proceedings of the 4th International Conference on Concurrency Theory London U.K. 1993;217\u2013232.","DOI":"10.1007\/3-540-57208-2_16"},{"key":"e_1_2_8_24_2","series-title":"Prentice Hall International Series in Computer Science","volume-title":"Communicating Sequential Processes","author":"Hoare CAR","year":"1985"}],"container-title":["Software: Practice and Experience"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fspe.1002","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/spe.1002","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,12]],"date-time":"2023-09-12T18:40:40Z","timestamp":1694544040000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/spe.1002"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,1,23]]},"references-count":23,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,2]]}},"alternative-id":["10.1002\/spe.1002"],"URL":"https:\/\/doi.org\/10.1002\/spe.1002","archive":["Portico"],"relation":{},"ISSN":["0038-0644","1097-024X"],"issn-type":[{"value":"0038-0644","type":"print"},{"value":"1097-024X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,1,23]]}}}