A two-level formal model for Big Data processing programs

•A high-level model for iterative and non-iterative large-scale data processing programs.•Formalizing data flow with Petri Nets and data processing operations with Monoid Algebra.•Application of the model to formalize mutation operators for mutation testing in data flow programs.•Proposal of new mutation operators for iterative data flow programs.