Using formal verification to evaluate the execution time of Spark applications

DOI10.1007/S00165-020-00505-4MaRDI QIDQ782497zbMATH OpenOpenAlexWikidataFDO

Authors Marcello M. Bersani, F. Marconi, Gaetano Quattrocchi, Matteo Rossi, Luciano Baresi

Publication date 27 July 2020

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/11311/1135498

zbMATH Keywords

big dataformal verificationmetric temporal logictimed automata

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verifying equivalence of Spark programs
• Modeling multiclass task-based applications on heterogeneous distributed environments
• Modeling big data processing programs
• Property-based testing for Spark Streaming
• Stream data load prediction for resource scaling using online support vector regression

Cites work

• A decomposition theorem for partially ordered sets
• A logical characterization of timed regular languages
• A survey of timed automata for the development of real-time systems
• A theory of timed automata
• A tool for deciding the satisfiability of continuous-time metric temporal logic
• An automata-theoretic approach to constraint LTL
• Constraint LTL satisfiability checking without automata
• scientific article; zbMATH DE number 653618 (Why is no real title available?)
• scientific article; zbMATH DE number 1507210 (Why is no real title available?)
• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• scientific article; zbMATH DE number 3340881 (Why is no real title available?)
• Model-checking in dense real-time
• Model-checking timed temporal logics
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Scheduling with timed automata
• Well-structured transition systems everywhere!

Cited in

(1)

• Verifying equivalence of Spark programs

Describes a project that uses

Uses Software

• NuSMV
• SPIN
• Kronos
• Uppaal
• GitHub

This page was built for publication: Using formal verification to evaluate the execution time of Spark applications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q782497)