{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T11:36:29Z","timestamp":1770896189022,"version":"3.50.1"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2017,11,1]],"date-time":"2017-11-01T00:00:00Z","timestamp":1509494400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000921","name":"European Cooperation in Science and Technology","doi-asserted-by":"publisher","award":["IC 1402"],"award-info":[{"award-number":["IC 1402"]}],"id":[{"id":"10.13039\/501100000921","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2017,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This paper addresses the monitoring of logic-independent linear-time user-provided properties in multi-threaded component-based systems. We consider intrinsically independent components that can be executed concurrently with a centralized coordination for multiparty interactions. In this context, the problem that arises is that a global state of the system is not available to the monitor. A naive solution to this problem would be to plug in a monitor which would force the system to synchronize in order to obtain the sequence of global states at runtime. Such a solution would defeat the whole purpose of having concurrent components. Instead, we reconstruct on-the-fly the global states by accumulating the partial states traversed by the system at runtime. We define transformations of components that preserve their semantics and concurrency and, at the same time, allow to monitor global-state properties. Moreover, we present RVMT-BIP, a prototype tool implementing the transformations for monitoring multi-threaded systems described in the Behavior, Interaction, Priority (BIP) framework, an expressive framework for the formal construction of heterogeneous systems. Our experiments on several multi-threaded BIP systems show that RVMT-BIP induces a cheap runtime overhead.<\/jats:p>","DOI":"10.1007\/s00165-017-0422-6","type":"journal-article","created":{"date-parts":[[2017,3,6]],"date-time":"2017-03-06T17:11:17Z","timestamp":1488820277000},"page":"951-986","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Concurrency-preserving and sound monitoring of multi-threaded component-based systems: theory, algorithms, implementation, and evaluation"],"prefix":"10.1145","volume":"29","author":[{"given":"Hosein","family":"Nazarpour","sequence":"first","affiliation":[{"name":"Inria, CNRS, VERIMAG, LIG, Univ. Grenoble Alpes, 38000, Grenoble, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yli\u00e8s","family":"Falcone","sequence":"additional","affiliation":[{"name":"Inria, CNRS, VERIMAG, LIG, Univ. Grenoble Alpes, 38000, Grenoble, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[{"name":"Inria, CNRS, VERIMAG, LIG, Univ. Grenoble Alpes, 38000, Grenoble, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[{"name":"Inria, CNRS, VERIMAG, LIG, Univ. Grenoble Alpes, 38000, Grenoble, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Basu A Bidinger P Bozga M Sifakis J (2008) Distributed semantics and implementation for systems with interaction and priority. In: Higashino KST El-Fakih KYK (eds) Formal techniques for networked and distributed systems\u2014FORTE 2008 28th IFIP WG 6.1 international conference Tokyo Japan June 10\u201313 2008 proceedings. Lecture notes in computer science vol 5048. Springer pp 116\u2013133","DOI":"10.1007\/978-3-540-68855-6_8"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-015-0226-3"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-012-0168-6"},{"key":"e_1_2_1_2_4_2","unstructured":"Basu A Bozga M Sifakis J (2006) Modeling heterogeneous real-time components in BIP. In: Fourth IEEE international conference on software engineering and formal methods (SEFM 2006) 11\u201315 September 2006 Pune India. IEEE Computer Society pp 3\u201312"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Bruneton E Coupaye T Leclercq M Qu\u00e9ma V Stefani J-B (2004) An open component model and its support in Java. In: International symposium on component-based software engineering. Springer pp 7\u201322","DOI":"10.1007\/978-3-540-24774-6_3"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Bauer AK Falcone Y (2012) Decentralised LTL monitoring. In: Giannakopoulou D Dominique M (eds) 18th international symposium on formal methods: FM 2012 Paris France August 27\u201331 2012 proceedings. Lecture notes in computer science vol 7436. Springer pp 85\u2013100","DOI":"10.1007\/978-3-642-32759-9_10"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0253-8"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn075"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Bauer A Leucker M Schallhart C (2011) Runtime verification for LTL and TLTL. ACM Trans Softw Eng Methodol 20(4):14:1\u201314:64","DOI":"10.1145\/2000799.2000800"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Bliudze S Sifakis J (2007) The algebra of connectors: structuring interaction in bip. In: Proceedings of the 7th ACM & IEEE international conference on embedded software. ACM pp 11\u201320","DOI":"10.1145\/1289927.1289935"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0251-x"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Dormoy J Kouchnarenko O Lanoix A (2010) Using temporal logic for dynamic reconfigurations of components. In: Barbosa LS Lumpe M (eds) Proceedings of the 7th international workshop on formal aspects of component software (FACS 2010). LNCS vol 6921. Springer pp 200\u2013217","DOI":"10.1007\/978-3-642-27269-1_12"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Falcone Y Cornebize T Fernandez J-C (2014) Efficient and generalized decentralized monitoring of regular languages. In: \u00c1brah\u00e1m E Palamidessi C (eds) Formal techniques for distributed objects components and systems\u201434th IFIP WG 6.1 international conference FORTE 2014 held as part of the 9th international federated conference on distributed computing techniques DisCoTec 2014 Berlin Germany June 3\u20135 2014 proceedings. Lecture notes in computer science vol 8461. Springer pp 66\u201383","DOI":"10.1007\/978-3-662-43613-4_5"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Falcone Y Fernandez J-C Mounier L (2009) Runtime verification of safety-progress properties. In: Bensalem S Peled D (eds) Proceedings of the 9th international workshop on runtime verification (RV 2009) selected papers. LNCS vol 5779. Springer pp 40\u201359","DOI":"10.1007\/978-3-642-04694-0_4"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0196-8"},{"key":"e_1_2_1_2_16_2","first-page":"2","article-title":"Runtime enforcement of regular timed properties by suppressing and delaying events","volume":"123","author":"Falcone Y","year":"2016","journal-title":"Syst Control Lett"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Falcone Y Jaber M Nguyen T-H Bozga M Bensalem S (2011) Runtime verification of component-based systems. In: SEFM 2011 pp 204\u2013220","DOI":"10.1007\/978-3-642-24690-6_15"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-013-0323-y"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-014-0217-9"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Hoare CAR (1978) Communicating sequential processes. In: The origin of concurrent programming. Springer pp 413\u2013443","DOI":"10.1007\/978-1-4757-3472-0_16"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Kouchnarenko O Weber J-F (2014) Adapting component-based systems at runtime via policies with temporal patterns. Lecture notes in computer science vol 8348. Springer Cham pp 234\u2013253","DOI":"10.1007\/978-3-319-07602-7_15"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Kouchnarenko O Weber J-F (2015) Decentralised evaluation of temporal patterns over component-based systems at runtime. Lecture notes in computer science vol 8997. Springer Cham pp 108\u2013126","DOI":"10.1007\/978-3-319-15317-9_7"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Mostafa M Bonakdarpour B (2015) Decentralized runtime verification of LTL specifications in distributed systems. In 2015 IEEE international parallel and distributed processing symposium IPDPS 2015 Hyderabad India May 25\u201329 2015. IEEE Computer Society pp 494\u2013503","DOI":"10.1109\/IPDPS.2015.95"},{"key":"e_1_2_1_2_24_2","unstructured":"Milner R (1995) Communication and concurrency. Prentice Hall International (UK) Ltd. Hertfordshire"},{"key":"e_1_2_1_2_25_2","unstructured":"Nazarpour H. Website of RVMT-BIP a tool for the runtime verification of multi-threaded BIP systems. http:\/\/www-verimag.imag.fr\/~nazarpou\/rvmt.html"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Nazarpour H Falcone Y Bensalem S Bozga M Combaz J (2016) Monitoring multi-threaded component-based systems. In: Abraham E Huisman M (eds) Proceedings of the 12th international conference on integrated formal methods. LNCS","DOI":"10.1007\/978-3-319-33693-0_10"},{"key":"e_1_2_1_2_27_2","unstructured":"Sen A Garg VK (2003) Detecting temporal logic predicates in distributed programs using computation slicing. In: Papatriantafilou M Hunel P (eds) Principles of distributed systems 7th international conference OPODIS 2003 La Martinique French West Indies December 10\u201313 2003 revised selected papers. Lecture notes in computer science vol 3144. Springer pp 171\u2013183"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2007.1011"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Sen K Vardhan A Agha G Rosu G (2006) Decentralized runtime analysis of multithreaded applications. In: 20th international parallel and distributed processing symposium (IPDPS 2006) 25\u201329 April 2006 proceedings Rhodes Island Greece. IEEE","DOI":"10.1109\/IPDPS.2006.1639591"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1006\/jpdc.1996.1298"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2634"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-017-0422-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0422-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0422-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-017-0422-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:13:53Z","timestamp":1641485633000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-017-0422-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11]]},"references-count":31,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2017,11]]}},"alternative-id":["10.1007\/s00165-017-0422-6"],"URL":"https:\/\/doi.org\/10.1007\/s00165-017-0422-6","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,11]]}}}