{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T08:45:05Z","timestamp":1742978705042,"version":"3.40.3"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031308253"},{"type":"electronic","value":"9783031308260"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T00:00:00Z","timestamp":1681948800000},"content-version":"vor","delay-in-days":109,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present \u201cVerified JavaBIP\u201d, a tool set for the verification of JavaBIP models. A JavaBIP model is a Java program where classes are considered as components, their behaviour described by finite state machine and synchronization annotations. While JavaBIP guarantees execution progresses according to the indicated state machines, it does not guarantee properties of the data exchanged between components. It also does not provide verification support to check whether the behaviour of the resulting concurrent program is as (safe as) expected. This paper addresses this by extending the JavaBIP engine with run-time verification support, and by extending the program verifier VerCors to verify JavaBIP models deductively. These two techniques complement each other: feedback from run-time verification allows quicker prototyping of contracts, and deductive verification can reduce the overhead of run-time verification. We demonstrate our approach on the \u201cSolidity Casino\u201d case study, known from the VerifyThis Collaborative Long Term Challenge.<\/jats:p>","DOI":"10.1007\/978-3-031-30826-0_8","type":"book-chapter","created":{"date-parts":[[2023,4,19]],"date-time":"2023-04-19T18:02:59Z","timestamp":1681927379000},"page":"143-150","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["JavaBIP meets VerCors: Towards the Safety of Concurrent Software Systems in Java"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7900-5271","authenticated-orcid":false,"given":"Simon","family":"Bliudze","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9212-1525","authenticated-orcid":false,"given":"Petra","family":"van den Bos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4467-072X","authenticated-orcid":false,"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5638-5945","authenticated-orcid":false,"given":"Robert","family":"Rubbens","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4490-7451","authenticated-orcid":false,"given":"Larisa","family":"Safina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,4,20]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","unstructured":"Abdellatif, T., Brousmiche, K.L.: Formal verification of smart contracts based on users and blockchain behaviors models. In: 9th IFIP International Conference on New Technologies, Mobility and Security (NTMS), pp.\u00a01\u20135. IEEE (Feb 2018). https:\/\/doi.org\/10.1109\/NTMS.2018.8328737","DOI":"10.1109\/NTMS.2018.8328737"},{"key":"8_CR2","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Chimento, J.M., Pace, G.J., Schneider, G.: Verifying data- and control-oriented properties combining static and runtime verification: theory and tools. Form. Methods Syst. Des. 51(1), 200\u2013265 (Aug 2017). https:\/\/doi.org\/10.1007\/s10703-017-0274-y","DOI":"10.1007\/s10703-017-0274-y"},{"key":"8_CR3","doi-asserted-by":"publisher","unstructured":"Amighi, A., Hurlin, C., Huisman, M., Haack, C.: Permission-based separation logic for multithreaded Java programs. Logical Methods in Computer Science 11(1) (Feb 2015). https:\/\/doi.org\/10.2168\/LMCS-11(1:2)2015","DOI":"10.2168\/LMCS-11(1:2)2015"},{"key":"8_CR4","unstructured":"Andr\u00e9, P., Attiogb\u00e9, C., Mottu, J.M.: Combining techniques to verify service-based components (Sep 2022), https:\/\/www.scitepress.org\/Link.aspx?doi=10.5220\/0006212106450656, [Online; accessed 26. Sep. 2022]"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"Arbab, F.: Reo: A channel-based coordination model for component composition. Mathematical Structures in Computer Science 14(3), 329\u2013366 (2004). https:\/\/doi.org\/10.1017\/S0960129504004153","DOI":"10.1017\/S0960129504004153"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: $$4^{th}$$ IEEE Int. Conf. on Software Engineering and Formal Methods (SEFM06). pp. 3\u201312 (Sep 2006). https:\/\/doi.org\/10.1109\/SEFM.2006.27, invited talk","DOI":"10.1109\/SEFM.2006.27"},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"Bliudze, S., van\u00a0den Bos, P., Huisman, M., Rubbens, R., Safina, L.: Artefact of: JavaBIP meets VerCors: Towards the Safety of Concurrent Software Systems in Java (2023). https:\/\/doi.org\/10.4121\/21763274","DOI":"10.4121\/21763274"},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"Bliudze, S., Cimatti, A., Jaber, M., Mover, S., Roveri, M., Saab, W., Wang, Q.: Formal verification of infinite-state BIP models. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) Automated Technology for Verification and Analysis. pp. 326\u2013343. Springer International Publishing, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_25","DOI":"10.1007\/978-3-319-24953-7_25"},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"Bliudze, S., Katsaros, P., Bensalem, S., Wirsing, M.: On methods and tools for rigorous system design. Int. J. Softw. Tools Technol. Transf. 23(5), 679\u2013684 (2021). https:\/\/doi.org\/10.1007\/s10009-021-00632-0","DOI":"10.1007\/s10009-021-00632-0"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"Bliudze, S., Mavridou, A., Szymanek, R., Zolotukhina, A.: Exogenous coordination of concurrent software components with JavaBIP. Software: Practice and Experience 47(11), 1801\u20131836 (Apr 2017). https:\/\/doi.org\/10.1002\/spe.2495","DOI":"10.1002\/spe.2495"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: Verification of parallel and concurrent software. In: IFM. Lecture Notes in Computer Science, vol. 10510, pp. 102\u2013110. Springer (2017), https:\/\/link.springer.com\/chapter\/10.1007\/978-3-319-66845-1_7","DOI":"10.1007\/978-3-319-66845-1_7"},{"key":"8_CR12","doi-asserted-by":"publisher","unstructured":"Bodden, E., Lam, P., Hendren, L.: Partially Evaluating Finite-State Runtime Monitors Ahead of Time. ACM Trans. Program. Lang. Syst. 34(2), 1\u201352 (Jun 2012). https:\/\/doi.org\/10.1145\/2220365.2220366","DOI":"10.1145\/2220365.2220366"},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Mavridou, A., Laszka, A., Stachtiari, E., Dubey, A.: VeriSolid: Correct-by-design smart contracts for Ethereum. In: Financial Cryptography and Data Security, pp. 446\u2013465. Springer, Cham, Switzerland (Sep 2019). https:\/\/doi.org\/10.1007\/978-3-030-32101-7_27","DOI":"10.1007\/978-3-030-32101-7_27"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Nimmer, J.W., Ernst, M.D.: Static verification of dynamically detected program invariants: Integrating Daikon and ESC\/Java. Electronic Notes in Theoretical Computer Science 55(2), 255\u2013276 (2001). https:\/\/doi.org\/10.1016\/S1571-0661(04)00256-7, RV\u20192001, Runtime Verification (in connection with CAV \u201901)","DOI":"10.1016\/S1571-0661(04)00256-7"},{"key":"8_CR15","unstructured":"Solidity team: Solidity programming language, https:\/\/soliditylang.org\/, (Accessed at: 2022-10-21)"},{"key":"8_CR16","doi-asserted-by":"publisher","unstructured":"Stulova, N., Morales, J.F., Hermenegildo, M.V.: Reducing the overhead of assertion run-time checks via static analysis. In: PPDP \u201916, pp. 90\u2013103. Association for Computing Machinery (Sep 2016). https:\/\/doi.org\/10.1145\/2967973.2968597","DOI":"10.1145\/2967973.2968597"},{"key":"8_CR17","unstructured":"VerifyThis collaborative long-term verification challenge: The Casino example, https:\/\/verifythis.github.io\/casino\/, (Accessed at: 2022-10-12)"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30826-0_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,22]],"date-time":"2023-05-22T22:02:34Z","timestamp":1684792954000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30826-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308253","9783031308260"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30826-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"20 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/fase","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"50","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"24% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6-7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The proceedings also include 2 tool papers, 2 NIER papers, and 2 competition papers","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}