{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T22:35:28Z","timestamp":1743114928010,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030638818"},{"type":"electronic","value":"9783030638825"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-63882-5_7","type":"book-chapter","created":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T14:08:03Z","timestamp":1605794883000},"page":"101-118","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Modeling Big Data Processing Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8142-2525","authenticated-orcid":false,"given":"Jo\u00e3o Batista","family":"de Souza Neto","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7707-8469","authenticated-orcid":false,"given":"Anamaria Martins","family":"Moreira","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9545-1821","authenticated-orcid":false,"given":"Genoveva","family":"Vargas-Solar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5589-3895","authenticated-orcid":false,"given":"Martin A.","family":"Musicante","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,11,19]]},"reference":[{"key":"7_CR1","volume-title":"Introduction to Software Testing","author":"P Ammann","year":"2017","unstructured":"Ammann, P., Offutt, J.: Introduction to Software Testing, 2nd edn. Cambridge University Press, New York (2017)","edition":"2"},{"issue":"3","key":"7_CR2","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/s10723-016-9371-1","volume":"14","author":"F Bajaber","year":"2016","unstructured":"Bajaber, F., Elshawi, R., Batarfi, O., Altalhi, A., Barnawi, A., Sakr, S.: Big Data 2.0 processing systems: taxonomy and open challenges. J. Grid Comput. 14(3), 379\u2013405 (2016). https:\/\/doi.org\/10.1007\/s10723-016-9371-1","journal-title":"J. Grid Comput."},{"key":"7_CR3","unstructured":"Beam, A.: Apache Beam: an advanced unified programming model (2016). https:\/\/beam.apache.org\/"},{"issue":"3","key":"7_CR4","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1145\/828.833","volume":"31","author":"SD Brookes","year":"1984","unstructured":"Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560\u2013599 (1984). https:\/\/doi.org\/10.1145\/828.833","journal-title":"J. ACM"},{"issue":"4","key":"7_CR5","first-page":"28","volume":"38","author":"P Carbone","year":"2015","unstructured":"Carbone, P., Ewen, S., Haridi, S., Katsifodimos, A., Markl, V., Tzoumas, K.: Apache flink: stream and batch processing in a single engine. IEEE Data Eng. Bull. 38(4), 28\u201338 (2015)","journal-title":"IEEE Data Eng. Bull."},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/978-3-319-59647-1_31","volume-title":"Networked Systems","author":"Y-F Chen","year":"2017","unstructured":"Chen, Y.-F., Hong, C.-D., Leng\u00e1l, O., Mu, S.-C., Sinha, N., Wang, B.-Y.: An executable sequential specification for Spark aggregation. In: El Abbadi, A., Garbinato, B. (eds.) NETYS 2017. LNCS, vol. 10299, pp. 421\u2013438. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-59647-1_31"},{"key":"7_CR7","unstructured":"Chlyah, S., Gesbert, N., Genev\u00e8s, P., Laya\u00efda, N.: An Algebra with a Fixpoint Operator for Distributed Data Collections, March 2019. https:\/\/hal.inria.fr\/hal-02066649"},{"key":"7_CR8","doi-asserted-by":"publisher","first-page":"e27","DOI":"10.1017\/S0956796817000193","volume":"27","author":"L Fegaras","year":"2017","unstructured":"Fegaras, L.: An algebra for distributed Big Data analytics. J. Funct. Program. 27, e27 (2017). https:\/\/doi.org\/10.1017\/S0956796817000193","journal-title":"J. Funct. Program."},{"key":"7_CR9","unstructured":"Fegaras, L.: Compile-time query optimization for Big Data analytics. Open J. Big Data (OJBD) 5(1), 35\u201361 (2019). https:\/\/www.ronpub.com\/ojbd\/OJBD2019v5i1n02Fegaras.html"},{"key":"7_CR10","unstructured":"Hadoop: Apache Hadoop Documentation (2019). https:\/\/hadoop.apache.org\/docs\/r2.7.3\/"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/11575771_16","volume-title":"On the Move to Meaningful Internet Systems 2005: CoopIS, DOA, and ODBASE","author":"J Hidders","year":"2005","unstructured":"Hidders, J., Kwasnikowska, N., Sroka, J., Tyszkiewicz, J., Van den Bussche, J.: Petri Net + nested relational calculus = dataflow. In: Meersman, R., Tari, Z. (eds.) OTM 2005. LNCS, vol. 3760, pp. 220\u2013237. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11575771_16"},{"issue":"3","key":"7_CR12","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1016\/j.is.2007.09.002","volume":"33","author":"J Hidders","year":"2008","unstructured":"Hidders, J., Kwasnikowska, N., Sroka, J., Tyszkiewicz, J., Van den Bussche, J.: DFL: a dataflow language based on Petri Nets and nested relational calculus. Inf. Syst. 33(3), 261\u2013284 (2008)","journal-title":"Inf. Syst."},{"issue":"3","key":"7_CR13","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/s10009-007-0038-x","volume":"9","author":"K Jensen","year":"2007","unstructured":"Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri Nets and CPN tools for modelling and validation of concurrent systems. Int. J. Softw. Tools Technol. Transf. 9(3), 213\u2013254 (2007). https:\/\/doi.org\/10.1007\/s10009-007-0038-x","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"7_CR14","doi-asserted-by":"publisher","unstructured":"Kavi, K.M., Buckles, B.P., Bhat, N.: A formal definition of data flow graph models. IEEE Trans. Comput. C-35(11), 940\u2013948 (1986). https:\/\/doi.org\/10.1109\/TC.1986.1676696","DOI":"10.1109\/TC.1986.1676696"},{"issue":"9","key":"7_CR15","doi-asserted-by":"publisher","first-page":"1334","DOI":"10.1109\/TASSP.1987.1165275","volume":"35","author":"E Lee","year":"1987","unstructured":"Lee, E., Messerschmitt, D.: Pipeline interleaved programmable DSP\u2019s: synchronous data flow programming. IEEE Trans. Acoust. Speech Signal Process. 35(9), 1334\u20131345 (1987)","journal-title":"IEEE Trans. Acoust. Speech Signal Process."},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-319-77935-5_22","volume-title":"NASA Formal Methods","author":"F Marconi","year":"2018","unstructured":"Marconi, F., Quattrocchi, G., Baresi, L., Bersani, M.M., Rossi, M.: On the timed analysis of Big-Data applications. In: Dutle, A., Mu\u00f1oz, C., Narkawicz, A. (eds.) NFM 2018. LNCS, vol. 10811, pp. 315\u2013332. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-77935-5_22"},{"issue":"4","key":"7_CR17","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T Murata","year":"1989","unstructured":"Murata, T.: Petri Nets: properties, analysis and applications. Proc. IEEE 77(4), 541\u2013580 (1989). https:\/\/doi.org\/10.1109\/5.24143","journal-title":"Proc. IEEE"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-642-24690-6_24","volume-title":"Software Engineering and Formal Methods","author":"K Ono","year":"2011","unstructured":"Ono, K., Hirai, Y., Tanabe, Y., Noda, N., Hagiya, M.: Using Coq in specification and program extraction of Hadoop MapReduce applications. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 350\u2013365. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24690-6_24"},{"key":"7_CR19","unstructured":"Petri, C.A.: Kommunikation mit Automaten. Ph.D. thesis, Universit\u00e4t Hamburg (1962). (in German)"},{"key":"7_CR20","unstructured":"Souza Neto, J.B.: Transformation mutation for Spark programs testing. Ph.D. thesis, Federal University of Rio Grande do Norte (UFRN), Natal\/RN, Brazil (2020). (in Portuguese)"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/978-3-030-49435-3_30","volume-title":"Advanced Information Systems Engineering","author":"JB Souza Neto","year":"2020","unstructured":"Souza Neto, J.B., Martins Moreira, A., Vargas-Solar, G., Musicante, M.A.: Mutation operators for large scale data processing programs in Spark. In: Dustdar, S., Yu, E., Salinesi, C., Rieu, D., Pant, V. (eds.) CAiSE 2020. LNCS, vol. 12127, pp. 482\u2013497. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-49435-3_30"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Yang, F., Su, W., Zhu, H., Li, Q.: Formalizing MapReduce with CSP. In: 2010 17th IEEE International Conference and Workshops on Engineering of Computer Based Systems, pp. 358\u2013367 (2010)","DOI":"10.1109\/ECBS.2010.50"},{"key":"7_CR23","unstructured":"Yu, Y., et al.: DryadLINQ: a system for general-purpose distributed data-parallel computing using a high-level language. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI 2008, pp. 1\u201314. USENIX Association, Berkeley, CA, USA (2008). http:\/\/dl.acm.org\/citation.cfm?id=1855741.1855742"},{"key":"7_CR24","unstructured":"Zaharia, M., Chowdhury, M., Franklin, M.J., Shenker, S., Stoica, I.: Spark: cluster computing with working sets. In: Proceedings of the 2nd USENIX Conference on Hot Topics in Cloud Computing, HotCloud 2010, p. 10. USENIX Association, Berkeley, CA, USA (2010). http:\/\/dl.acm.org\/citation.cfm?id=1863103.1863113"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-63882-5_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,24]],"date-time":"2021-04-24T19:50:18Z","timestamp":1619293818000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-63882-5_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030638818","9783030638825"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-63882-5_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"19 November 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SBMF","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazilian Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ouro Preto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","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":"25 November 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 November 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sbmf2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sbmf2020.ufop.br\/","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":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"17","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":"10","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":"59% - 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":"1","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":"3 invited talks are also included. The symposium was held virtually due to the COVID-19 pandemic.","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)"}}]}}