{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T09:42:47Z","timestamp":1762508567740,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030837228"},{"type":"electronic","value":"9783030837235"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-83723-5_14","type":"book-chapter","created":{"date-parts":[[2021,8,4]],"date-time":"2021-08-04T06:02:58Z","timestamp":1628056978000},"page":"199-215","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Verification of Liveness and Safety Properties of Behavioral Programs Using\u00a0BPjs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0153-8465","authenticated-orcid":false,"given":"Michael","family":"Bar-Sinai","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5832-8768","authenticated-orcid":false,"given":"Gera","family":"Weiss","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,8,5]]},"reference":[{"unstructured":"Runtime Verification Conference Website (2001\u20132019). http:\/\/www.runtime-verification.org\/","key":"14_CR1"},{"unstructured":"A scenario based on-board software and testing environment for satellites. In: Proceedings of the 59th Israel Annual Conference on Aerospace Sciences (2019)","key":"14_CR2"},{"unstructured":"Appendix, Code: Verification of Liveness and Safety Properties of Behavioral Programs Using BPjs. Zenodo, July 2020. https:\/\/doi.org\/10.5281\/zenodo.3967250","key":"14_CR3"},{"unstructured":"Aljamaan, H., Garzon, M., Lethbridge, T.: UmpleRun: a dynamic analysis tool for textually modeled state machines using umple. In: EXE@MoDELS, pp. 16\u201320 (2015)","key":"14_CR4"},{"unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)","key":"14_CR5"},{"unstructured":"Bar-Sinai, M.: BP visual running examples code repository (2019). https:\/\/github.com\/bthink-bgu\/VisualRunningExamples","key":"14_CR6"},{"doi-asserted-by":"crossref","unstructured":"Bar-Sinai, M., Weiss, G.: Code Appendix for \u201cBPjs - A Behavioral Programming Tool Suite\u201d (2018). https:\/\/github.com\/michbarsinai\/BPjs-SCP-OSP_CodeAppendix","key":"14_CR7","DOI":"10.1145\/3270112.3270126"},{"unstructured":"Bar-Sinai, M., Weiss, G., Marron, A.: Defining semantic variations of diagrammatic languages using behavioral programming and queries. In: EXE@MoDELS (2016)","key":"14_CR8"},{"doi-asserted-by":"publisher","unstructured":"Bar-Sinai, M., Weiss, G., Shmuel, R.: BPjs: an extensible, open infrastructure for behavioral programming research. In: Proceedings of the 21st ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings, MODELS 2018, Copenhagen, Denmark, 14\u201319 October 2018, pp. 59\u201360 (2018). https:\/\/doi.org\/10.1145\/3270112.3270126","key":"14_CR9","DOI":"10.1145\/3270112.3270126"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-030-45237-7_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2020","unstructured":"Beyer, D.: Advances in automatic software verification: SV-COMP 2020. In: TACAS 2020. LNCS, vol. 12079, pp. 347\u2013367. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_21"},{"issue":"1","key":"14_CR11","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1023\/A:1011227529550","volume":"19","author":"W Damm","year":"2001","unstructured":"Damm, W., Harel, D.: LSCs: breathing life into message sequence charts. Formal Methods Syst. Des. 19(1), 45\u201380 (2001). https:\/\/doi.org\/10.1023\/A:1011227529550","journal-title":"Formal Methods Syst. Des."},{"doi-asserted-by":"publisher","unstructured":"Gordon, M., Marron, A., Meerbaum-Salant, O.: Spaghetti for the main course?: observations on the naturalness of scenario-based programming. In: Proceedings of the 17th ACM Annual Conference on Innovation and Technology in Computer Science Education (ITiCSE 2012). ACM, New York (2012). https:\/\/doi.org\/10.1145\/2325296.2325346","key":"14_CR12","DOI":"10.1145\/2325296.2325346"},{"unstructured":"Greenyer, J., Bar-Sinai, M., Weiss, G., Sadon, A., Marron, A.: Modeling and programming a leader-follower challenge problem with scenario-based tools. In: Hebig, R., Berger, T. (eds.) Proceedings of MODELS 2018 Workshops: ModComp, MRT, OCL, FlexMDE, EXE, COMMitMDE, MDETools, GEMOC, MORSE, MDE4IoT, MDEbug, MoDeVVa, ME, MULTI, HuFaMo, AMMoRe, PAINS co-located with ACM\/IEEE 21st International Conference on Model Driven Engineering Languages and Systems (MODELS 2018), Copenhagen, Denmark, 14 October 2018. CEUR Workshop Proceedings, vol. 2245, pp. 376\u2013385. CEUR-WS.org (2018). http:\/\/ceur-ws.org\/Vol-2245\/mdetools_paper_8.pdf","key":"14_CR13"},{"doi-asserted-by":"crossref","unstructured":"Harel, D., Katz, G.: Scaling-up behavioral programming: steps from basic principles to application architectures. In: Proceedings of the 4th International Workshop on Programming Based on Actors Agents & Decentralized Control, pp. 95\u2013108. ACM (2014)","key":"14_CR14","DOI":"10.1145\/2687357.2687359"},{"doi-asserted-by":"crossref","unstructured":"Harel, D., Lampert, R., Marron, A., Weiss, G.: Model-checking behavioral programs. In: Proceedings of 11th International Conference on Embedded Software (EMSOFT), pp. 279\u2013288 (2011)","key":"14_CR15","DOI":"10.1145\/2038642.2038686"},{"doi-asserted-by":"publisher","unstructured":"Harel, D., Marelly, R.: Come, Let\u2019s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-642-19029-2","key":"14_CR16","DOI":"10.1007\/978-3-642-19029-2"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-642-14107-2_12","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"D Harel","year":"2010","unstructured":"Harel, D., Marron, A., Weiss, G.: Programming coordinated behavior in Java. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 250\u2013274. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14107-2_12"},{"doi-asserted-by":"crossref","unstructured":"Harel, D., Marron, A., Weiss, G.: Behavioral programming. Comm. ACM 55(7) (2012)","key":"14_CR18","DOI":"10.1145\/2209249.2209270"},{"doi-asserted-by":"publisher","unstructured":"Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. Int. J. Softw. Tools Technol. Transfer 2(4), 366\u2013381 (2000). https:\/\/doi.org\/10.1007\/s100090050043","key":"14_CR19","DOI":"10.1007\/s100090050043"},{"doi-asserted-by":"publisher","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997). https:\/\/doi.org\/10.1109\/32.588521","key":"14_CR20","DOI":"10.1109\/32.588521"},{"doi-asserted-by":"publisher","unstructured":"Keller, R.M.: Formal verification of parallel programs. Commun. ACM 19(7), 371\u2013384 (1976). https:\/\/doi.org\/10.1145\/360248.360251","key":"14_CR21","DOI":"10.1145\/360248.360251"},{"doi-asserted-by":"publisher","unstructured":"Klose, J., Toben, T., Westphal, B., Wittke, H.: Check it out: on the efficient formal verification of live sequence charts. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 219\u2013233. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_22","key":"14_CR22","DOI":"10.1007\/11817963_22"},{"doi-asserted-by":"publisher","unstructured":"Lethbridge, T.C., Mussbacher, G., Forward, A., Badreddin, O.: Teaching UML using umple: applying model-oriented programming in the classroom. In: 2011 24th IEEE-CS Conference on Software Engineering Education and Training (CSEE T), pp. 421\u2013428, May 2011. https:\/\/doi.org\/10.1109\/CSEET.2011.5876118","key":"14_CR23","DOI":"10.1109\/CSEET.2011.5876118"},{"unstructured":"Mozilla, individual contributors: The Mozilla Rhino JavaScript Engine (2019). https:\/\/mozilla.org\/rhino","key":"14_CR24"},{"doi-asserted-by":"publisher","unstructured":"Rodrigues da Silva, A.: Model-driven engineering. Comput. Lang. Syst. Struct. 43(C), 139\u2013155 (2015). https:\/\/doi.org\/10.1016\/j.cl.2015.06.001","key":"14_CR25","DOI":"10.1016\/j.cl.2015.06.001"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-83723-5_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,4]],"date-time":"2021-08-04T06:08:49Z","timestamp":1628057329000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-83723-5_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030837228","9783030837235"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-83723-5_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"5 August 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/isola-conference.org\/isola2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}