Call for Papers

Providing rigorous specification and analytic techniques for process-aware information systems is one of the main tasks to address in Business Process Management. For this purpose, in the last two decades well-established approaches from Formal Methods have been successfully developed and adopted so as to provide solid foundations and concrete tools for the automated analysis and testing of complex processes. 
FMBPM welcomes submissions that use Formal Methods to specify, model and analyze business processes and process-aware information systems. The aim of this workshop is to bring together researchers and practitioners who are interested in the application of formal methods to improve the quality of information systems, and specifically those that rely on BPM concepts and technologies. FMBPM strives at promoting research and development of formal methods and tools in all areas related to BPM: industrial applications, theoretical frameworks, formal modeling, algorithms and methodologies, tooling, experience reports including teaching and industrial cases. 
In addition, the workshop will provide a platform for discussions and the exchange of innovative ideas, thus we also highly encourage submissions on work in progress.

Submission Details

All papers should be in English and describe original work that has not been published or submitted elsewhere. All submissions will be reviewed by members of the Program Committee. Only papers in English will be considered. Submitted papers must present original research contributions not concurrently submitted elsewhere. Authors are requested to prepare submissions according to the LNBIP format specified by Springer (https://www.springer.com/computer/lncs?SGWID=0-164-6-791344-0). The title page must contain a short abstract and a list of keywords, preferably using the list of topics given above. Papers must be submitted electronically via EasyChair: enter the main conference installation (https://easychair.org/conferences/?conf=bpm2023) and select “Workshop on Formal Methods for BPM” as the submission track.
We are interested in research, work-in-progress, tools, case-study, position papers or surveys of two types:

Regular papers of up to 12 pages (including references)

Short papers of 5–6 pages (including references)

Topics of interests

Topics of interest include (but are not limited to) the following.

Modeling and related aspects. This topic covers techniques and languages supporting modeling of complex, process-aware information systems. We are interested in particular in:

• Formal specification languages for multi-perspective and/or probabilistic process models, where perspectives account for time, resources, data and their combination. 
• Formal representation of ethical, normative and legal aspects in business processes. 
• Compositionality and true concurrency in (multi-perspective) process models. 
• Formal modeling of cyber-physical processes and safety-critical information systems.
•  Theoretical foundations of process modeling frameworks. 
• Connections between foundational models and standard specification languages. 
• Meta-modeling approaches for BPM (e.g., formal languages for specifying meta-constraints between multiple process models). 
• Business process modeling methods and design science. 
• Requirements formalization and formal specification. 
• Procedural, declarative and hybrid modeling paradigms. 
• Formal modeling of service-oriented, cloud-based as well as component-based and multi-agent systems. 
• Design by contract.
  

Verification, validation and other analytic techniques. This topic covers foundational analytic techniques devised for formal models, including those mentioned above. The following themes help in understanding the potential submission topics:

• Automated reasoning and theorem proving techniques (and their advancements), including SAT and SMT, for analyzing (multi-perspective) process models. 
• Static analysis, safety checking, correctness by construction, abstraction, modularization and refinement techniques. 
• Runtime verification and monitoring of business processes. 
• Formal analysis of timed, real-time, hybrid and probabilistic process models. 
• Automata-theoretic approaches for process analysis. 
• Synthesis, planning and scheduling. 
• Game theoretic techniques in BPM. 
• Techniques and algorithms for scaling formal analysis in BPM (e.g., symbolic methods, abstraction, modular and compositional techniques, parallel and/or distributed techniques). 
• Analysis of QoS and other non-functional properties (e.g., trust, compliance, security, privacy). 
• Analytic techniques with formal guarantees such as decidabilities and computational complexity. 
• Process correctness and compliance by design.
• Combination of static and dynamic analytic methods. 
• Formally-grounded performance analysis approaches. 
• Compliance and conformance checking. 
• Process evolution, maintenance, re-engineering and reuse. 
• Statistical and probabilistic analysis. 
• Business process specification synthesis and repair. 
• Techniques focusing on analytic tasks for modern process-aware information systems that are currently addressed ad-hoc.

Tools. We invite those who are currently developing tools or having at hand already running prototypes to reflect on related topics, that may touch upon the following themes:

• Verification and analytic tools for BPM: engineering and implementation, benchmarks and comparative studies. 
• Description and showcasing of publicly available artifacts of formal method applications in BPM. 
• Integration of formal methods tools.
• Design and implementation of integrated modeling and verification environments.
• Experimental validation, studies of scalability issues of formal methods techniques for BPM analytic tasks.

Applications. We highly solicit the scientific community to share their experience and ideas of how formal methods are or should be applied in BPM.

• Model-driven engineering of process-aware information systems. 
• Formal analysis support for modeling languages used in industry. 
• Limitations of formal methods in BPM regarding their usability and scalability. 
• Use of formal methods for automated testing and simulation of business processes. 
• Innovative ways of using formal methods in BPM. 
• Usability of formal methods and guidelines of how to use them in practice. 
• Process debugging. 
• Applications of formal methods for analytic tasks within the BPM spectrum, e.g., in automated generation of event logs via model simulations. 
• Impact of the adoption of formal methods on the process development and associated costs. 
• Application of formal methods in standardization in BPM.

Case studies and experience reports (teaching, industrial use cases, etc).

• Empirical evaluations of formal methods in BPM Design and empirical case studies. 
• Insightful surveys, case studies and experience reports on the adoption and application of formal methods, both from academy and industry.
• Experience reports on teaching formal methods in the BPM context or with references to BPM. 
• Discussions of future/new research directions and open questions related to formal methods in BPM.

Organizers

• Claudio Di Ciccio - Sapienza University of Rome, Italy
• Alessandro Gianola - Free University of Bozen-Bolzano, Italy
• Andrey Rivkin - Technical University of Denmark, Denmark

Program Committee

• Carl Corea, University of Koblenz-Landau, Germany
• Jörg Desel, FernUniversität in Hagen, Germany
• Chiara Di Francescomarino, DISI - University of Trento, Italy
• Dirk Fahland, Eindhoven University of Technology, Netherlands
• Sérgio Guerreiro, INESC-ID / Instituto Superior Técnico, Portugal
• Sylvain Hallé, Université du Québec à Chicoutimi, Canada
• Thomas Hildebrandt, University of Copenhagen, Denmark
• Cosimo Laneve, University of Bologna, Italy
• Hugo A. López, Technical University of Denmark, Denmark
• Andrea Marrella, Sapienza University of Rome, Italy
• Fabio Patrizi, Sapienza University of Rome, Italy
• Pascal Poizat, Université Paris Nanterre and LIP6, France
• Jorge A. Pérez, University of Groningen, Netherlands
• Barbara Re, University of Camerino, Italy
• Gwen Salaün, University of Grenoble Alpes, France
• Jianwen Su, University of California Santa Barbara, USA
• Sergio Tessaris, Free University of Bozen-Bolzano, Italy
• Emilio Tuosto, Gran Sasso Science Institute, Italy
• Andrea Vandin, Sant'Anna School of Advanced Studies, Italy
• Victor Vianu, University of California San Diego, USA
• Matthias Weidlich, Humboldt-Universität zu Berlin, Germany
• Mathias Weske, HPI - University of Potsdam, Germany
• Sarah Winkler, Free University of Bozen-Bolzano, Italy
• Matteo Zavatteri, University of Padova, Italy

Accepted Papers

Full papers:

• Mohammadreza Fani Sani, Martin Kabierski, Sebastiaan van Zelst and Wil van der Aalst, Model Independent Error Bound Estimation for Conformance Checking Approximation.
• Matteo Zavatteri, Davide Bresolin and Massimiliano de Leoni, Repair of Unsound Data-Aware Process Models.
• Isabelle Kuhlmann, Carl Corea and John Grant, Non-Automata Based Conformance Checking of Declarative Process Specifications Based on ASP.
• Marco Montali and Sarah Winkler, Equivalence of Data Petri Nets with Arithmetic.

Short papers:

• Alessandro Burigana and Marco Montali, Reasoning about Knowledge in BPM: A Systematic Approach.
• Luca Geatti, Alessandro Gianola and Nicola Gigante, Formal Specification of Business Processes in LTL Modulo Theories over Finite Traces.

Program

Invited Talk

Invited Speaker: Joost-Pieter Katoen, RWTH Aachen University

Title: What Can Probabilistic Model Checking Offer to BPM?

Abstract. Probabilistic model checking (PMC) is a fully automated technique to verify a broad range of properties on Markov models. Given such a model, it can compute e.g. the probability to ever reach a bad state or the probability that three requests are issued before a response occurs. Tools such as Storm and PRISM scale to models with billions of states. PMC requires all probabilities in the system model to be known. In many scenarios this is a stringent requirement. Parameter synthesis aims at answering "for which probability values is the probability to ever reach a bad state low"? It thus explores the design space and provides useful information to decide whether a model is good or not. Recent advances allow to treat models with up to thousand parametric probabilities. In this talk, I will introduce these techniques and illustrate its application. I will also report on first investigations on how PMC can be used to stochastic conformance checking in BPM, and argue that PMC can address various aspects that could be relevant for stochastic process mining.

Detailed Program

Session 1 (13.45-15.15)

• Opening
• Mohammadreza Fani Sani, Martin Kabierski, Sebastiaan van Zelst and Wil van der Aalst. Model Independent Error Bound Estimation for Conformance Checking Approximation. (long)
• Matteo Zavatteri, Davide Bresolin and Massimiliano de Leoni. Repair of Unsound Data-Aware Process Models. (long)
• Marco Montali and Sarah Winkler. Equivalence of Data Petri Nets with Arithmetic. (long)
• Luca Geatti, Alessandro Gianola and Nicola Gigante. Formal Specification of Business Processes in LTL Modulo Theories over Finite Traces. (short)
• Isabelle Kuhlmann, Carl Corea and John Grant. Non-Automata Based Conformance Checking of Declarative Process Specifications Based on ASP. (long)
• Alessandro Burigana and Marco Montali. Reasoning about Knowledge in BPM: Call for a Systematic Approach. (short)

Session 2 (16.00-17.30)

• Invited talk by Joost-Pieter Katoen (Title: “What Can Probabilistic Model Checking Offer to BPM?”)
• Closing

Time for talks

• Long papers: 15 minutes (10min presentation + 5min Q&A)
• Short papers: 10 minutes (7min presentation + 3min Q&A)