{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T14:11:30Z","timestamp":1742998290393,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031059025"},{"type":"electronic","value":"9783031059032"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"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":[[2022]]},"DOI":"10.1007\/978-3-031-05903-2_8","type":"book-chapter","created":{"date-parts":[[2022,5,19]],"date-time":"2022-05-19T10:04:19Z","timestamp":1652954659000},"page":"109-123","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Sound and Correct Formalism to Specify, Verify and Synthesize Behavior in BIG DATA Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5498-6878","authenticated-orcid":false,"given":"Fernando","family":"Asteasuain","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luciana Rodriguez","family":"Caldeira","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,5,20]]},"reference":[{"issue":"2","key":"8_CR1","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s00766-015-0242-2","volume":"22","author":"F Asteasuain","year":"2016","unstructured":"Asteasuain, F., Braberman, V.: Declaratively building behavior by means of scenario clauses. Requirements Eng. 22(2), 239\u2013274 (2016). https:\/\/doi.org\/10.1007\/s00766-015-0242-2","journal-title":"Requirements Eng."},{"key":"8_CR2","unstructured":"Asteasuain, F., Caldeira, L.R.: A parallel tableau algorithm for big data verification. In: CACIC, pp. 360\u2013369 (2020). ISBN 978-987-4417-90-9"},{"key":"8_CR3","unstructured":"Asteasuain, F., Caldeira, L.R.: An expressive and enriched specification language to synthezise behavior in big data systems. In: CACIC, pp. 357\u2013366 (2021). ISBN 978-987-633-574-4"},{"key":"8_CR4","unstructured":"Asteasuain, F., Calonge, F., Gamboa, P.: Behavioral synthesis with branching graphical scenarios. In: CONAIISI (2019)"},{"issue":"3","key":"8_CR5","first-page":"1","volume":"24","author":"F Asteasuain","year":"2021","unstructured":"Asteasuain, F., Federico, C., Manuel, D., Pablo, G.: Open and branching behavioral synthesis with scenario clauses. CLEI J. 24(3), 1\u201320 (2021)","journal-title":"CLEI J."},{"issue":"2","key":"8_CR6","first-page":"7","volume":"21","author":"F Asteasuain","year":"2021","unstructured":"Asteasuain, F., Luciana, R.C.: Exploring parallel formal verification of big-data systems. Revista Ciencia y Tecnolog\u00eda 21(2), 7\u201318 (2021)","journal-title":"Revista Ciencia y Tecnolog\u00eda"},{"key":"8_CR7","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-04519-1_1","volume-title":"Cloud Computing and Services Science","author":"D Balouek","year":"2013","unstructured":"Balouek, D., et al.: Adding virtualization capabilities to the grid\u20195000 testbed. In: Ivanov, I.I., van Sinderen, M., Leymann, F., Shan, T. (eds.) CLOSER 2012. CCIS, vol. 367, pp. 3\u201320. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-04519-1_1"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Barnat, J., Bauch, P., Brim, L., \u010ce\u0161ka, M.: Employing multiple CUDA devices to accelerate LTL model checking. In: 2010 IEEE 16th International Conference on Parallel and Distributed Systems, pp. 259\u2013266. IEEE (2010)","DOI":"10.1109\/ICPADS.2010.82"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., \u010ce\u0161ka, M., Ro\u010dkai, P.: Divine: parallel distributed model checker. In: 2010 ninth PDMC, pp. 4\u20137. IEEE (2010)","DOI":"10.1109\/PDMC-HiBi.2010.9"},{"issue":"1","key":"8_CR10","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s10009-003-0129-2","volume":"7","author":"A Bell","year":"2005","unstructured":"Bell, A., Haverkort, B.R.: Sequential and distributed model checking of petri nets. STTT J. 7(1), 43\u201360 (2005)","journal-title":"STTT J."},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Bellettini, C., Camilli, M., Capra, L., Monga, M.: Mardigras: simplified building of reachability graphs on large clusters. In: RP Workshop, pp. 83\u201395 (2013)","DOI":"10.1007\/978-3-642-41036-9_9"},{"issue":"11","key":"8_CR12","first-page":"3025","volume":"28","author":"C Bellettini","year":"2016","unstructured":"Bellettini, C., Camilli, M., Capra, L., Monga, M.: Distributed CTL model checking using map reduce: theory and practice. CCPE 28(11), 3025\u20133041 (2016)","journal-title":"CCPE"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa\u2019Ar, Y.: Synthesis of reactive (1) designs (2011)","DOI":"10.1016\/j.jcss.2011.08.007"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Boukala, M.C., Petrucci, L.: Distributed model-checking and counterexample search for CTL logic. IJSR 3,3(1\u20132), 44\u201359 (2012)","DOI":"10.1504\/IJCCBS.2012.045076"},{"key":"8_CR15","unstructured":"Brassesco, M.V.: S\u00edntesis concurrente de controladores para juegos definidos con objetivos de generalized reactivity(1). Tesis de Licenciatura., http:\/\/dc.sigedep.exactas.uba.ar\/media\/academic\/grade\/thesis\/tesis_18.pdf UBA FCEyN Dpto Computacion (2017)"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Brim, L., \u010cern\u00e1, I., Moravec, P., \u0160im\u0161a, J.: Accepting predecessors are better than back edges in distributed LTL model-checking. In: FMCAD, pp. 352\u2013366 (2004)","DOI":"10.1007\/978-3-540-30494-4_25"},{"issue":"1","key":"8_CR17","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/s10009-004-0163-8","volume":"7","author":"L Brim","year":"2005","unstructured":"Brim, L., Yorav, K., \u017d\u00eddkov\u00e1, J.: Assumption-based distribution of CTL model checking. STTT 7(1), 61\u201373 (2005)","journal-title":"STTT"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Camilli, M.: Formal verification problems in a big data world: towards a mighty synergy. In: ICSE, pp. 638\u2013641 (2014)","DOI":"10.1145\/2591062.2591088"},{"issue":"1","key":"8_CR19","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1111\/jpim.12545","volume":"38","author":"F Cappa","year":"2021","unstructured":"Cappa, F., Oriani, R., Peruffo, E., McCarthy, I.: Big data for creating and capturing value in the digitalized environment: unpacking the effects of volume, variety, and veracity on firm performance. J. Prod. Innov. Manage. 38(1), 49\u201367 (2021)","journal-title":"J. Prod. Innov. Manage."},{"issue":"5","key":"8_CR20","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/s10009-020-00576-x","volume":"22","author":"R DeFrancisco","year":"2020","unstructured":"DeFrancisco, R., Cho, S., Ferdman, M., Smolka, S.A.: Swarm model checking on the GPU. STTT 22(5), 583\u2013599 (2020)","journal-title":"STTT"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Ding, J., Zhang, D., Hu, X.-H.: A framework for ensuring the quality of a big data service. In: 2016 SCC, pp. 82\u201389. IEEE (2016)","DOI":"10.1109\/SCC.2016.18"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"Drechsler, R., et al.: Advanced Formal Verification. vol. 122. Springer, New York (2004). https:\/\/doi.org\/10.1007\/b105236","DOI":"10.1007\/b105236"},{"issue":"7","key":"8_CR23","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","volume":"27","author":"V D\u2019silva","year":"2008","unstructured":"D\u2019silva, V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 27(7), 1165\u20131178 (2008)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"8_CR24","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1016\/j.cosrev.2015.05.002","volume":"17","author":"CK Emani","year":"2015","unstructured":"Emani, C.K., Cullot, N., Nicolle, C.: Understandable big data: a survey. Comput. Sci. Rev. 17, 70\u201381 (2015)","journal-title":"Comput. Sci. Rev."},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Magee, J.: Fluent model checking for event-based systems. In: European Software Engineering Conference, pp. 257\u2013266 (2003)","DOI":"10.1145\/949952.940106"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Hummel, O., Eichelberger, H., Giloj, A., Werle, D., Schmid, K.: A collection of software engineering challenges for big data system development. In: SEAA, pp. 362\u2013369. IEEE (2018)","DOI":"10.1109\/SEAA.2018.00066"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Inverso, O., Trubiani, C.: Parallel and distributed bounded model checking of multi-threaded programs. In: PPoPP, pp. 202\u2013216 (2020)","DOI":"10.1145\/3332466.3374529"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Kumar, V.D., Alencar, P.: Software engineering for big data projects: domains, methodologies and gaps. In: 2016 IEEE International Conference on Big Data (Big Data), pp. 2886\u20132895. IEEE (2016)","DOI":"10.1109\/BigData.2016.7840938"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Laigner, R., Kalinowski, M., Lifschitz, S., Monteiro, R.S., de Oliveira, D.: A systematic mapping of software engineering approaches to develop big data systems. In: SEAA, pp. 446\u2013453. IEEE (2018)","DOI":"10.1109\/SEAA.2018.00079"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203\u2013210. IEEE (1988)","DOI":"10.1109\/LICS.1988.5119"},{"issue":"2","key":"8_CR31","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/s10796-014-9492-7","volume":"17","author":"S Li","year":"2014","unstructured":"Li, S., Xu, L.D., Zhao, S.: The internet of things: a survey. Inf. Syst. Front. 17(2), 243\u2013259 (2014). https:\/\/doi.org\/10.1007\/s10796-014-9492-7","journal-title":"Inf. Syst. Front."},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Maoz, S., Ringert, J.O.: Synthesizing a Lego forklift controller in gr (1): a case study. arXiv preprint arXiv:1602.01172 (2016)","DOI":"10.4204\/EPTCS.202.5"},{"key":"8_CR33","series-title":"Smart Innovation, Systems and Technologies","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-981-16-5036-9_30","volume-title":"Advances in Intelligent Data Analysis and Applications","author":"M Naeem","year":"2022","unstructured":"Naeem, M., et al.: Trends and future perspective challenges in big data. In: Pan, J.-S., Balas, V.E., Chen, C.-M. (eds.) Advances in Intelligent Data Analysis and Applications. SIST, vol. 253, pp. 309\u2013325. Springer, Singapore (2022). https:\/\/doi.org\/10.1007\/978-981-16-5036-9_30"},{"issue":"3","key":"8_CR34","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1109\/MS.2021.3049322","volume":"38","author":"S Nejati","year":"2021","unstructured":"Nejati, S.: Next-generation software verification: an AI perspective. IEEE Softw. 38(3), 126\u2013130 (2021)","journal-title":"IEEE Softw."},{"issue":"1","key":"8_CR35","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1109\/MIS.2014.76","volume":"30","author":"CE Otero","year":"2014","unstructured":"Otero, C.E., Peter, A.: Research directions for engineering big data analytics software. IEEE Intell. Syst. 30(1), 13\u201319 (2014)","journal-title":"IEEE Intell. Syst."},{"issue":"1","key":"8_CR36","first-page":"74","volume":"4","author":"PA Sri","year":"2016","unstructured":"Sri, P.A., Anusha, M.: Big data-survey. Indonesian J. Electr. Eng. Inf. (IJEEI) 4(1), 74\u201380 (2016)","journal-title":"Indonesian J. Electr. Eng. Inf. (IJEEI)"},{"key":"8_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/978-3-540-71209-1_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y-K Tsay","year":"2007","unstructured":"Tsay, Y.-K., Chen, Y.-F., Tsai, M.-H., Wu, K.-N., Chan, W.-C.: GOAL: a graphical tool for manipulating B\u00fcchi automata and temporal formulae. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 466\u2013471. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_35"},{"key":"8_CR38","doi-asserted-by":"crossref","unstructured":"Xu, L.D., Xu, E.L., Li, L.: Industry 4.0: state of the art and future trends. Int. J. Prod. Res. 56(8), 2941\u20132962 (2018)","DOI":"10.1080\/00207543.2018.1444806"}],"container-title":["Communications in Computer and Information Science","Computer Science \u2013 CACIC 2021"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-05903-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,25]],"date-time":"2024-09-25T14:13:12Z","timestamp":1727273592000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-05903-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031059025","9783031059032"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-05903-2_8","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"20 May 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CACIC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Argentine Congress of Computer Science","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 October 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 October 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cacic2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cacic2021.unsa.edu.ar\/en\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"RedUNCI","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"130","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":"18","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":"3","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":"14% - 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.1","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":"1.2","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)"}}]}}